We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions. It is practically relevant because it makes it possible to use a decision procedure for the guarded fragment in order to decide regular grammar logics with (...) converse. The class of regular grammar logics includes numerous logics from various application domains. A consequence of the translation is that the general satisfiability problem for every regular grammar logics with converse is in EXPTIME. This extends a previous result of the first author for grammar logics without converse. Other logics that can be translated into GF2 include nominal tense logics and intuitionistic logic. In our view, the results in this paper show that the natural first-order fragment corresponding to regular grammar logics is simply GF2 without extra machinery such as fixed-point operators. (shrink)

We define cut-free display calculi for knowledge logics wherean indiscernibility relation is associated to each set of agents, andwhere agents decide the membership of objects using thisindiscernibility relation. To do so, we first translate the knowledgelogics into polymodal logics axiomatised by primitive axioms and thenuse Kracht's results on properly displayable logics to define thedisplay calculi. Apart from these technical results, we argue thatDisplay Logic is a natural framework to define cut-free calculi for manyother logics with relative accessibility relations.

We consider fragments of the relational logic RL(1) obtained by posing various constraints on the relational terms involving the operator of composition of relations. These fragments allow to express several non classical logics including modal and description logics. We show how relational dual tableaux can be employed to provide decision procedures for each of them.

We present a framework for machine implementation of families of non-classical logics with Kripke-style semantics. We decompose a logic into two interacting parts, each a natural deduction system: a base logic of labelled formulae, and a theory of labels characterizing the properties of the Kripke models. By appropriate combinations we capture both partial and complete fragments of large families of non-classical logics such as modal, relevance, and intuitionistic logics. Our approach is modular and supports uniform proofs of soundness, completeness and (...) proof normalization. We have implemented our work in the Isabelle Logical Framework. (shrink)

This book provides a detailed exposition of one of the most practical and popular methods of proving theorems in logic, called Natural Deduction. It is presented both historically and systematically. Also some combinations with other known proof methods are explored. The initial part of the book deals with Classical Logic, whereas the rest is concerned with systems for several forms of Modal Logics, one of the most important branches of modern logic, which has wide applicability.

Recently M. Szabolcs [12] has shown that many substructural logics including Lambek CalculusL are complete with respect to relativized Relational Semantics. The current paper proves that it is sufficient forL to consider a relativization to the relation x dividesy in some fixed semigroupG.

ABSTRACT Propositional dynamic logic with converse and test, is enriched with complement, intersection and relational operations of weakest prespecification and weakest postspecification. Relational deduction system for the logic is given based on its interpretation in the relational calculus. Relational interpretation of the operators ?repeat? and ?loop? is given.

We present a labelled version of Lambek Calculus without unit, and we use it to prove a completeness theorem for Lambek Calculus with respect to some relational semantics.

This is an extended version of the lectures given during the 12-thConference on Applications of Logic in Philosophy and in the Foundationsof Mathematics in Szklarska Poręba. It contains a surveyof modal hybrid logic, one of the branches of contemporary modal logic. Inthe first part a variety of hybrid languages and logics is presented with adiscussion of expressivity matters. The second part is devoted to thoroughexposition of proof methods for hybrid logics. The main point is to showthat application of hybrid logics (...) may remarkably improve the situation inmodal proof theory. (shrink)

This paper introduces Basic Intuitionistic Set Theory BIST, and investigates it as a first-order set theory extending the internal logic of elementary toposes. Given an elementary topos, together with the extra structure of a directed structural system of inclusions on the topos, a forcing-style interpretation of the language of first-order set theory in the topos is given, which conservatively extends the internal logic of the topos. This forcing interpretation applies to an arbitrary elementary topos, since any such is equivalent to (...) one carrying a dssi. We prove that the set theory BIST+Coll is sound and complete relative to forcing interpretations in toposes with natural numbers object . Furthermore, in the case that the structural system of inclusions is superdirected, the full Separation schema is modelled. We show that all cocomplete and realizability toposes can be endowed with such superdirected systems of inclusions.A large part of the paper is devoted to an alternative notion of category-theoretic model for BIST, which, following the general approach of Joyal and Moerdijkʼs Algebraic Set Theory, axiomatizes the structure possessed by categories of classes compatible with BIST. We prove soundness and completeness results for BIST relative to the class-category semantics. Furthermore, BIST+Coll is complete relative to the restricted collection of categories of classes given by categories of ideals over elementary toposes with nno and dssi. It is via this result that the completeness of the original forcing interpretation is obtained, since the internal logic of categories of ideals coincides with the forcing interpretation. (shrink)

Contact relations have been studied in the context of qualitative geometry and physics since the early 1920s, and have recently received attention in qualitative spatial reasoning. In this paper, we present a sound and complete proof system in the style of Rasiowa and Sikorski (1963) for relation algebras generated by a contact relation.

Over the last twenty years, in all of these neighbouring fields, modal systems have been developed that we call multi-dimensional. (Our definition of multi ...

We introduce an Automatic Theorem Prover (ATP) of a dual tableau system for a relational logic for order of magnitude qualitative reasoning, which allows us to deal with relations such as negligibility, non-closeness and distance. Dual tableau systems are validity checkers that can serve as a tool for verification of a variety of tasks in order of magnitude reasoning, such as the use of qualitative sum of some classes of numbers. In the design of our ATP, we have introduced some (...) heuristics, such as the so called phantom variables, which improve the efficiency of the selection of variables used un the proof. (shrink)