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

There are various contexts in which it is not pertinent to generate and attend to all the classical consequences of a given premiss—or to trace all the premisses which classically entail a given consequence. Such contexts may involve limited resources of an agent or inferential engine, contextual relevance or irrelevance of certain consequences or premisses, modelling everyday human reasoning, the search for plausible abduced hypotheses or potential causes, etc. In this paper we propose and explicate one formal framework for a (...) whole spectrum of consequence relations, flexible enough to be tailored for choices from a variety of contexts. We do so by investigating semantic constraints on classical entailment which give rise to a family of infra-classical logics with appealing properties. More specifically, our infra-classical reasoning demands (beyond ${\alpha\models\beta}$ ) that Mod(β) does not run wild, but lies within the scope (whatever that may mean in some specific context) of Mod(α), and which can be described by a sentence ${\bullet\alpha}$ with ${\beta\models\bullet\alpha}$ . Besides being infra-classical, the resulting logic is also non-monotonic and allows for non-trivial reasoning in the presence of inconsistencies. (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.