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.
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.
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.
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.
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.