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