This volume examines the notion of an analytic proof as a natural deduction, suggesting that the proof's value may be understood as its normal form--a concept with significant implications to proof-theoretic semantics.

Although resolution-based inference is perhaps the industry standard in automated theorem proving, there have always been systems that employed a different format. For example, the Logic Theorist of 1957 produced proofs by using an axiomatic system, and the proofs it generated would be considered legitimate axiomatic proofs; Wang’s systems of the late 1950’s employed a Gentzen-sequent proof strategy; Beth’s systems written about the same time employed his semantic tableaux method; and Prawitz’s systems of again about the same time are often (...) said to employ a natural deduction format. [See Newell, et al (1957), Beth (1958), Wang (1960), and Prawitz et al (1960)]. Like sequent proof systems and tableaux proof systems, natural deduction systems retain.. (shrink)

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)

LetL be any modal or tense logic with the finite model property. For eachm, definer L (m) to be the smallest numberr such that for any formulaA withm modal operators,A is provable inL if and only ifA is valid in everyL-model with at mostr worlds. Thus, the functionr L determines the size of refutation Kripke models forL. In this paper, we will give an estimation ofr L (m) for some linear modal and tense logicsL.

This paper is about the good side of modal logic, the bad side of modal logic, and how hybrid logic takes the good and fixes the bad.In essence, modal logic is a simple formalism for working with relational structures . But modal logic has no mechanism for referring to or reasoning about the individual nodes in such structures, and this lessens its effectiveness as a representation formalism. In their simplest form, hybrid logics are upgraded modal logics in which reference to (...) individual nodes is possible.But hybrid logic is a rather unusual modal upgrade. It pushes one simple idea as far as it will go: represent all information as formulas. This turns out to be the key needed to draw together a surprisingly diverse range of work . Moreover, it displays a number of knowledge representation issues in a new light, notably the importance of sorting. (shrink)

The paper contains an exposition of standard ND-formalizations for modal logics. For the sake of simplicity, it is limited to propositional monomodal logics because focus is on methods not on logics. Some of the discussed approaches, however, may be easily extended to first order modal logics of different sorts or to multimodal logics . Natural Deduction is understood in the strict sense, explained below; neither Gentzen Sequent Calculus, nor Tableau Systems belong to that group. Moreover, some ND-systems with generalized apparatus, (...) like [2] or [3] are also omitted in this survey. There are four basic approaches to modality via NDformalization, which are compared and evaluated with respect to their generality: modalization of assumptions, modalization of reiteration rule, modalization of rules, application of modal assumptions. We focus on practical matters, especially on the applicability of discussed approaches, the only exception is the discussion of independent rules for necessity and possibility in the last section. (shrink)

This completely self-contained study, widely considered the best book in the field, is intended to serve both as an introduction to quantification theory and as ...

Description Logics are a family of knowledge representation formalisms mainly characterised by constructors to build complex concepts and roles from atomic ones. Expressive role constructors are important in many applications, but can be computationally problematical.We present an algorithm that decides satisfiability of the DL ALC extended with transitive and inverse roles and functional restrictions with respect to general concept inclusion axioms and role hierarchies; early experiments indicate that this algorithm is well-suited for implementation. Additionally, we show that ALC extended with (...) just transitive and inverse roles is still in PSPACE. We investigate the limits of decidability for this family of DLs, showing that relaxing the constraints placed on the kinds of roles used in number restrictions leads to the undecidability of all inference problems. Finally, we describe a number of optimisation techniques that are crucial in obtaining implementations of the decision procedures, which, despite the high worst-case complexity of the problem, exhibit good performance with real-life problems. (shrink)

We will define cut-free Gentzen-style systems for the modal propositional logics $S4.3 \vee \square)$ and $S4.3Grz \supset A)\supset A)$, and give a syntactical proof of the cut-elimination theorem. As its application, we will give a syntactical proof of the McKinsey-Tarski correspondence between $S_\omega$ and S4.3 and its extension.