D. Galmiche and M. Gawek and D. Méry. Beth Semantics and Labelled Deduction for Intuitionistic Sentential Calculus with Identity. 6th International Conference on
Formal Structures for Computation and Deduction, FSCD 2021, Buenos Aires, Argentina, July 2021. PDF
TBI
D. Galmiche and D. Méry. Labelled Cyclic Proofs for Separation Logic. Journal of Logic and Computation, Accepted for publication, 2020. PDF
Separation Logic (SL) is a logical formalism for reasoning about programs that use pointers to mutate data structures. SL has proven itself successful in the field of program verification over the past fifteen years as an assertion language to state properties about memory heaps using Hoare triples. Since the full logic is not recursively enumerable, most of the proof-systems and verification tools for SL focus on the decidable but rather restricted symbolic heaps fragment. Moreover, recent proof-systems that go beyond symbolic heaps allow either the full set of connectives, or the definition of arbitrary predicates, but not both. In this work, we present a labelled proof-system, called GMSL, that allows both the definition of arbitrary inductive predicates and the full set of SL connectives.
D. Galmiche and P. Kimmel and D. Pym. A substructural epistemic resource logic: theory and modelling applications. Journal of Logic and Computation, 29(8): 1251-1287, 2019. PDF
We present a substructural epistemic logic, based on Boolean BI, in which the epistemic modalities are parametrized on agents’ local resources. The new modalities can be seen as generalizations of the usual epistemic modalities. The logic combines Boolean BI’s resource semantics—we introduce BI and its resource semantics at some length—with epistemic agency. We illustrate the use of the logic in systems modelling by discussing some examples about access control, including semaphores, using resource tokens. We also give a labelled tableaux calculus and establish soundness and completeness with respect to the resource semantics.
D. Galmiche and M. Marti and D. Méry. Relating Labelled and Label-free Bunched Calculi in BI logic. In 28th Int. Conference on Automated Reasoning with Analytic
Tableaux and Related Methods, TABLEAUX 2019, LNAI 11714, pages 130-146, London, UK, September 2019. PDF
In this paper we study proof translations between labelled and label-free calculi for the logic of Bunched Implications (BI). We first consider the bunched sequent calculus LBI and define a labelled sequent calculus, called GBI, in which labels and constraints reflect the properties of a specifically tailored Kripke resource semantics of BI with two total resource composition operators and explicit internalization of inconsistency. After showing the soundness of GBI w.r.t. our specific Kripke frames, we show how to translate any LBI-proof into a GBI-proof. Building on the properties of that translation we devise a tree property that every LBI-translated GBI-proof enjoys. We finally show that any GBI-proof enjoying this tree property (and not only LBI-translated ones) can systematically be translated to an LBI-proof.
D. Galmiche and Y. Salhi. Tree-sequent calculi and decision procedures for intuitionistic modal logics. Journal of Logic and Computation, 28(5): 967-989, 2018. PDF
In this article we define label-free sequent calculi for the intuitionistic modal logics obtained from the combinations of the axioms T , B , 4 and 5. These calculi are based on a multi-contextual sequent structure, called Tree-sequent, which allows us to define such calculi for such intuitionistic modal logics. From the calculi defined for the IK , IT , IB4 and ITB logics, we also provide new decision procedures and alternative syntactic proofs of decidability.
B. Lellmann. From Input/Output Logic to Conditional Logics via Sequents - With Provers. Proceedings of Tableaux 2021. PDF
We consider cut-free sequent calculi for a number of deontic logics from the family of Input/Output logics. These sequent calculi provide a correspondence to the flat fragment of certain conditional logics. Two of the introduced calculi are non-standard in that they include non-derivability statements, and hence are interesting also from a purely technical perspective. We further modularise the calculi in an extended sequent framework. Proof search in the extended calculi is implemented in Prolog, providing seemingly the first automated reasoning systems for some of the considered logics.
R. Goré, R. Ramanayake, I. Shillito. Cut-elimination for provability logic by terminating proof search: formalised and deconstructed using Coq. Proceedings of Tableaux 2021. PDF
Recently, Brighton gave another cut-admissibility proof for the standard set-based sequent calculus GLS for modal provability logic GL. One of the two induction measures that Brighton uses is novel: the maximal height of regress trees in an auxiliary calculus called RGL. Tautology elimination is established rather than direct cut-admissibility, and at some points the input derivation appears to be ignored in favour of a derivation obtained by backward proof-search. By formalising the GLS calculus and the proofs in Coq, we show that: (1) the use of the novel measure is problematic under the usual interpretation of the Gentzen comma as set union, and a multiset-based sequent calculus provides a more natural formulation; (2) the detour through tautology elimination is unnecessary; and (3) we can use the same induction argument without regress trees to obtain a direct proof of cut-admissibility that is faithful to the input derivation.
T. Dalmonte, C. Grellois and N. Olivetti. Terminating Calculi and Countermodels for Constructive Modal Logics. Proceedings of Tableaux 2021. PDF
We investigate terminating sequent calculi for constructive modal logics CK and CCDL in the style of Dyckhoff's calculi for intuitionistic logic. We first present strictly terminating calculi for these logics. Our calculi provide immediately a decision procedure for the respective logics and have good proof-theoretical properties, namely they allow for a syntactic proof of cut admissibility. We then present refutation calculi for non-provability in both logics. Their main feature is that they support direct countermodel extraction: ach refutation directly defines a finite countermodel of the refuted formula in a natural neighbourhood semantics for these logics.
T. Lyon. Nested Sequents for Intuitionistic Modal Logics via Structural Refinement. Proceedings of Tableaux 2021. PDF
We employ a recently developed methodology---called "structural refinement"---to extract nested sequent systems for a sizable class of intuitionistic modal logics from their respective labelled sequent systems. This method can be seen as a means by which labelled sequent systems can be transformed into nested sequent systems through the introduction of propagation rules and the elimination of structural rules, followed by a notational translation. The nested systems we obtain incorporate propagation rules that are parameterized with formal grammars, and which encode certain frame conditions expressible as first-order Horn formulae that correspond to a subclass of the Scott-Lemmon axioms. We show that our nested systems are sound, cut-free complete, and admit hp-admissibility of typical structural rules.
A. Ciabattoni, T. Lang, and R. Ramanayake. Bounded sequent calculi and restricted
embeddings: hypersequent logics. Accepted for publication in the Journal of Symbolic Logic. 2021
R. Balasubramanian, T. Lang and R. Ramanayake. Decidability and Complexity in Weakening and Contraction Hypersequent Substructural Logics. LICS 2021. Accepted.
T. Dalmonte, B. Lellmann, N. Olivetti, E. Pimentel. Hypersequent calculi for non-normal modal and deontic logics: Countermodels and optimal complexity. Accepted for publications in the LFCS2020 post-proceedings volume of the Journal of Logic and Computation. PDF
We present some hypersequent calculi for all systems of the classical cube and their extensions with axioms T, P and D and for every n≥1, rule RD+n. The calculi are internal as they only employ the language of the logic, plus additional structural connectives. We show that the calculi are complete with respect to the corresponding axiomatization by a syntactic proof of cut elimination. Then, we define a terminating proof search strategy in the hypersequent calculi and show that it is optimal for coNP-complete logics. Moreover, we show that from every failed proof of a formula or hypersequent it is possible to directly extract a countermodel of it in the bi-neighbourhood semantics of polynomial size for coNP logics, and for regular logics also in the relational semantics. We finish the paper by giving a translation between hypersequent rule applications and derivations in a labelled system for the classical cube.
B. Lellmann, R. Kuznets. Interpolation for Intermediate Logics via Injective Nested Sequents. Accepted for publications to the Special issue of the Journal of Logic and Computation on External and Internal Calculi for Non Classical Logics. PDF
F. Aschieri, A. Ciabattoni, F. A. Genco. On the concurrent computational content of intermediate logics. Theor. Comput. Sci. 813: 375-409 (2020). PDF
We provide a proofs-as-concurrent-programs interpretation for a large class of intermediate logics that can be formalized by cut-free hypersequent calculi. Obtained by adding classical disjunctive tautologies to intuitionistic logic, these logics are used to type concurrent λ-calculi by Curry–Howard correspondence; each of the calculi features a specific communication mechanism, enhanced expressive power when compared to the λ-calculus, and implements forms of code mobility. We thus confirm Avron's 1991 thesis that intermediate logics formalizable by hypersequent calculi can serve as basis for concurrent λ-calculi.
F. Aschieri, A. Ciabattoni, F. A. Genco. A typed parallel lambda calculus via 1-depth intermediate proofs, Proceedings of LPAR 2020.
T. Lyon. On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics. Journal of Logic and Computation (2020). PDF
This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, first-order intuitionistic logic with non-constant domains and first-order intuitionistic logic with constant domains. It is shown that Fitting’s nested calculi naturally arise from their corresponding labelled calculi—for each of the aforementioned logics—via the elimination of structural rules in labelled derivations. The translational correspondence between the two types of systems is leveraged to show that the nested calculi inherit proof-theoretic properties from their associated labelled calculi, such as completeness, invertibility of rules and cut admissibility. Since labelled calculi are easily obtained via a logic’s semantics, the method presented in this paper can be seen as one whereby refined versions of labelled calculi (containing nested calculi as fragments) with favourable properties are derived directly from a logic’s semantics.
T. Dalmonte, C. Grellois, N. Olivetti. Intuitionistic Non-normal Modal Logics: A General Framework. Journal of Philosophical Logic 49(5): 833-882 (2020). PDF
We define a family of intuitionistic non-normal modal logics; they can be seen as intuitionistic counterparts of classical ones.
We first consider monomodal logics, which contain only Necessity or Possibility. We then consider the more important case of bimodal logics,
which contain both modal operators. In this case we define several interactions between Necessity and Possibility of increasing strength,
although weaker than duality. We thereby obtain a lattice of 24 distinct bimodal logics. For all logics we provide both a Hilbert axiomatisation
and a cut-free sequent calculus, on its basis we also prove their decidability.
We then define a semantic characterisation of our logics in terms of neighbourhood models containing two distinct neighbourhood functions corresponding
to the two modalities. Our semantic framework captures modularly not only our systems but also already known intuitionistic non-normal modal logics
such as Constructive K (CK) and the propositional fragment of Wijesekera's Constructive Concurrent Dynamic Logic.
T. Dalmonte, N. Olivetti, G. L. Pozzato. HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description). Proceedings of IJCAR 2020. PDF
We present HYPNO (HYpersequent Prover for NOn-normal modal logics), a Prolog-based theorem prover and countermodel generator for non-normal modal logics.
HYPNO implements some hypersequent calculi recently introduced for the basic system E and its extensions with axioms M, N, and C.
It is inspired by the methodology of Open image in new window, so that it does not make use of any ad-hoc control mechanism. Given a formula,
HYPNO provides either a proof in the calculus or a countermodel, directly built from an open saturated hypersequent.
Preliminary experimental results show that the performances of HYPNO are very promising with respect to other theorem provers for the same class of logics.
T. Dalmonte, C. Grellois, N. Olivetti. Proof systems for the logics of bringing-it-about. Proceedings of DEON 2020. PDF
The logic of Bringing-it-About was introduced by Elgesem to formalise the notions of agency and capability.
It contains two families of modalities indexed by agents,the first one expressing what an agent brings about (does),
and the second express-ing what she can bring about (can do). We first introduce a new neighbourhood semantics,
defined in terms of bi-neighbourhood models for this logic, which is more suited for countermodel construction than the semantics defined in the literature.
We then introduce a hypersequent calculus for this logic, which leads to a decision procedure allowing for a practical countermodel extraction.
We finally extend both the semantics and the calculus to a coalitional version of Elgesem logic proposed by Troquard.
D. Kirst and D. Larchey-Wendling. Trakhtenbrot's Theorem in Coq. Proceedings of IJCAR 2020. PDF
We study finite first-order satisfiability (FSAT) in the constructive setting of dependent type theory. Employing synthetic accounts of enumerability and decidability, we give a full classification of FSAT depending on the first-order signature of non-logical symbols. On the one hand, our development focuses on Trakhtenbrot's theorem, stating that FSAT is undecidable as soon as the signature contains an at least binary relation symbol. Our proof proceeds by a many-one reduction chain starting from the Post correspondence problem. On the other hand, we establish the decidability of FSAT for monadic first-order logic, i.e. where the signature only contains at most unary function and relation symbols, as well as the enumerability of FSAT for arbitrary enumerable signatures. All our results are mechanised in the framework of a growing Coq library of synthetic undecidability proofs.
D. Larchey-Wendling. Constructive Decision via Redundancy-free Proof-Search (extended)
Journal of Automated Reasoning, June 2020. PDF
We give a constructive account of Kripke–Curry’s method which was used to establish the decidability of implicational relevance logic (R→). To sustain our approach, we mechanize this method in axiom-free Coq, abstracting away from the specific features of R→ to keep only the essential ingredients of the technique. In particular we show how to replace Kripke/Dickson’s lemma by a constructive form of Ramsey’s theorem based on the notion of almost full relation. We also explain how to replace König’s lemma with an inductive form of Brouwer’s Fan theorem. We instantiate our abstract proof to get a constructive decision procedure for R→ and discuss potential applications to other logical decidability problems.
K. van Berkel and T. Lyon. The Varieties of Ought-implies-Can and Deontic STIT Logic. Proceedings of DEON 2020. PDF
STIT logic is a prominent framework for the analysis of interactive, multi-agent choicemaking. In the available deontic extensions of STIT, the principle of ought-impliescan (OiC) fulfils a central role. However, in the philosophical literature a variety of
OiC interpretations have been discussed and, in fact, the most prevalent readings
of OiC are either weaker or stronger than the one employed in the traditional STIT
setting. This paper provides a modular framework for deontic STIT that accounts
for a multitude of OiC principles. In particular, we order, discuss and formalize ten
such readings. Furthermore, we indicate how these readings relate to other central
metaethical principles. Last, we provide sound and complete sequent-style calculi for
the various STIT logics accommodating these different OiC principles.
A. Ciabattoni, T. Lyon, R. Ramanayake, and A. Tiu. Display to Labelled Proofs and Back Again for Tense Logics.
ACM Transaction on Computational Logic. PDF
We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense
logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended
with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus.
Concerning the converse translation, we show that for Kt extended with path axioms, every derivation in the
corresponding labeled calculus can be put into a special form that is translatable to a derivation in the associated
display calculus. A key insight in this converse translation is a canonical representation of display sequents as
labeled polytrees. The latter, which represent equivalence classes of display sequents modulo display postulates,
also shed light on related correspondence results for tense logics.
R. Ramanayake. Extended Kripke lemma and decidability for hypersequent substructural logics. Proceedings of LICS 2020. PDF
We establish the decidability of every axiomatic extension of the commutative Full Lambek calculus with contraction FLec that has a cut-free hypersequent calculus. The axioms include familiar properties such as linearity (fuzzy logics) and the substructural versions of bounded width and weak excluded middle. Kripke famously proved the decidability of FLec by combining structural proof theory and combinatorics. This work significantly extends both ingredients: height-preserving admissibility of contraction by internalising a fixed amount of contraction (a Curry's lemma for hypersequent calculi) and an extended Kripke lemma for hypersequents that relies on the componentwise partial order on n-tuples being an \omega^2-well-quasi-order.
T. Dalmonte, B. Lellmann, N. Olivetti, E. Pimentel. Countermodel Construction via Optimal Hypersequent Calculi for Non-normal Modal Logics. Proceedings of LFCS 2020. PDF
We develop semantically-oriented calculi for the cube of non-normal modal logics and some deontic extensions.
The calculi manipulate hypersequents and have a simple semantic interpretation. Their main feature is that they
allow for direct countermodel extraction. Moreover they provide an optimal decision procedure for the respective logics.
They also enjoy standard proof-theoretical properties, such as a syntactical proof of cut-admissibility.
K. van Berkel, T. Lyon, and F. Olivieri. A Decidable Multi-Agent Logic for Reasoning about Actions, Instruments, and Norms.
Proceedings of CLAR 2020. PDF
We formally introduce a novel, yet ubiquitous, category of norms: norms of instrumentality. Norms of this category describe which actions are obligatory, or prohibited, as instruments for certain results. We propose the Logic of Agency and Norms (LAN) that enables reasoning about actions, instrumentality, and normative principles in a multi-agent setting. Leveraging LAN, we formalize norms of instrumentality and compare them to two prevalent norm categories: norms to be and norms to do. Last, we pose principles describing relations between the three categories and evaluate their validity vis-a-vis notions of deliberative acting. On a technical note, the logic will be shown decidable via the finite model property.
T. Lyon. Syntactic Cut-Elimination for Intuitionistic Fuzzy Logic via Linear Nested Sequents.
Proceedings of LFCS 2020. PDF
This paper employs the linear nested sequent framework to design a new cut-free calculus LNIF for intuitionistic fuzzy logic--the first-order Gödel logic characterized by linear relational frames with constant domains. Linear nested sequents--which are nested sequents restricted to linear structures--prove to be a well-suited proof-theoretic formalism for intuitionistic fuzzy logic. We show that the calculus LNIF possesses highly desirable proof-theoretic properties such as invertibility of all rules, admissibility of structural rules, and syntactic cut-elimination.
T. Lyon. On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems.
Proceedings of LFCS 2020. PDF
This paper shows how to derive nested calculi from labelled calculi for propositional intuitionistic logic and first-order intuitionistic logic with constant domains, thus connecting the general results for labelled calculi with the more refined formalism of nested sequents. The extraction of nested calculi from labelled calculi obtains via considerations pertaining to the elimination of structural rules in labelled derivations. Each aspect of the extraction process is motivated and detailed, showing that each nested calculus inherits favorable proof-theoretic properties from its associated labelled calculus.
T. Lyon, A. Tiu, R. Goré, and R. Clouston. Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents.
Proceedings of CSL 2020. PDF
We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a “converse” modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequent calculus, but have all been shown to have cut-free nested sequent calculi. The proof of the interpolation theorem uses these calculi and is purely syntactic, without resorting to embeddings, semantic arguments, or interpreted connectives external to the underlying logical language. A novel feature of our proof includes an orthogonality condition for defining duality between interpolants.
T. Dalmonte, S. Negri, N. Olivetti, G. L. Pozzato. PRONOM: Proof-Search and Countermodel Generation for Non-normal Modal Logics. Proceedings of AI*IA 2019. PDF
We present PRONOM, a theorem prover and countermodel generator for non-normal modal logics.
PRONOM implements some labelled sequent calculi recently introduced for the basic system E and its extensions
with axioms M, N, and C based on bi-neighbourhood semantics. PRONOM is inspired by the methodology of
LeanTAP and is implemented in Prolog. When a modal formula is valid, then PRONOM
computes a proof (a closed tree) in the labelled calculi having that formula as a root in the labelled
calculi, otherwise PRONOM is able to extract a model falsifying it from an open, saturated branch.
The paper shows some experimental results, witnessing that the performances of PRONOM are promising.
T. Lyon and K. van Berkel. Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics.
Proceedings of PRIMA 2019. PDF
This work provides proof-search algorithms and automated counter-model extraction for a class of STIT logics. With this, we answer an open problem concerning syntactic decision procedures and cut-free calculi for STIT logics. A new class of cut-free complete labelled sequent calculi G3LdmL^m_n, for multi-agent STIT with at most n-many choices, is introduced. We refine the calculi G3LdmL^m_n through the use of propagation rules and demonstrate the admissibility of their structural rules, resulting in auxiliary calculi Ldm^m_nL. In the single-agent case, we show that the refined calculi Ldm^m_nL derive theorems within a restricted class of (forestlike) sequents, allowing us to provide proof-search algorithms that decide single-agent STIT logics. We prove that the proof-search algorithms are correct and terminate.
D. Larchey-Wendling and R. Matthes. Certification of Breadth-First Algorithms by Extraction.
Proceedings of MPC 2019. PDF
By using pointers, breadth-first algorithms are very easy to implement efficiently in imperative languages. Implementing them with
the same bounds on execution time in purely functional style can be challenging, as explained in Okasaki’s paper at ICFP 2000 that even restricts the problem to binary trees but considers numbering instead of just traversal. Okasaki’s solution is modular and factors out the problem of implementing queues (FIFOs) with worst-case constant time operations. We certify those FIFO-based breadth-first algorithms on binary trees by extracting them from fully specified Coq terms, given an
axiomatic description of FIFOs. In addition, we axiomatically characterize the strict and total order on branches that captures the nature of breadth-first traversal and propose alternative characterizations of breadth-first traversal of forests. We also propose efficient certified implementations of FIFOs by extraction, either with pairs of lists (with amortized constant time operations) or triples of lazy lists (with worstcase constant time operations), thus getting from extraction certified breadth-first algorithms with the optimal bounds on execution time.
B. Lellmann, E. Pimentel, and R. Ramanayake. Sequentialising Nested Systems.
Proceedings of Tableaux 2019. PDF
In this work, we investigate the proof theoretic connections between sequent and nested proof calculi. Specifically, we identify gen-
eral conditions under which a nested calculus can be transformed into a sequent calculus by restructuring the nested sequent derivation (proof)
and shedding extraneous information to obtain a derivation of the same formula in the sequent calculus. These results are formulated generally
so that they apply to calculi for intuitionistic, normal modal logics and negative modalities.
A. Ciabattoni, T. Lang, and R. Ramanayake. Bounded Sequent Calculi for Non-Classical Logics via Hypersequents.
Proceedings of Tableaux 2019. PDF
Using substructural and modal logics as case studies, a uniform method is presented for transforming cut-free hypersequent proofs
into sequent calculus proofs satisfying relaxations of the subformula property. As a corollary we prove decidability for a large class of commutative
substructural logics with contraction and mingle, and get a simple syntactic proof of a well known result: the sequent calculus for S5 is analytic.
K. van Berkel and T. Lyon. A Neutral Temporal Deontic STIT Logic.
Proceedings of LORI 2019. PDF
In this work we answer a long standing request for temporal embeddings of deontic STIT logics by introducing the multi-agent STIT logic TDS. The logic is based upon atemporal utilitarian STIT logic. Yet, the logic presented here will be neutral: instead of committing ourselves to utilitarian theories, we prove the logic TDS sound and complete with respect to relational frames not employing any utilitarian function. We demonstrate how these neutral frames can be transformed into utilitarian temporal frames, while preserving validity. Last, we discuss problems that arise from employing binary utility functions in a temporal setting.
Y. Forster and D. Larchey-Wendling. Hilbert’s Tenth Problem in Coq.
Proceedings of FSCD 2019. PDF
We formalise the undecidability of solvability of Diophantine equations, i.e. polynomial equations over natural numbers, in Coq’s constructive type theory. To do so, we give the first full mechanisation of the Davis-Putnam-Robinson-Matiyasevich theorem, stating that every recursively enumerable problem – in our case by a Minsky machine – is Diophantine. We obtain an elegant and comprehensible proof by using a synthetic approach to computability and by introducing Conway’s FRACTRAN
language as intermediate layer.
Y. Forster and D. Larchey-Wendling. Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines.
Proceedings of CPP 2019. PDF
We formally prove the undecidability of entailment in intuitionistic linear logic in Coq. We reduce the Post correspondence problem (PCP) via binary stack machines and Minsky machines to intuitionistic linear logic. The reductions rely on several technically involved formalisations, amongst them a binary stack machine simulator for PCP, a verified low-level compiler for instruction-based languages and a soundness proof for intuitionistic linear logic with respect to trivial phase semantics. We exploit the computability of all functions definable in constructive type theory and thus do not have to rely on a concrete model of computation, enabling the reduction proofs to focus on correctness properties.
M. Girlando, B. Lellmann, and N. Olivetti. Nested sequents for the logic of conditional belief.
Proceedings of JELIA 2019. PDF
The logic of conditional belief, called Conditional Doxastic Logic (CDL), was proposed by Board, Baltag and Smets to model revisable belief and knowledge in a multi-agent setting. We present a proof system for CDL in the form of a nested sequent calculus. To the best of our knowledge, ours is the first internal and standard calculus for this logic. We take as as primitive a multi-agent version of the “comparative plausibility operator”, as in Lewis’ counterfactual logic. The calculus is analytic and provides a decision procedure for CDL. As a by-product we also obtain a nested sequent calculus for multi-agent modal logic S5i .
K. van Berkel and T. Lyon. Cut-free Calculi and Relational Semantics for Temporal STIT Logics.
Proceedings of JELIA 2019. PDF
We present cut-free labelled sequent calculi for a central formalism in logics of agency:
STIT logics with temporal operators. These include sequent systems for LDM, TSTIT and XSTIT. All calculi presented possess essential structural properties such as contraction- and cut-admissibility. The labelled calculi G3LDM and G3TSTIT are shown sound and complete relative to irreflexive temporal frames. Additionally, we extend current results by showing that also XSTIT can be characterized through relational frames, omitting the use of BT+AC frames.
R. Ramanayake. Inducing syntactic cut-elimination for indexed nested sequents. Logical Methods in Computer Science 14(4:18), pp. 1-25, 2018. PDF
The key to the proof-theoretic study of a logic is a proof calculus with a subformula property. Many different proof formalisms have been introduced (e.g. sequent, nested sequent, labelled sequent formalisms) in order to provide such calculi for the many logics of interest. The nested sequent formalism was recently generalised to indexed nested sequents in order to yield proof calculi with the subformula property for extensions of the modal logic K by (Lemmon-Scott) Geach axioms. The proofs of completeness and cut-elimination therein were semantic and intricate. Here we show that derivations in the labelled sequent formalism whose sequents are `almost treelike' correspond exactly to indexed nested sequents. This correspondence is exploited to induce syntactic proofs for indexed nested sequent calculi making use of the elegant proofs that exist for the labelled sequent calculi. A larger goal of this work is to demonstrate how specialising existing proof-theoretic transformations alleviate the need for independent proofs in each formalism. Such coercion can also be used to induce new cutfree calculi. We employ this to present the first indexed nested sequent calculi for intermediate logics.
A. Ciabattoni and F. Genco. Hypersequents and Systems of Rules: Embeddings and Applications. ACM Transaction on Computational Logic 19(2), Article 11 (2018). PDF
We define a bi-directional embedding between hypersequent calculi and a subclass of systems of rules (2-
systems). In addition to showing that the two proof frameworks have the same expressive power, the embedding
allows for the recovery of the benefits of locality for 2-systems, analyticity results for a large class of such
systems, and a rewriting of hypersequent rules as natural deduction rules.
A. Ciabattoni, T. Lyon, and R. Ramanayake. From Display to Labelled Proofs for Tense Logics.
Proceedings of LFCS 2018. PDF
We introduce an effective translation from proofs in the display calculus to proofs in the labelled calculus in the context of tense
logics. We identify the labelled calculus proofs in the image of this translation as those built from labelled sequents whose underlying directed graph possesses certain properties. For the minimal normal tense logic Kt,
the image is shown to be the set of all proofs in the labelled calculus G3Kt.
T. Dalmonte, N. Olivetti, and S. Negri. Non-normal modal logics: bi-neighbourhood semantics and its labelled calculi.
Proceedings of AIML 2018. PDF
The classical cube of non-normal modal logics is considered, and an alternative neighbourhood semantics is given in which worlds are equipped with sets of pairs of neighbourhoods. The intuition is that the two neighbourhoods of a pair provide independent positive and negative evidence (or support) for a formula. This bi-neighbourhood semantics is significant in particular for logics without the monotonicity property. It is shown that this semantics characterises the cube of non-normal modal logics and that there is a mutual correspondence between models in the standard and in the bi-neighbourhood semantics. On the basis of this alternative semantics, labelled sequent calculi are developed for all the logics of the classical cube. The calculi thus obtained are fully modular and have good structural properties, first of all, syntactic cut elimination. Moreover, they provide a decision procedure and an easy countermodel extraction, both in the bi-neighbourhood and in the standard semantics.
D. Galmiche, M. Marti and D. Méry. Proof Translations in BI Logic - extended abstract. 1st Int. Workshop on External and Internal Calculi for Non-Classical Logics, EICNCL 2018, Oxford, UK, July 2018. PDF
In order to study proof translations in BI logic, we consider first the bunched
sequent calculus LBI and then define a new labelled sequent calculus, called GBI. We
propose a procedure that translates LBI proofs into GBI proofs and prove its soundness.
Moreover we discuss some steps towards the reverse translation of GBI proofs into LBI
proofs and propose an algorithm that is illustrated by some examples. Further work will
be devoted to its correctness and also to the design of translations of LBI proofs to TBI
(labelled-tableaux) proofs.
D. Galmiche and D. Méry. Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic. 3rd Int. Workshop on Automated Reasoning in Quantified Non-Classical Logics, ARQNL 2018, Oxford, UK, July 2018. PDF
We propose a connection-based characterization for multiplicative intuitionistic linear
logic (MILL) which is based on labels and constraints that capture Urquhart's possible
world semantics of the logic. We first briefly recall the purely syntactic sequent calculus
for MILL, which we call LMILL. Then, in the spirit of our previous results on the Logic
of Bunched Implications (BI), we present a connection-based characterization of MILL
provability. We show its soundness and completeness without the need for any notion of
multiplicity. From the characterization, we finally propose a labelled sequent calculus for
MILL.
D. Galmiche and D. Méry. Labelled Cyclic Proofs for Separation Logic. 1st Int. Workshop on Automated Deduction for Separation
Logic, ADSL 2018, Oxford, UK, July 2018. PDF
Separation Logic (SL) is a logical formalism for reasoning
about programs that use pointers to mutate data structures. SL has
proven itself successful in the field of program verification over the past
fifteen years as an assertion language to state properties about memory
heaps using Hoare triples. Since the full logic is not recursively enumerable,
most of the proof-systems and verification tools for SL focus on
the decidable but rather restricted symbolic heaps fragment. Moreover,
recent proof-systems that go beyond symbolic heaps allow either the full
set of connectives, or the definition of arbitrary predicates, but not both.
In this work, we present a labelled proof-system called GMSL that allows
both the definition of arbitrary inductive predicates and the full set of
SL connectives.
M. Girlando, S. Negri, and N. Olivetti. Counterfactual logic: labelled and internal calculi, two sides of the same coin?
Proceedings of AIML 2018. PDF
Lewis’ Logic V is the fundamental logic of counterfactuals. Its proof theory is here
investigated by means of two sequent calculi based on the connective of comparative
plausibility. First, a labelled calculus is defined on the basis of Lewis’ sphere semantics. This calculus has good structural properties and provides a decision procedure
for the logic. An internal calculus, recently introduced, is then considered. In this
calculus, each sequent in a derivation can be interpreted directly as a formula of V. In
spite of the fundamental difference between the two calculi, a mutual correspondence
between them can be established in a constructive way. In one direction, it is shown
that any derivation of the internal calculus can be translated into a derivation in the
labelled calculus. The opposite direction is considerably more difficult, as the labelled
calculus comprises rules which cannot be encoded by purely logical rules. However,
by restricting to derivations in normal form, derivations in the labelled calculus can
be mapped into derivations in the internal calculus. On a general level, these results
aim to contribute to the understanding of the relations between labelled and internal
proof systems for logics belonging to the realm of modal logic and its extensions, a
topic still relatively unexplored.
M. J. Gouveia, L. Santocanale. Mix * -autonomous quantales and the continuous weak order, 2018, to appear in the proceedings of the conference RAMICS 2018. PDF
The set of permutations on a finite set can be given a lattice structure (known as the weak Bruhat order). The lattice structure is generalized to the set of words on a fixed alphabet Σ= {x,y,z,...}, where each letter has a fixed number of occurrences (these lattices are known as multinomial lattices and, in dimension 2, as lattices of lattice paths). By interpreting the letters x,y,z,... as axes, these words can be interpreted as discrete increasing paths on a grid of a d-dimensional cube, where d = card(Σ). We show in this paper how to extend this order to images of continuous monotone paths images of monotone functions from the unit interval to a d-dimensional cube. The key tool used to realize this construction is the quantale LV(I) of join-continuos functions from the unit interval to itself; the construction relies on a few algebraic properties of this quantale: it is star-autonomous and it satisfies the mix rule. We begin developing a structural theory of these lattices by characterizing join-irreducible elements, and by proving these lattices are generated from their join-irreducible elements under infinite joins.
R. Kuznets and B. Lellmann. Interpolation for Intermediate Logics via Hyper- and Linear Nested Sequents. Proceedings of AIML 2018. PDF
The goal of this paper is extending to intermediate logics the constructive
proof-theoretic method of proving Craig and Lyndon interpolation via hypersequents and
nested sequents developed earlier for classical modal logics. While both Jankov and
Gödel logics possess hypersequent systems, we show that our method can only be
applied to the former. To tackle the latter, we switch to linear nested sequents,
demonstrate syntactic cut elimination for them, and use it to prove interpolation for
Gödel logic. Thereby, we answer in the positive the open question of whether Gödel
logic enjoys the Lyndon interpolation property.
D. Larchey-Wendling. Constructive Decision via Redundancy-free Proof-Search. Proceedings of IJCAR 2018. PDF
We give a constructive account of Kripke-Curry’s method
which was used to establish the decidability of Implicational Relevance
Logic (R→). To sustain our approach, we mechanize this method in
axiom-free Coq, abstracting away from the specific features of R→ to
keep only the essential ingredients of the technique. In particular we
show how to replace Kripke/Dickson’s lemma by a constructive form of
Ramsey’s theorem based on the notion of almost full relation. We also explain
how to replace König’s lemma with an inductive form of Brouwer’s
Fan theorem. We instantiate our abstract proof to get a constructive
decision procedure for R→ and discuss potential applications to other
logical decidability problems.
D. Larchey-Wendling. Proof Pearl: Constructive Extraction of Cycle Finding Algorithms. Proceedings of ITP 2018. PDF
We present a short implementation of the well-known Tortoise and Hare cycle finding algorithm in the constructive setting of Coq.
This algorithm is interesting from a constructive perspective because it is both very simple and potentially non-terminating (depending on the input). To overcome potential non-termination, we encode the given termination argument (there exists a cycle) into a bar inductive predicate that we use as termination certificate. From this development, we extract the standard OCaml implementation of this algorithm. We generalize the method to the full Floyd’s algorithm that computes the entry point and the period of the cycle in the iterated sequence, and to the more efficient Brent’s algorithm for computing the period only, again with accurate extractions of their respective standard OCaml implementations.
M. Marti and T. Studer. The internalized Disjunction Property for Intuitionistic Justification Logic. Proceedings of AIML 2018. PDF
In intuitionistic justification logic, evidence terms represent intuitionistic proofs, that
is a formula r:A means r is an intuitionistic proof of A. A natural principle in this
context is the internalized disjunction property (IDP), which is: for each term r there
exists a term s such that r:(A or B) implies s:A or s:B.
We introduce a light extension of iJT4, in which IDP is valid. Our proof relies on
a model construction that enforces sharp evidence relations and a tight connection
between syntax and semantics. This makes it possible to switch between proofs and
models, which will be the key to proving IDP.
L. Santocanale. The equational theory of the natural join and inner union is decidable, in: C. Baier, U. D. Lago (eds.), Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018. Proceedings, vol. 10803 of Lecture Notes in Computer Science, Springer, 2018, pp. 494--510. PDF
The natural join and the inner union operations combine relations of a database. Tropashko and Spight realized that these two operations are the meet and join operations in a class of lattices, known by now as the relational lattices. They proposed then lattice theory as an algebraic approach to the theory of databases, alternative to the relational algebra. Previous works proved that the quasiequational theory of these lattices—that is, the set of definite Horn sentences valid in all the relational lattices—is undecidable, even when the signature is restricted to the pure lattice signature. We prove here that the equational theory of relational lattices is decidable. That, is we provide an algorithm to decide if two lattice theoretic terms t, s are made equal under all intepretations in some relational lattice. We achieve this goal by showing that if an inclusion t ≤ s fails in any of these lattices, then it fails in a relational lattice whose size is bound by a triple exponential function of the sizes of t and s.
A. Ciabattoni and R. Ramanayake. Bunched Hypersequent Calculi for Distributive Substructural Logics.
Proceedings of LPAR 2017. PDF
We introduce a new proof-theoretic framework which enhances the expressive power of bunched sequents by extending them with a hypersequent structure.
A general cut-elimination theorem that applies to bunched hypersequent calculi satisfying general rule conditions is then proved. We adapt the methods of transforming axioms into rules to provide cutfree bunched hypersequent calculi for a large class of logics extending the distributive commutative Full Lambek calculus and Bunched Implication logic BI. The methodology is then used to formulate new logics equipped with a cutfree calculus in the vicinity of Boolean BI.
J. R. Courtault and H. van Ditmarsch and D. Galmiche. A Public Announcement Separation Logic. Mathematical Structures in Computer Science, 29(6):828-871, 2019. PDF
We define a Public Announcement Separation Logic, denoted PASL, that allows us to consider
epistemic possible worlds as resources that can be shared or separated, in the spirit of separation
logics. After studying its semantics and illustrating its interest for modelling systems, we provide a
sound and complete tableau calculus that deals with resource, agent and announcement constraints
and give also a countermodel extraction method.
M. Girlando, B. Lellmann, N. Olivetti, and G.L. Pozzato. Hypersequent Calculi for Lewis’ Conditional Logics with Uniformity and Reflexivity. Proceedings of Tableaux 2017. PDF
We present the first internal calculi for Lewis’ conditional logics characterized by uniformity and reflexivity, including non-standard internal hypersequent calculi for a number of extensions of the logic VTU. These calculi allow for syntactic proofs of cut elimination and known connections to S5. We then introduce standard internal hypersequent calculi for all these logics, in which sequents are enriched by additional structures to encode plausibility formulas as well as diamond formulas. These calculi provide both a decision procedure for the respective logics and constructive countermodel extraction from a failed proof search attempt.
M. Girlando, B. Lellmann, N. Olivetti, G.L. Pozzato, and Q. Vitalis. VINTE: an Implementation of Internal Calculi for Lewis’ Logics of Counterfactual Reasoning. Proceedings of Tableaux 2017. PDF
We present VINTE, a theorem prover for conditional logics for counterfactual reasoning introduced by Lewis in the seventies. VINTE implements some internal calculi recently introduced for the basic system V and some of its signicant extensions with axioms N, T, C, W and A. VINTE is inspired by the methodology of leanTAP and it is implemented in Prolog. The paper shows some experimental results, witnessing that the performances of VINTE are promising.
D. Larchey-Wendling. Typing Total Recursive Functions in Coq*. Proceedings of ITP 2017. PDF
We present a (relatively) short mechanized proof that Coq
types any recursive function which is provably total in Coq. The wellfounded
(and terminating) induction scheme, which is the foundation of
Coq recursion, is maximal. We implement an unbounded minimization
scheme for decidable predicates. It can also be used to reify a whole category
of undecidable predicates. This development is purely constructive
and requires no axiom. Hence it can be integrated into any project that
might assume additional axioms.
Software
HYPNO: A theorem prover for Non-Normal Modal Logics based on Hypersequent Calculi
PRONOM: A theorem Prover for Non-Normal Modal Logic based on Labelled Calculi
VINTE: A theorem prover for Lewis' logics for counterfactual reasoning
iiProve. A prover for intermediate logics using nested sequents