Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Fundamenta Informaticae

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: equational reasoning

Sortuj według:

Ogranicz wyniki do:

Combining Satisfiability Procedures for Unions of Theories with a Shared Counting Operator

Nicolini E., Ringeissen C., Rusinowitch M.

Fundamenta Informaticae

2011

Vol. 105, nr 1/2

163-187

We present some decidability results for the universal fragment of theories modeling data structures and endowed with arithmetic constraints. More precisely, all the theories taken into account extend a theory that constrains the function symbol for the successor. A general decision procedure is obtained, by devising an appropriate calculus based on superposition. Moreover, we derive a decidability result for the combination of the considered theories for data structures and some fragments of arithmetic by applying a general combination schema for theories sharing a common subtheory. The effectiveness of the resulting algorithm is ensured by using the proposed calculus and a careful adaptation of standard methods for reasoning about arithmetic, such as Gauss elimination, Fourier-Motzkin elimination and Groebner bases computation.

Names, equations, relations : practical ways to reason about new

Stark I.

Fundamenta Informaticae

1998

Vol. 33, nr 4

369-396

The nu-calculus of Pitts and Stark is a typed lambda-calculus, extended with state in the from of dynamically-generated names. These names can be created locally, passed around, and compared with one another. Through the interaction between names and functions, the language can capture notions of scope, visibility and sharing. Originally motivated by the study of references in Standard ML, the nu-calculus has connections to local declaations in general; to the mobile processes of the p-calculus; and to security protocols in the spi-calculus. This paper introduces a logic of equations and relations which allows one to reason about expressions of the nu-calculus: this uses a simple representation of the private and public scope of names, and allows straightforward proofs of contextual equivalence (also known as observational, or observable, equivalence). The logic based on earlier operational techniques, providing the same power but in a much more accessible from. In particular it allows intuitive and direct proofs of all contextual equivalences between first-order functions with local names.