Catálogo de publicaciones - libros

We present constructive arithmetic in Deduction modulo with rewrite rules only.

We define infinitary combinatory reduction systems (iCRSs). This provides the first extension of infinitary rewriting to higher-order rewriting. We lift two well-known results from infinitary term rewriting systems and infinitary -calculus to iCRSs:

Many applications of congruence closure nowadays require the ability of recovering, among the thousands of input equations, the small subset that caused the equivalence of a given pair of terms. For this purpose, here we introduce an incremental congruence closure algorithm that has an additional operation.

First, two variations of union-find data structures with are introduced. Then, these are applied inside a congruence closure algorithm with , where a -step proof can be recovered in almost optimal time (quasi-linear in ), without increasing the overall ( log ) runtime of the fastest known congruence closure algorithms.

This non-trivial (ground) equational reasoning result has been quite intensively sought after (see, e.g., [SD99,dMRS04,KS04]), and moreover has important applications to verification.

Proofs of equalities may be built from assumptions using proof rules for reflexivity, symmetry, and transitivity. Reflexivity is an axiom proving x=x for any x; symmetry is a 1-premise rule taking a proof of x=y and returning a proof of y=x; and transitivity is a 2-premise rule taking proofs of x=y and y=z, and returning a proof of x=z. Define an equivalence relation to hold between proofs iff they prove a theorem in common. The main theoretical result of the paper is that if all assumptions are independent, this equivalence relation is axiomatized by the standard axioms of group theory: reflexivity is the unit of the group, symmetry is the inverse, and transitivity is the multiplication. Using a standard completion of the group axioms, we obtain a rewrite system which puts equality proofs into canonical form. Proofs in this canonical form use the fewest possible assumptions, and a proof can be canonized in linear time using a simple strategy. This result is applied to obtain a simple extension of the union-find algorithm for ground equational reasoning which produces minimal proofs. The time complexity of the original union-find operations is preserved, and minimal proofs are produced in worst-case time , where is the number of expressions being equated. As a second application, the approach is used to achieve significant performance improvements for the CVC cooperating decision procedure.

We consider the problem of symbolic reachability analysis of a class of term rewrite systems called Process Rewrite Systems (PRS). A PRS can be seen as the union of two mutually interdependent sets of term rewrite rules: a prefix rewrite system (or, equivalently, a pushdown system), and a multiset rewrite system (or, equivalently, a Petri net). These systems are natural models for multithreaded programs with dynamic creation of concurrent processes and recursive procedure calls. We propose a generic framework based on tree automata allowing to combine (finite-state automata based) procedures for the reachability analysis of pushdown systems with (linear arithmetics/semilinear sets based) procedures for the analysis of Petri nets in order to analyze PRS models. We provide a construction which is parametrized by such procedures and we show that it can be instantiated to (1) derive procedures for constructing the (exact) reachability sets of significant classes of PRS, (2) derive various approximate algorithms, or exact semi-algorithms, for the reachability analysis of PRS obtained by using existing symbolic reachability analysis techniques for Petri nets and counter automata.

In this paper, we consider the monadic second order logic (MSO) and two of its extensions, namely Counting MSO (CMSO) and Presburger MSO (PMSO), interpreted over unranked and unordered trees. We survey classes of tree automata introduced for the logics PMSO and CMSO as well as other related formalisms; we gather results from the literature and sometimes clarify or fill the remaining gaps between those various formalisms. Finally, we complete our study by adapting these classes of automata for capturing precisely the expressiveness of the logic MSO.