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.
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. In: G. Bezhanishvili, G. D'Agostino, G. Metcalfe, T. Studer (eds.): Advances in Modal Logic 12, pp. 473-492. College Publications (2018).
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.
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.
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