In most theorem proving applications, a proper treatment of equational theories or equality is mandatory. In this paper we show how to integrate a modern treatment of equality in ...
Abstract The situation calculus is one of the most established formalisms for reasoning about action and change. In this paper we will review the basics of Reiter’s version of th...
Introduced at the end of the nineties, the Rewriting Calculus (ρ-calculus, for short) is a simple calculus that fully integrates term-rewriting and λ-calculus. The rewrite rules...
Paolo Baldan, Clara Bertolissi, Horatiu Cirstea, C...
We obtain a new formalism for concurrent object-oriented languages by extending Abadi and Cardelli's imperative object calculus with operators for concurrency from the -calc...
The past decade has seen an explosion of work on calculi of explicit substitutions. Numerous work has illustrated the usefulness of these calculi for practical notions like the im...
The paper focusses on the logical backgrounds of the Dijkstra-Scholten program development style for correct programs. For proving the correctness of a program (i.e. the fact that...
Parallel computers have not yet had the expected impact on mainstream computing. Parallelism adds a level of complexity to the programming task that makes it very error-prone. More...
We present a calculus for modelling "environment-aware" computations, that is computations that adapt their behaviour according to the capabilities of the environment. T...
Tarski-Givant's map calculus is briefly reviewed, and a plan of research is outlined aimed at investigating applications of this ground equational formalism in the theorem-pr...
Andrea Formisano, Eugenio G. Omodeo, Marco Temperi...
In 1969 Cordell Green presented his seminal description of planning as theorem proving with the situation calculus. The most pleasing feature of Green's account was the negli...