Abstract Treating syntactic equality as a logical connective—governed by left- and right-introduction rules within the sequent calculus—offers an elegant and powerful approach to term identity. This treatment of equality allows for the derivation of core mathematical principles, such as Peano’s axioms (excluding induction), and serves as a foundation for the Abella interactive proof assistant. However, integrating this equality into automated proof search remains challenging. We present a proof search procedure that extends unification to handle the complexities of quantifier alternation and equations that occur in both positive and negative occurrences. While established logical frameworks such as $$\lambda $$ λ Prolog and LF lack direct support for this kind of equality, our procedure enables a lightweight logical framework that addresses this gap. Our system enables unification-aware proof search across a diverse range of first-order sequent calculi that can directly use this form of equality.

Abstract We present a proof-theoretic treatment of forward chaining and saturation within a multisorted, first-order intuitionistic logic with equality. The notions of polarity and focused proofs are central to our approach since they provide a characterization of geometric implications as bipolar formulas as well as a natural setting to describe forward chaining and the concept of productive proofs . We identify conditions under which forward chaining with a given set of formulas is guaranteed to saturate in a finite number of steps. The motivation for this research stems, in part, from exploring avenues to automate the Abella theorem prover, which relies on relational specifications, and where theorems in typical proof developments are essentially bipolar formulas. We illustrate the potential benefits of automating forward chaining and saturation for Abella by presenting examples that compute congruence closure and assist in other equational and relational reasoning tasks.

Abstract Subformula linking is an interactive theorem proving technique that was initially proposed for (classical) linear logic. It is based on truth and context preserving rewrites of a conjecture that are triggered by a user indicatinglinksbetween subformulas, which can be done by direct manipulation, without the need of tactics or proof languages. The system guarantees that a true conjecture can always be rewritten to a known, usually trivial, theorem. In this work, we extend subformula linking to intuitionistic first-order logic with simply typed lambda-terms as the term language of this logic. We then use a well known embedding of intuitionistic type theory into this logic to demonstrate one way to extend linking to type theory.

When presented with a formula to prove, most theorem provers for classical first-order logic process that formula following several steps, one of which is commonly called skolemization. That process eliminates quantifier alternation within formulas by extending the language of the underlying logic with new Skolem functions and by instantiating certain quantifiers with terms built using Skolem functions. In this paper, we address the problem of checking (i.e., certifying) proof evidence that involves Skolem terms. Our goal is to do such certification without using the mathematical concepts of model-theoretic semantics (i.e., preservation of satisfiability) and choice principles (i.e., epsilon terms). Instead, our proof checking kernel is an implementation of Gentzen's sequent calculus, which directly supports quantifier alternation by using eigenvariables. We shall describe deskolemization as a mapping from client-side terms, used in proofs generated by theorem provers, into kernel-side terms, used within our proof checking kernel. This mapping which associates skolemized terms to eigenvariables relies on using outer skolemization. We also point out that the removal of Skolem terms from a proof is influenced by the polarities given to propositional connectives.

HyLL (Hybrid Linear Logic) is an extension of intuitionistic linear logic (ILL) that has been used as a framework for specifying systems that exhibit certain modalities. In HyLL, truth judgements are labelled by worlds (having a monoidal structure) and hybrid connectives (at and ↓) relate worlds with formulas. We start this work by showing that HyLL's axioms and rules can be adequately encoded in linear logic (LL), so that one focused step in LL will correspond to a step of derivation in HyLL. This shows that any proof in HyLL can be exactly mimicked by a LL focused derivation. Another extension of LL that has extensively been used for specifying systems with modalities is Subexponential Linear Logic (SELL). In SELL, the LL exponentials (!, ?) are decorated with labels representing locations, and a pre-order on such labels defines the provability relation. We propose an encoding of HyLL into SELL⋒ (SELL plus quantification over locations) that gives better insights about the meaning of worlds in HyLL. More precisely, we identify worlds as locations, and show that a flat subexponential structure is sufficient for representing any world structure in HyLL. This shows that HyLL's monoidal structure is not reflected in LL derivations, hence not increasing the expressiveness of LL, from a proof theoretical point of view. We conclude by proposing the notion of fixed points in multiplicative additive HyLL (μHyMALL), which can be encoded into multiplicative additive linear logic with fixed points (μMALL). As an application, we propose encodings of Computational Tree Logic (CTL) into both μMALL and μHyMALL. In the former, states are represented as atoms in the linear context, hence reflecting a more operational view of CTL connectives. In the latter, worlds represent states of the transition system, thus exhibiting a pleasant similarity with the semantics of CTL.

Lambda-tree syntax (λTS), also known as higher-order abstract syntax (HOAS), is a representational technique where the pure λ-calculus in a meta-language is used to represent binding constructs in an object language. A key feature of λTS is that capture-avoiding substitution in the object language is represented by β-reduction in the meta language. However, to reason about the meta-theory of (simultaneous) substitutions, it may seem that λTS gets in the way: not only does iterated β-reduction not capture simultaneity, but also β-redexes are not first-class constructs.

Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design and implementation and their use in reasoning tasks ranging from the correctness of software to the properties of formal computational systems have been the focus of considerable research over the last two decades.

Subexponential logic is a variant of linear logic with a family of exponential connectives – called subexponentials – that are indexed and arranged in a pre-order. Each subexponential has or lacks associated structural properties of weakening and contraction. We show that a classical propositional multiplicative subexponential logic (MSEL) with one unrestricted and two linear subexponentials can encode the halting problem for two register Minsky machines, and is hence undecidable. We then show how the additive connectives can be directly simulated by giving an encoding of propositional multiplicative additive linear logic (MALL) in an MSEL with one unrestricted and four linear subexponentials.

The sequent calculus is often criticized for requiring proofs to contain large amounts of low-level syntactic details that can obscure the essence of a given proof. Because each inference rule introduces only a single connective, sequent proofs can separate closely related steps—such as instantiating a block of quantifiers—by irrelevant noise. Moreover, the sequential nature of sequent proofs forces proof steps that are syntactically non-interfering and permutable to nevertheless be written in some arbitrary order. The sequent calculus thus lacks a notion of canonicity : proofs that should be considered essentially the same may not have a common syntactic form. To fix this problem, many researchers have proposed replacing the sequent calculus with proof structures that are more parallel or geometric. Proof-nets, matings and atomic flows are examples of such revolutionary formalizms. We propose, instead, an evolutionary approach to recover canonicity within the sequent calculus, which we illustrate for classical first-order logic. The essential element of our approach is the use of a multi-focused sequent calculus as the means for abstracting away low-level details from classical cut-free sequent proofs. We show that, among the multi-focused proofs, the maximally multi-focused proofs that collect together all possible parallel foci are canonical. Moreover, if we start with a certain focused sequent proof system, such proofs are isomorphic to expansion proofs —a well known, minimalistic and parallel generalization of Herbrand disjunctions—for classical first-order logic. This technique appears to be a systematic way to recover the ‘essence of proof’ from within sequent calculus proofs.

Bisimilarity of two processes is formally established by producing a bisimulation relation that contains those two processes and obeys certain closure properties. In many situations, particularly when the underlying labeled transition system is unbounded, these bisimulation relations can be large and even infinite. The bisimulation-up-to technique has been developed to reduce the size of the relations being computed while retaining soundness, that is, the guarantee of the existence of a bisimulation. Such techniques are increasingly becoming a critical ingredient in the automated checking of bisimilarity. This paper is devoted to the formalization of the meta theory of several major bisimulation-up-to techniques for the process calculi CCS and the π-calculus (with replication). Our formalization is based on recent work on the proof theory of least and greatest fixpoints, particularly the use of relations defined (co-)inductively, and of co-inductive proofs about such relations, as implemented in the Abella theorem prover. An important feature of our formalization is that our definitions of the bisimulation-up-to relations are, in most cases, straightforward translations of published informal definitions, and our proofs clarify several technical details of the informal descriptions. Since the logic behind Abella also supports λ-tree syntax and generic reasoning using the ∇-quantifier, our treatment of the λ-calculus is both direct and natural.

The two-level logic approach (2LL) to reasoning about computational specifications, as implemented by the Abella theorem prover, represents derivations of a specification language as an inductive definition in a reasoning logic. This approach has traditionally been formulated with the specification and reasoning logics having the same type system, and only the formulas being translated. However, requiring identical type systems limits the approach in two important ways: (1) every change in the specification language's type system requires a corresponding change in that of the reasoning logic, and (2) the same reasoning logic cannot be used with two specification languages at once if they have incompatible type systems. We propose a technique based on adequate encodings of the types and judgements of a typed specification language in terms of a simply typed higher-order logic program, which is then used for reasoning about the specification language in the usual 2LL. Moreover, a single specification logic implementation can be used as a basis for a number of other specification languages just by varying the encoding. We illustrate our technique with an implementation of the LF dependent type theory as a new specification language for Abella, co-existing with its current simply typed higher-order hereditary Harrop specification logic, without modifying the type system of its reasoning logic.

The logic of hereditary Harrop formulas (HH) has proven useful for specifying a wide range of formal systems that are commonly presented via syntax-directed rules that make use of contexts and side-conditions. The two-level logic approach, as implemented in the Abella theorem prover, embeds the HH specification logic within a rich reasoning logic that supports inductive and co-inductive definitions, an equality predicate, and generic quantification. Properties of the encoded systems can then be proved through the embedding, with special benefit being extracted from the transparent correspondence between HH derivations and those in the encoded formal systems. The versatility of HH relies on the free use of nested implications, leading to dynamically changing assumption sets in derivations. Realizing an induction principle in this situation is nontrivial and the original Abella system uses only a subset of HH for this reason. We develop a method here for supporting inductive reasoning over all of HH. Our approach relies on the ability to characterize dynamically changing contexts through finite inductive definitions, and on a modified encoding of backchaining for HH that allows these finite characterizations to be used in inductive arguments. We demonstrate the effectiveness of our approach through examples of formal reasoning on specifications with nested implications in an extended version of Abella.