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, 2017, to appear. 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
VINTE: A theorem prover for Lewis' logics for counterfactual reasoning
iiProve. A prover for intermediate logics using nested sequents