ABSTRACT. CEGAR-tableaux utilise SAT-solvers and modal clause learning to give  the current state-of-the-art satisfiability checkers for basic modal  logics K, KT and S4. I will start with a brief overview of the basic  CEGAR-tableaux method for these logics.

I will show how to extend CEGAR-Tableaux to handle the five basic  extensions of K by the axioms D, T, B, 4 and 5, and then indirectly to  the whole modal cube. Experiments confirm that the resulting  satisfiability-checkers are also the current best ones for these  logics.

I will show how to extend CEGAR-tableaux to handle the modal tense  logic Kt, which involves modalities for the "future" and the "past".  Once again, our experiments show that CEGAR-tableaux are  state-of-the-art for these logics.

The talk is intended as an exposition for a broad audience and does  not require any knowledge of SAT-solvers or computer science but some  knowledge of modal logic would help.

The research reported in this talk is a result of joint work with Cormac Kikkert.

ABSTRACT. Although strong logicist programs for reduction of set theory to logics failed, it is still reasonable to investigate weaker logics of classes without special existence assumptions for specific sets. In particular, proof theoretic tools may be applied to investigate the properties of such logics. Some proposals of this kind, but significantly different, were developed by Quine, Scott and Tennant. We present cut-free sequent calculi for some of these approaches based on the methodology of defining well-behaved rules for term-forming operators, like set abstracts.

ABSTRACT. I'll present a novel theory of definite descriptions. The background logic is positive free logic, the methodology proof theoretic semantics. Rather than formalising definite descriptions `the F' by a term forming operator as ixFx, as is customary, they are treated in the context of complete sentences by a binary quantifier: Ix(F, G) means `The F is G'. The meaning of I is given by its rules of inference in accordance with proof-theoretic semantics. The approach settles a number of questions regarding the logical laws governing definite descriptions in a principled fashion.

ABSTRACT. Modal logic with definite descriptions (ML(DD)) is an extension of modal hybrid logic in which not only nominals can occur in the subscript of a satisfaction operator, but also arbitrary formulas from the language of the logic. Intuitively, a formula @_φψ reads `at the only world at which φ holds, ψ also holds'. In the talk, we will show complexity results for ML(DD), define a bisimulation that adequately characterises this logic, and discuss an analytic tableau calculus for it.

ABSTRACT. We present a bisequent calculus (BSC) for the minimal theory of definite descriptions (DD) in the setting of neutral free logic, where formulae with non-denoting terms have no truth value. The treatment of quantifiers, atomic formulae and simple terms is based on the approach developed by Pavlovic and Gratzl. We extend their results to the version with identity and definite descriptions. In particular, the admissibility of cut is proven for this extended system.

ABSTRACT. In this article, the disjunction-free fragment of Jaskowski's discussive logic D_2 in the language of classical logic is shown to be complete with respect to three- and four-valued semantics. As a byproduct, a rather simple axiomatization of the disjunction-free fragment of D_2 is obtained. Some implications of this result are also discussed.

ABSTRACT. It is not uncommon for a logic to be invented multiple times, hinting at its robustness. This trend is followed also by the expansion BD+ of Belnap-Dunn logic by Boolean negation. Ending up in the same logic, however, does not mean that the semantic interpretations are always the same as well. In particular, different interpretations can bring us to different logics, once the basic setting is moved from a classical one to an intuitionistic one. For BD+, two such paths seem to have been taken; one (BDi) by N. Kamide along the so-called American plan, and another (HYPE) by G. Moisil and H. Leitgeb along the so-called Australian plan. The aim of this paper is to better understand this divergence. This task is approached mainly by (i) formulating a semantics for first-order BD+ that provides an Australian view of the system; (ii) showing connections of the less explored (first-order) BDi with neighbouring systems, including an intermediate logic and variants of Nelson's logics.

ABSTRACT. In this short paper we will discuss the similarities and differences between two semantic approaches to modal logics – non-deterministic semantics and restricted non-deterministic semantics. Generally speaking, both kinds of semantics are similar in the sense that they employ non-deterministic matrices as a starting point but differ significantly in the way extensions of the minimal modal logic M are constructed.

Both kinds of semantics are many-valued and truth-values are typically expressed in terms of tuples of 0s and 1s, where each dimension of the tuple represents either truth/falsity, possibility/non-possibility, necessity/non-necessity etc. And while non-deterministic semantics for modal logic offers an intuitive interpretation of the truth-values and the concept of modality, restricted non-deterministic semantics are more general in terms of providing extensions of M, including normal ones, in an uniform way.

On the example of three modal logics, MK, MKT and MKT4, we will show the differences and similarities of those two approaches. Additionally, we will briefly discuss (current) restrictions of both approaches.

ABSTRACT. We combine the concepts of modal logics and many-valued logics in a general and comprehensive way. Namely, given any finite linearly ordered set of truth values and any set of propositional connectives defined by truth tables, we define the many-valued minimal normal modal logic, presented as a Gentzen-like sequent calculus, and prove its soundness and strong completeness with respect to many-valued Kripke models. The logic treats necessitation and possibility independently, i.e., they are not defined by each other, so that the duality between them is reflected in the proof system itself. We also prove the finite model property (that implies strong decidability) of this logic and consider some of its extensions. Moreover, we show that there is exactly one way to define negation such that De Morgan's duality between necessitation and possibility holds. We also prove that many-valued intuitionistic logic is a fragment of one of the extensions of our many-valued modal logic.