Advertisement

Analytic Labelled ND and Proof Search

  • Andrzej IndrzejczakEmail author
Chapter
Part of the Trends in Logic book series (TREN, volume 30)

Abstract

LND system from  Chapter 8 allows us to construct simple derivations but is not analytic. We have mentioned in Section 8.5 that one may obtain complete, universal and analytic version similarly as in  Chapter 4; by step-wise simulation of every tableau with the help of only elimination rules and analytic applications of cut (i.e. [LRED]).

Keywords

Modal Logic Temporal Logic Decision Procedure Linear Logic Elimination Rule 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Reference

  1. [95]
    Fitting, M. 1996. First-order logic and automated theorem proving. Berlin; Springer.Google Scholar
  2. [186]
    Massacci, F. 1998. Single step tableaux for modal logics: Methodology, computations, algorithms. Technical Report TR-04, Dipartimento di Informatica e Sistemistica, Universita di Roma “La Sapienza”.Google Scholar
  3. [134]
    Horrocks, I., U. Satler, and S. Tobies. 2000. Practical reasoning for very expressive description logics. Logic Journal of the IGPL 8(3): 239–263.CrossRefGoogle Scholar
  4. [133]
    Horrocks, I. 1997. Optimising tableaux decision procedures for description logics, PhD Thesis, University of Manchester.Google Scholar
  5. [185]
    Massacci, F. 1994. Strongly analytic tableaux for normal modal logics. In Proc. CADE-12, ed. A. Bundy, LNAI 814: 723–737. New York: Springer.Google Scholar
  6. [117]
    Goré, R. 1999. Tableau methods for modal and temporal logics. In Handbook of tableau methods, eds. M. D’Agostino et al., 297–396. Dordrecht: Kluwer Academic Publishers.Google Scholar
  7. [93]
    Fitting, M. 1983. Proof methods for modal and intuitionistic logics. Dordrecht; Rei-del.Google Scholar
  8. [200]
    Ono, H., and A. Nakamura. 1980. On the size of refutation Kripke models for some linear modal and tense logics. Studia Logica 39: 325–333.CrossRefGoogle Scholar
  9. [183]
    Marx, M., S. Mikulas, and M. Reynolds. 2000. The mosaic method for temporal logics. In Automated reasoning with analytic tableaux and related methods, ed. R. Dyckhoff, Proc. of International Conference TABLEAUX 2000, Saint Andrews, Scotland, LNAI 1847, 324–340. New York: Springer.Google Scholar
  10. [231]
    Rescher, N., and A. Urquhart. 1971. Temporal logic. New York: Springer-Verlag.Google Scholar
  11. [112]
    Goldblatt, R.I. 1987. Logics of time and computation. Stanford: CSLI Lecture Notes.Google Scholar
  12. [151]
    Indrzejczak, A. 2003. A labelled natural deduction system for linear temporal logic. Studia Logica 75(3): 345–376.CrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media B.V. 2010

Authors and Affiliations

  1. 1.Dept. LogicUniversity of LódzLódzPoland

Personalised recommendations