Term rewriting has a significant presence in various areas, not least in automated theorem proving where it is used as a proof technique. Many theorem provers employ specialised proof tactics for rewriting. This results in an interleaving between deduction and computation (i.e., rewriting) steps. If the logic of reasoning supports partial functions, it is necessary that rewriting copes with potentially ill-defined terms. In this paper, we provide a basis for integrating rewriting with a deductive proof system that deals with well-definedness. The definitions and theorems presented in this paper are the theoretical foundations for an extensible rewriting-based prover that has been implemented for the set theoretical formalism Event-B.
A proof tableau of Hoare logic is an annotated program with pre- and post-conditions, which corresponds to an inference tree of Hoare logic. In this paper, we show that a proof tableau for partial correctness can be transformed into an inference sequence of rewriting induction for constrained rewriting. We also show that the resulting sequence is a valid proof for an inductive theorem corresponding to the Hoare triple if the constrained rewriting system obtained from the program is terminating. Such a valid proof with termination of the constrained rewriting system implies total correctness of…
In this note we give a simple unifying proof of the undecidability of several diagrammatic properties of term rewriting systems that include: local confluence, strong confluence, diamond property, subcommutative property, and the existence of successor. The idea is to code configurations of Turing Machines into terms, and then define a suitable relation on those terms such that the termination of the Turing Machine becomes equivalent to the satisfiability of the diagrammatic property.
We introduce a sound and complete coinductive proof system for reachability properties in transition systems generated by logically constrained term rewriting rules over an order-sorted signature modulo builtins. A key feature of the calculus is a circularity proof rule, which allows to obtain finite representations of the infinite coinductive proofs.
Several proof assistants, such as Isabelle or Coq, can concurrently check multiple proofs. In contrast, the vast majority of today's small proof checkers either does not support concurrency at all or only limited forms thereof, restricting the efficiency of proof checking on multi-core processors. This work shows the design of a small, memory- and thread-safe kernel that efficiently checks proofs both concurrently and non-concurrently. This design is implemented in a new proof checker called Kontroli for the lambda-Pi calculus modulo rewriting, which is an established framework to uniformly ex…
Proof terms in term rewriting are a representation means for reduction sequences, and more in general for contraction activity, allowing to distinguish e.g simultaneous from sequential reduction. Proof terms for finitary, first-order, left-linear term rewriting are described in the Terese book, chapter 8. In a previous work, we defined an extension of the finitary proof-term formalism, that allows to describe contractions in infinitary first-order term rewriting, and gave a characterisation of permutation equivalence. In this work, we discuss how projections of possibly infinite rewrite sequen…
Linear rules have played an increasing role in structural proof theory in recent years. It has been observed that the set of all sound linear inference rules in Boolean logic is already coNP-complete, i.e. that every Boolean tautology can be written as a (left- and right-)linear rewrite rule. In this paper we study properties of systems consisting only of linear inferences. Our main result is that the length of any 'nontrivial' derivation in such a system is bound by a polynomial. As a consequence there is no polynomial-time decidable sound and complete system of linear inferences, unless coNP…
We introduce proof terms for string rewrite systems and, using these, show that various notions of equivalence on reductions known from the literature can be viewed as different perspectives on the notion of causal equivalence. In particular, we show that permutation equivalence classes (as known from the lambda-calculus and term rewriting) are uniquely represented both by trace graphs (known from physics as causal graphs) and by so-called greedy multistep reductions (as known from algebra). We present effective maps from the former to the latter, topological multi-sorting TM, and vice versa, …
The notion of normal forms is ubiquitous in various equivalent transformations. Confluence (CR), one of the central properties of term rewriting systems (TRSs), concerns uniqueness of normal forms. Yet another such property, which is weaker than confluence, is the property of unique normal forms w.r.t. conversion (UNC). Famous examples having UNC but not CR include the TRSs consisting of S,K,I-rules for the combinatory logic supplemented with various pairing rules (de Vrijer, 1999). Recently, automated confluence proof of TRSs has caught attentions leading to investigations of automatable meth…
This paper develops an algorithmic-based approach for proving inductive properties of propositional sequent systems such as admissibility, invertibility, cut-elimination, and identity expansion. Although undecidable in general, these structural properties are crucial in proof theory because they can reduce the proof-search effort and further be used as scaffolding for obtaining other meta-results such as consistency. The algorithms -- which take advantage of the rewriting logic meta-logical framework, and use rewrite- and narrowing-based reasoning -- are explained in detail and illustrated wit…
In this paper, we prove that (first-order) cons-free term rewriting with a call-by-value reduction strategy exactly characterises the class of PTIME-computable functions. We use this to give an alternative proof of the result by Carvalho and Simonsen which states that cons-free term rewriting with linearity constraints characterises this class.
Driven by the interest of reasoning about probabilistic programming languages, we set out to study a notion of unicity of normal forms for them. To provide a tractable proof method for it, we define a property of distribution confluence which is shown to imply the desired uniqueness (even for infinite sequences of reduction) and further properties. We then carry over several criteria from the classical case, such as Newman's lemma, to simplify proving confluence in concrete languages. Using these criteria, we obtain simple proofs of confluence for $λ_1$, an affine probabilistic $λ$-calculus, a…
We show confluence of a conditional term rewriting system CL-pc${}^1$, which is an extension of Combinatory Logic by Boolean constants. This solves problem 15 from the RTA list of open problems. The proof has been fully formalised in the Coq proof assistant.
In this paper, we reconsider the unfolding-based technique that we have introduced previously for detecting loops in standard term rewriting. We improve it by guiding the unfolding process, using distinguished positions in the rewrite rules. This results in a depth-first computation of the unfoldings, whereas the original technique was breadth-first. We have implemented this new approach in our tool NTI and compared it to the previous one on a bunch of rewrite systems. The results we get are promising (better times, more successful proofs).
Dedukti has been proposed as a universal proof checker. It is a logical framework based on the lambda Pi calculus modulo that is used as a backend to verify proofs coming from theorem provers, especially those implementing some form of rewriting. We present a shallow embedding into Dedukti of proofs produced by Zenon Modulo, an extension of the tableau-based first-order theorem prover Zenon to deduction modulo and typing. Zenon Modulo is applied to the verification of programs in both academic and industrial projects. The purpose of our embedding is to increase the confidence in automatically …
Since the very beginning of the theory of linear logic it is known how to represent the $λ$-calculus as linear logic proof nets. The two systems however have different granularities, in particular proof nets have an explicit notion of sharing---the exponentials---and a micro-step operational semantics, while the $λ$-calculus has no sharing and a small-step operational semantics. Here we show that the \emph{linear substitution calculus}, a simple refinement of the $λ$-calculus with sharing, is isomorphic to proof nets at the operational level. Nonetheless, two different terms with sharing can s…
RP-Rewriter (Retain-Property) is a verified clause processor that can use some of the existing ACL2 rewrite rules to prove conjectures through term rewriting. Optimized for conjectures that can expand into large terms, the rewriter tries to mimic some of the ACL2 rewriting heuristics but also adds some extra features. It can attach side-conditions to terms that help the rewriter retain properties about them and prevent possibly some very expensive backchaining. The rewriter supports user-defined complex meta rules that can return a special structure to prevent redundant rewriting. Additionally…
Time complexity in rewriting is naturally understood as the number of steps needed to reduce terms to normal forms. Establishing complexity bounds to this measure is a well-known problem in the rewriting community. A vast majority of techniques to find such bounds consist of modifying termination proofs in order to recover complexity information. This has been done for instance with semantic interpretations, recursive path orders, and dependency pairs. In this paper, we follow the same program by tailoring tuple interpretations to deal with innermost complexity analysis. A tuple interpretation…
This book can be seen either as a text on theorem proving that uses techniques from general algebra, or else as a text on general algebra illustrated and made concrete by practical exercises in theorem proving. The book considers several different logical systems, including first-order logic, Horn clause logic, equational logic, and first-order logic with equality. Similarly, several different proof paradigms are considered. However, we do emphasize equational logic, and for simplicity we use only the OBJ3 software system, though it is used in a rather flexible manner. We do not pursue the lof…
