ABSTRACT. We present CEGAR-Tableaux, a tableaux-like method for propositional modal logics utilising SAT-solvers, modal clause-learning and multiple optimisations from modal and description logic tableaux calculi. We use the standard Counter-example Guided Abstract Refinement (CEGAR) strategy for SAT-solvers to mimic a tableau-like search strategy that explores a rooted tree-model with the classical propositional logic part of each Kripke world evaluated using a SAT-solver. Unlike modal encodings into SAT-solvers and modal resolution methods, we do not explicitly represent the accessibility relation but track it implicitly via recursion. By using ``satisfiability under unit assumptions'', we can iterate rather than ``backtrack'' over the satisfiable diamonds at the same modal level (context) of the tree model with one SAT-solver. By keeping modal contexts separate from one another, we add further refinements for reflexivity and transitivity which manipulate modal contexts once only. Our solver CEGARBox is, overall, the best for modal logics K, KT and S4 over the standard benchmarks, sometimes by orders of magnitude. It can now also handle all of the 15 logics in the modal cube as well as multimodal tense logic K_t(n) (AKA description logic ALCI). We believe that in the future, all tableaux calculi implementations will use CEGAR-Tableaux.

ABSTRACT. This paper introduces the logics of super-strict implications that are based on C.I. Lewis' non-normal modal logics $S2$ and $S3$. The semantics of these logics is based on Kripke's semantics for non-normal logics. This solves a question we left open in a previous paper by showing that these logics are connexive.

ABSTRACT. This paper studies a first-order expansion of a combination C+J of intuitionistic and classical propositional logic, which was studied by Humberstone(1979) and Del Cerro and Herzig(1996), from a proof-theoretic viewpoint. While C+J has both classical and intuitionistic implications, our first-order expansion adds classical and intuitionistic universal quantifiers and one existential quantifier to C+J. This paper provides a multi-succedent sequent calculus G(FOC+J) for our combination of the first-order intuitionistic and classical logic. Our sequent calculus G(FOC+J) restricts contexts of the right rules for intuitionistic implication and intuitionistic universal quantifier to particular forms of formulas. The cut-elimination theorem is established syntactically to ensure the subformula property. As a corollary, G(FOC+J) is conservative over both first-order intuitionistic and classical logic. Strong completeness of G(FOC+J) is proved via a canonical model argument.

ABSTRACT. After recalling the definitions of atomic and molecular logics, we show how notions of bisimulation can be automatically defined from the truth conditions of the connectives of any of these logics. Then, we prove a generalization of van Benthem modal characterization theorem for molecular logics. Our molecular connectives should be uniform and contain all conjunctions and disjunctions. We use modal intuitionistic logic as case study and compare in particular our work with Olkhovikov's work.

ABSTRACT. In this talk, we present logical formalisms in which reasoning about concrete domains is embedded in formulae at the atomic level. These mainly include temporal/description logics with concrete domains. For the simple concrete domain (ℕ,<), we present known proof techniques to handle satisfiable (infinite) symbolic models, sometimes at the cost of going beyond omega-regularity. The talk is freely inspired from [1].

References:

[1] Stéphane Demri & Karin Quaas (2021): Concrete Domains in Logics: A Survey. ACM SIGLOG News 8(3), pp. 6–29, doi:10.1145/3477986.3477988.

ABSTRACT. We consider certain infectious logics (Sfde, dSfde, K3w, and PWK) and several their non-infectious modifications, including two new logics, reformulate previously constructed natural deduction systems for them (or present such systems from scratch for the case of new logics) in such a way that the proof of normalisation theorem becomes possible for these logics. We present such a proof and establish the negation subformula property for the logics in question.

ABSTRACT. We consider an example of four valued semantics partially inspired by quantum computations and negation-like operations occurred therein. In particular we consider a representation of so called square root of negation within four valued semantics as an operation which acts like a cycling negation. We define two variants of logical matrices performing different orders over the set of truth values. Purely formal logical result of our study consists in axiomatizing the logics of defined matrices as the systems of binary consequence relation and proving correctness and completeness theorems for these deductive systems.