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.
Levesque and Lakemeyer proposed a logic called ℒ as a first-order logic for knowledge representation and reasoning in knowledge-based systems. A characteristic feature of this logic is that it uses a countably infinite set of what are called standard names, which are syntactically treated like constants, but which are also isomorphic to a fixed universe of discourse. Quantifiers in ℒ are then given a substitutional interpretation. This non-standard semantics not only simplifies the proofs for certain meta-theoretic properties, but is also exploited in dedicated reasoning procedures for modal extensions of ℒ that include notions of belief, actions, time, and more. However, the only sound and complete proof system provided for ℒ so far is a Hilbert-style axiom system, as well as an iterative reasoning mechanism based on resolution and clause subsumption. In this paper, we present a tableau system for ℒ , and show its soundness and completeness. Completeness is proved first by reduction to the existing axiom system, and involves the cut rule, and then via Hintikka sets, which does not require the cut rule.
This paper considers the bi-modal logic with both and arising from Kripke models with crisp accessibility whose propositions are valued over the standard Gödel algebra [0, 1]. Since this logic lacks the finite model property, we study the logic GW^c relying on witnessed Kripke models where, for each modal formula, there is an assignment where the formula without the modality takes the same value as the modal one. We provide a cut-free sequent calculus and we exploit it to prove that GW^c is decidable and meets the finite model property. Finally, we explore a connection between the witnessed models and the well-known bi-relational Kripke semantics.
We provide a simple cut elimination proof for the interpretability logic of . To achieve this, we introduce a traditional Gentzen-style sequent calculus for and a non-wellfounded version of it. The non-wellfounded calculus makes it possible to avoid diagonal formulas. Hence, we can give a simple argument based on a general proof-theoretic method for calculi of this kind. Our results provide a useful basis for further research; in particular, they will allow us to establish uniform interpolation for .
We consider a family of non-classical three-valued logics proposed to model indicative conditionals in natural language. Among these, systems introduced by B. De Finetti, W.S. Cooper, J. Cantwell and R.J. Farrell, as well as some variants that have not appeared in the literature, but seem nevertheless to be natural objects of interest from a formal point of view. Most of these logics are not easily treatable with the standard techniques of algebraic logic. We therefore resort to non-deterministic structures and multiple-conclusion calculi to provide alternative semantical characterizations and axiomatizations. In the best cases-logics given by a finite monadic matrix-this can be done directly, in a modular way, through a procedure due to Shoesmith and Smiley. In the more involved ones-logics preserving degrees of truth-some ingenuity and more sophisticated techniques are required. We characterize these logics by a partial non-deterministic matrix, and show how to produce analytic (and effective) calculi that are complete with respect to this generalized semantics. In all cases, the calculi thus obtained can be straightforwardly converted, by a uniform procedure, into traditional single-conclusion Hilbert-style axiomatizations.
We consider intuitionistic multimodal logics with modalities satisfying axiom K and the axiom of Necessity, as well as collections of axioms for transforming, removing and splitting modalities, specified by a relation between modalities and sequences of modalities. These axioms can be used for systems of knowledge and belief, describing multiple environments of truth and their awareness of each other. We extend Gentzen's decidable cut-free calculus to accommodate such multimodal systems, using a modal shift operation on contexts to extend the cut elimination proof in a novel way. We then adapt the inverse method to formulate a correct and complete forward proof search for these logics, which can be interpreted in a Fitch-style manner. Proof derivation is streamlined by implementing most derivations using the cut rule. The resulting proof search allows for making multiple queries, building a database of assumptions and their consequences which can be fine-tuned and updated to fit an application.
Commonly used proof strategies by automated reasoners organise proof search either by ordering-based saturation or by reducing goals to subgoals. In this paper, we combine these two approaches and advocate a SAT-based method with symmetry breaking for connection calculi in first-order logic, with the purpose of further pushing the automation in first-order classical logic proofs. In contrast to classical ways of reducing first-order logic to propositional logic, our method encodes the structure of the proof search itself. We present three distinct SAT encodings for connection calculi, analyse their theoretical properties, and discuss the effect of using SAT/SMT solvers on these encodings. We implemented our work in the new solver upCoP and showcase its practical feasibility.
This paper presents a formalization of the nonassociative Lambek calculus in the Agda proof assistant. The sequent calculus for this logic has sequents with binary trees as antecedents, in which formulae are stored as leaves. The shape of the antecedents creates subtleties when proving logical properties, since in many cases one needs to analyze equalities involving sequentially-composed trees. We formally characterize these equalities and show how to employ the resulting technical lemma to prove cut admissibility and the Maehara interpolation properly, which implies Craig interpolation. We show that both the cut rule and the interpolation procedure are well-defined wrt. a certain notion of equivalence of derivations. We additionally prove a proof-relevant version of Maehara interpolation, exhibiting the interpolation procedure as a right inverse of the admissible cut rule.
We present a new approach for solving string equations as extensions of Nielsen transformations. Key to our work are the combination of three techniques: a power operator for strings; generalisations of Parikh images; and equality decomposition. Using these methods allows us to solve complex string equations, including less commonly encountered SMT inputs over strings.
The proof theory and semantics of intuitionistic modal logics have been studied by Simpson in terms of Prawitz-style labelled natural deduction systems and Kripke models. An alternative to model-theoretic semantics is provided by proof-theoretic semantics, which is a logical realization of inferentialism, in which the meaning of constructs is understood through their use. The key idea in proof-theoretic semantics is that of a base of atomic rules, all of which refer only to propositional atoms and involve no logical connectives. A specific form of proof-theoretic semantics, known as base-extension semantics (B-eS), is concerned with the validity of formulae and provides a direct counterpart to Kripke models that is grounded in the provability of atomic formulae in a base. We establish, systematically, B-eS for Simpson's intuitionistic modal logics and, also systematically, obtain soundness and completeness theorems with respect to Simpson's natural deduction systems.
We investigate the systematic development of refined tableau systems for a subset of the logics of confluence, which are modal logics comprising of instances of the Scott-Lemmon axioms. In particular, we look at rule refinements aiming to decrease branching, perform fewer inferences and reduce the application of rules which create new labels in the tableau. Propagation rules are common forms of refined rules, that construct smaller pre-models sufficient to determine satisfiability, without needing to construct full concrete models satisfying the correspondence properties which would require a lot more inference steps. These rules have already been developed for the confluence logics that are part of the modal logic cube, but are lacking for some instances outside the cube. Such instances can be awkward, as the nature of their correspondence properties makes the development of propagation rules particularly challenging. These are the logics KG0111, KG and KDe for which we propose refined tableau systems. We also present refined tableau systems for the combined logics Kalt1De, KBG0111 and KDDe. Soundness and completeness results for all the systems are established.
Proof search in non-confluent tableau calculi, such as the connection tableau calculus, suffers from excess backtracking, but simple restrictions on backtracking are incomplete. We adopt constraint learning to reduce backtracking in the classical first-order connection calculus, while retaining completeness. An initial constraint learning language for connection-driven search is iteratively refined to greatly reduce backtracking in practice. The approach may be useful for proof search in other non-confluent tableau calculi.
We extend the mono-modal CEGAR-tableaux of Goré and Kikkert to normal multi-modal logic K_n with global assumptions. We then extend these CEGAR-tableaux to multi-modal tense logic Kt_n without global assumptions by “compiling in” the residuation conditions between “future” and “past” modalities. Our new implementation CEGARBox++ uses C^++ and includes multiple optimisations which speed up proof-search. is the best satisfiability-checker for mono-modal tense logic Kt_1 but is not competitive for global assumptions.
Converse PDL is the extension of propositional dynamic logic with a converse operation on programs. Our main result states that Converse PDL enjoys the (local) Craig Interpolation Property, with respect to both atomic programs and propositional variables. As a corollary we establish the Beth Definability Property for the logic. Our interpolation proof is based on an adaptation of Maehara's proof-theoretic method. For this purpose we introduce a sound and complete cyclic sequent system for this logic. This calculus features an analytic cut rule and uses a focus mechanism for recognising successful cycles.
We present a non-deterministic semantic framework for all modal logics in the modal cube, extending prior works by Kearns and others. Our approach introduces modular and uniform multi-valued non-deterministic matrices (Nmatrices) for each logic, where necessitation is captured by the systematic use of level valuations. The semantics is grounded in an eight-valued system and provides a sound and complete decision procedure for each modal logic, extending and refining earlier semantics as particular cases. Additionally, we propose a novel model-theoretic perspective that links our framework to relational (Kripke-style) semantics, addressing longstanding questions regarding the correspondence between modal axioms and semantic conditions in non-deterministic settings. This yields a philosophically robust and technically modular alternative to traditional possible-world semantics.
Propositional inquisitive logic is the limit of its n-bounded approximations. In the predicate setting, however, this does not hold anymore, as discovered by Ciardelli and Grilletti [11], who also found complete axiomatizations of n-bounded inquisitive logics _n , for every fixed n. We introduce cut-free labelled sequent calculi for these logics. We illustrate the intricacies of schematic validity in such systems by showing that the well-known Casari formula is atomically valid in (a weak sublogic of) predicate inquisitive logic , fails to be schematically valid in it, and yet is schematically valid under the finite boundedness assumption. The derivations in our calculi, however, are guaranteed to be schematically valid whenever a single specific rule is not used.
