Theorem Proving Modulo

Deduction modulo is a way to remove computational arguments from proofs by reasoning modulo a congruence on propositions. Such a technique, issued from automated theorem proving, is of general interest because it permits one to separate computations and deductions in a clean way. The first contribution of this paper is to define a sequent calculus modulo that gives a proof-theoretic account of the combination of computations and deductions. The congruence on propositions is handled through rewrite rules and equational axioms. Rewrite rules apply to terms but also directly to atomic propositions. The second contribution is to give a complete proof search method, called extended narrowing and resolution (ENAR), for theorem proving modulo such congruences. The completeness of this method is proved with respect to provability in sequent calculus modulo. An important application is that higher-order logic can be presented as a theory in deduction modulo. Applying the ENAR method to this presentation of higher-order logic subsumes full higher-order resolution. This revised version was published online in August 2006 with corrections to the Cover Date.     

Clausal Presentation of Theories in Deduction Modulo

Resolution modulo is an extension of first-order resolution in which rewrite rules are used to rewrite clauses during the search. In the first version of this method, clauses are rewritten to arbitrary propositions. These propositions are needed to be dynamically transformed into clauses. This unpleasant feature can be eliminated when the rewrite system is clausal, i.e., when it rewrites clauses to clauses. We show in this paper how to transform any rewrite system into a clausal one, preserving the existence of cut free proofs of any sequent.     

A modal logic internalizing normal proofs

In the proof-theoretic study of logic, the notion of normal proof has been understood and investigated as a metalogical property. Usually we formulate a system of logic, identify a class of proofs as normal proofs, and show that every proof in the system reduces to a corresponding normal proof. This paper develops a system of modal logic that is capable of expressing the notion of normal proof within the system itself, thereby making normal proofs an inherent property of the logic. Using a modality △ to express the existence of a normal proof, the system provides a means for both recognizing and manipulating its own normal proofs. We develop the system as a sequent calculus with the implication connective ⊃ and the modality △, and prove the cut elimination theorem. From the sequent calculus, we derive two equivalent natural deduction systems.     

A new mapping between combinatorial proofs and sequent calculus proofs read out from logical flow graphs

Combinatorial proofs are abstract invariants for sequent calculus proofs, similarly to homotopy groups which are abstract invariants for topological spaces. Sequent calculus fails to be surjective onto combinatorial proofs, and here we extract a syntactically motivated closure of sequent calculus from which there is a surjection onto a complete set of combinatorial proofs. We characterize a class of canonical sequent calculus proofs for the full set of propositional tautologies and derive a new completeness theorem for combinatorial propositions. For this, we define a new mapping between combinatorial proofs and sequent calculus proofs, different from the one originally proposed, which explicitly links the logical flow graph of a proof to a skew fibration between graphs of formulas. The categorical properties relating the original and the new mappings are explicitly discussed.     

Resolution is Cut-Free

In this article, we show that the extension of the resolution proof system to deduction modulo is equivalent to the cut-free fragment of the sequent calculus modulo. The result is obtained through a syntactic translation, without using any cut-elimination procedure. Additionally, we show Skolem theorem and inversion/focusing results. Thanks to the expressiveness of deduction modulo, all these results also apply to the cases of higher-order resolution, Peano’s arithmetic and Gentzen’s LK.     

The <Emphasis Type="Italic">λ</Emphasis>-Calculus and the Unity of Structural Proof Theory

In the context of intuitionistic implicational logic, we achieve a perfect correspondence (technically an isomorphism) between sequent calculus and natural deduction, based on perfect correspondences between left-introduction and elimination, cut and substitution, and cut-elimination and normalisation. This requires an enlarged system of natural deduction that refines von Plato’s calculus. It is a calculus with modus ponens and primitive substitution; it is also a “coercion calculus”, in the sense of Cervesato and Pfenning. Both sequent calculus and natural deduction are presented as typing systems for appropriate extensions of the λ-calculus. The whole difference between the two calculi is reduced to the associativity of applicative terms (sequent calculus = right associative, natural deduction = left associative), and in fact the achieved isomorphism may be described as the mere inversion of that associativity. The novel natural deduction system is a “multiary” calculus, because “applicative terms” may exhibit a list of several arguments. But the combination of “multiarity” and left-associativity seems simply wrong, leading necessarily to non-local reduction rules (reason: normalisation, like cut-elimination, acts at the head of applicative terms, but natural deduction focuses at the tail of such terms). A solution is to extend natural deduction even further to a calculus that unifies sequent calculus and natural deduction, based on the unification of cut and substitution. In the unified calculus, a sequent term behaves like in the sequent calculus, whereas the reduction steps of a natural deduction term are interleaved with explicit steps for bringing heads to focus. A variant of the calculus has the symmetric role of improving sequent calculus in dealing with tail-active permutative conversions.     

Dual Systems of Tableaux and Sequents for PLTL

On one hand, traditional tableau systems for temporal logic (TL) generate an auxiliary graph that must be checked and (possibly) pruned in a second phase of the refutation procedure. On the other hand, traditional sequent calculi for TL make use of a kind of inference rules (mainly, invariant-based rules or infinitary rules) that complicates their automatization. A remarkable consequence of using auxiliary graphs in the tableaux framework and invariants or infinitary rules in the sequents framework is that TL fails to carry out the classical correspondence between tableaux and sequents. In this paper, we first provide a tableau method TTM that does not require auxiliary graphs to decide whether a set of PLTL-formulas is satisfiable. This tableau method TTM is directly associated to a one-sided sequent calculus called TTC. Since TTM is free from all the structural rules that hinder the mechanization of deduction, e.g. weakening and contraction, then the resulting sequent calculus TTC is also free from this kind of structural rules. In particular, TTC is free of any kind of cut, including invariant-based cut. From the deduction system TTC, we obtain a two-sided sequent calculus GTC that preserves all these good freeness properties and is finitary, sound and complete for PTL. Therefore, we show that the classical correspondence between tableaux and sequent calculi can be extended to TL. Every deduction system is proved to be complete. In addition, we provide illustrative examples of deductions in the different systems.     

Dynamically Typed Computations for Order-sorted Equational Presentations

Equational presentations with ordered sorts encompass partially defined functions and subtyping information in an algebraic framework. In this work we address the problem of computing in order-sorted algebras, with few restrictions on the allowed presentations. We adopt the G-algebra framework, where equational, membership and existence formulas can be expressed, and this provides a complete deduction calculus which incorporates the interaction between all these formulas.To practically deal with this calculus, we introduce an operational semantics for G-algebra using rewrite systems over so-called decorated terms, that has assertions concerning the sort membership of any subterm in its head node. Decorated rewrite rules perform equational replacement, decoration rewrite rules enrich the decorations and record sort information. Therefore we use the semantic sort principle, i.e. equal terms belong to equal sorts, rather than the syntactic sort principle that does not use the equational part of a presentation.In order to have a complete and decidable unification on decorated terms, we restrict to sort-inheritance theories. Then a completion procedure on decorated terms is designed to compute all interactions between equational and membership formulas. When the completion terminates, the resulting set of rewrite rules provides a way to decide equational theorems of the form (t = t′) and typing theorems of the form (t : A).The sort inheritance property is undecidable in general but we propose a test to check it for a given presentation. The test provides information on how to extend the presentation in a model conservative way, in order to obtain sort inheritance.     

On the Formalization of the Modal μ-Calculus in the Calculus of Inductive Constructions

We present a natural deduction proof system for the propositional modal μ-calculus and its formalization in the calculus of inductive constructions. We address several problematic issues, such as the use of higher-order abstract syntax in inductive sets in the presence of recursive constructors, and the formalization of modal (sequent-style) rules and of context sensitive grammars. The formalization can be used in the system Coq, providing an experimental computer-aided proof environment for the interactive development of error-free proofs in the modal μ-calculus. The techniques we adopt can be readily ported to other languages and proof systems featuring similar problematic issues.     

Inductive proof search modulo

We present an original narrowing-based proof search method for inductive theorems in equational rewrite theories given by a rewrite system $\mathcal{R}$ and a set E of equalities. It has the specificity to be grounded on deduction modulo and to rely on narrowing to provide both induction variables and instantiation schemas. Whenever the equational rewrite system $(\mathcal{R},E)$ has good properties of termination, sufficient completeness, and when E is constructor and variable preserving, narrowing at defined-innermost positions leads to consider only unifiers which are constructor substitutions. This is especially interesting for associative and associative-commutative theories for which the general proof search system is refined. The method is shown to be sound and refutationally correct and complete. A major feature of our approach is to provide a constructive proof in deduction modulo for each successful instance of the proof search procedure.     

Certifying Term Rewriting Proofs in ELAN

Term rewriting has been shown to be a good environment for both programming and proving. For analysing and debugging rule-based programs, we propose in this work a formalism based on the rewriting calculus with explicit substitutions (ρσ-calculus). This formalism also allows us to build the proof terms of rewriting derivations. Therefore, term rewriting proofs can be exported to other systems by translating them into the corresponding syntaxes. That is, using a proof checker, one can certify these proofs and vice versa, this method allows us to get term rewriting in proof assistants using an external system. Our method not only works with syntactic rewriting but also with rewriting modulo a set of axioms (e.g. associativity-commutativity).     

Issues in the Analysis of Proof-Search Strategies in Sequential Presentations of Logics

Many proof search strategies can be expressed as restrictions on the order of application of the rules of the sequent calculus. Properties of these strategies are then shown by permutation arguments, such as showing that a given strategy is complete by transforming an arbitrary proof into one which obeys the strategy. Such analyses involve some very tedious manipulations of proofs, and are potentially overwhelming for humans. In this paper we investigate the development of systematic techniques for the analysis of sequent calculi. We show how a particular specification of inference rules leads to a detailed analysis of permutation properties for these rules, and we also investigate how to detect redundancies in proofs resulting from these rules.     

A Port Graph Calculus for Autonomic Computing and Invariant Verification

From our previous work on biochemical applications, the structure of port graph (or multigraph with ports) and a rewriting calculus have proved to be well-suited formalisms for modeling interactions between proteins. Then port graphs have been proposed as a formal model for distributed resources and grid infrastructures, where each resource is modeled by a node with ports. The lack of global information and the autonomous and distributed behavior of components are modeled by a multiset of port graphs and rewrite rules which are applied locally, concurrently, and non-deterministically. Some computations take place wherever it is possible and in parallel, while others may be controlled by strategies. In this paper, we first introduce port graphs as graphs with multiple edges and loops, with nodes having explicit connection points, called ports, and edges attaching to ports of nodes. We then define an abstract biochemical calculus that instantiates to a rewrite calculus on these graphs. Rules and strategies are themselves port graphs, i.e. first-class objects of the calculus. As a consequence, they can be rewritten as well, and rules can create new rules, providing a way of modeling adaptive systems. This approach also provides a formal framework to reason about computations and to verify useful properties. We show how structural properties of a modeled system can be expressed as strategies and checked for satisfiability at each step of the computation. This provides a way to ensure invariant properties of a system. This work is a contribution to the formal specification and verification of adaptive systems and to theoretical foundations of autonomic computing.     

Lifting lower bounds for tree-like proofs

It is known that constant-depth Frege proofs of some tautologies require exponential size. No such lower bound result is known for more general proof systems. We consider tree-like sequent calculus proofs in which formulas can contain modular connectives and only the cut formulas are restricted to be of constant depth. Under a plausible hardness assumption concerning small-depth Boolean circuits, we prove exponential lower bounds for such proofs. We prove these lower bounds directly from the computational hardness assumption. We start with a lower bound for cut-free proofs and “lift” it so it applies to proofs with constant-depth cuts. By using the same approach, we obtain the following additional results. We provide a much simpler proof of a known unconditional lower bound in the case where modular connectives are not used. We establish a conditional exponential separation between the power of constant-depth proofs that use different modular connectives. We show that these tree-like proofs with constant-depth cuts cannot polynomially simulate similar dag-like proofs, even when the dag-like proofs are cut-free. We present a new proof of the non-finite axiomatizability of the theory of bounded arithmetic I Δ₀(R). Finally, under a plausible hardness assumption concerning the polynomial-time hierarchy, we show that the hierarchy \({G_i^*}\) of quantified propositional proof systems does not collapse.     

Reasoning with first order nondeterministic specifications

The paper presents a variant of first order logic for specifying nondeterministic software. Models of the logics are multialgebras, i.e. multi-sorted algebras with set-valued operations, together with multi-sorted valuations of variables. We allow empty carrier sets but the valuations are kept total. Terms are interpreted as sets and the usual set of algebraic terms is extended by an additional construct used for limiting nondeterminism. Atomic formulae are of the form where is a rewrite operator, corresponding semantically to inclusion. For the above logic, we develop two complete deduction systems in the natural deduction style: a Rasiowa-Sikorski system for sequences of formulae, and a cut-free Gentzen-style sequent calculus. We also consider the issues of determinism and partiality, proposing alternate solutions to defining the respective predicates in our logic. Received: 4 March 1997 / 25 May 1999     

Non-commutative logic III: focusing proofs

It is now well-established that the so-called focalization property plays a central role in the design of programming languages based on proof search, and more generally in the proof theory of linear logic. We present here a sequent calculus for non-commutative logic (NL) which enjoys the focalization property. In the multiplicative case, we give a focalized sequentialization theorem, and in the general case, we show that our focalized sequent calculus is equivalent to the original one by studying the permutabilities of rules for NL and showing that all permutabilities of linear logic involved in focalization can be lifted to NL permutabilities. These results are based on a study of the partitions of partially ordered sets modulo entropy.     

Static analysis of Linear Logic programming

Linear Logic is gaining momentum in computer science because it offers a unified framework and a common vocabulary for studying and analyzing different aspects of programming and computation. We focus here on models where computation is identified with proof search in the sequent system of Linear Logic. A proof normalization procedure, called “focusing”, has been proposed to make the problem of proof search tractable. Correspondingly, there is a normalization procedure mapping formulae of Linear Logic into a syntactic fragment of that logic, calledLinLog, where the focusing normalization for proofs can be most conveniently expressed. In this paper, we propose to push this compilation/normalization process further, by applying abstract interpretation and partial evaluation techniques to (focused) proofs inLinLog. These techniques provide information concerning the evolution of the computational resources (formulae) during the execution (proof construction). The practical outcome that we expect from this theoretical effort is the definition of a general tool for statically analyzing and reasoning about the runtime behavior of programs in frameworks where computations can be accounted for in terms of proof search in Linear Logic.     

针对教学场景的ZFC集合论Coq形式化

离散数学是计算机类专业的基础课程之一,命题逻辑、一阶逻辑与公理集合论是其重要组成部分.教学实践表明,初学者准确理解语法、语义、推理系统等抽象概念是有一定难度的.近年来,已有一些学者开始在教学中引入交互式定理证明工具,以帮助学生构造形式化证明,更透彻地理解逻辑系统.然而,现有的定理证明器有较高上手门槛,直接使用会增加学生的学习负担.鉴于此,在Coq中开发了针对教学场景的ZFC公理集合论证明器.首先,形式化了一阶逻辑推理系统和ZFC公理集合论;之后,开发了数条自动化推理规则证明策略.学生可以在与教科书风格相同的简洁证明环境中使用自动化证明策略完成定理的形式化证明.该工具被用在了大一新生离散数学课程的教学中,没有定理证明经验的学生使用该工具可以快速完成数学归纳法和皮亚诺算术系统等定理的形式化证明,验证了该工具的实际效果.     

Axioms and models of linear logic

Girard's recent system of linear logic is presented in a way that avoids the two-level structure of formulae and sequents, and that minimises the number of primitive function symbols. A deduction theorem is proved concerning the classical implication as embedded in linear logic. The Hilbert-style axiomatisation is proved to be equivalent to the sequent formalism. The axiomatisation leads to a complete class of algebraic models. Various models are exhibited. On the meta-level we use Dijkstra's method of explicit equational proofs.