The first algorithm to transform a proof in Nishimura's sequent calculus GKt for tense logic Kt into an analytic proof of the same sequent is presented. In an analytic proof, every rule instance is analytic i.e., each formula in every premise is a subformula of some formula in its conclusion. We call this algorithm analytic restriction to convey that it extends analytic cut-restriction where just the cut-rule instances are made analytic. This distinction is essential in tense logic since cut and modal rules can both cause non-analyticity. Analytic cut-restriction is itself an extension of cut-elimination so our work contributes to a broader program of transforming arbitrary sequent proofs into ones constructed from a designated set of formulas-not necessarily subformulas. As with cut-elimination, the aim is to limit the proof search space and support proof-theoretic and meta-logical investigations.
We present the logic IBV, which is an intuitionistic version of BV, in the sense that its restriction to the MLL connectives is exactly IMLL, the intuitionistic version of MLL. For this logic we give a deep inference proof system and show cut elimination. We also show that the logic obtained from IBV by dropping the associativity of the new non-commutative seq-connective is an intuitionistic variant of the recently introduced logic NML. For this logic, called INML, we give a cut-free sequent calculus.
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.
We present an intuitionistic counterpart of the modal μ -calculus formulated with the binary Lewis arrow, a generalisation of the -operator. Using Ruitenburg’s theorem, we prove that every formula is equivalent to a guarded one. We then provide a sound and complete non-wellfounded proof system for the logic that is cut-free, and obtain as a corollary that the logic is decidable and admits a cyclic proof system. A game semantics for the logic is developed which acts as a mediator between the formal proof system and the relational semantics.
Justification logic is an explication of modal logic: boxes are replaced with proof terms formally through realisation theorems. This can be achieved syntactically using a cut-free proof system for a modal logic, e.g., using sequent, hypersequent, or nested sequent calculi. In constructive modal logic, boxes and diamonds are decoupled and not De Morgan dual. Previous work provides a justification counterpart to constructive modal logic (and some extensions) by making diamonds explicit and introducing new terms called satisfiers. We continue this line of work and provide a justification counterpart to intuitionistic modal logic and its extensions with the and axioms. We extend the syntax of proof terms to accommodate the additional axioms of intuitionistic modal logic and provide an axiomatisation of these justification logics with a syntactic realisation procedure using a cut-free nested sequent system for intuitionistic modal logic.
