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]).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Note that in case ψ is a negated formula \(\neg \varphi \) we must consider all cases which φ may obtain.
- 2.
More detailed account of complexity problems of several techniques may be found e.g. in Massacci [186] .
- 3.
Cf. respective considerations from the preceding section.
Reference
Fitting, M. 1996. First-order logic and automated theorem proving. Berlin; Springer.
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”.
Horrocks, I., U. Satler, and S. Tobies. 2000. Practical reasoning for very expressive description logics. Logic Journal of the IGPL 8(3): 239–263.
Horrocks, I. 1997. Optimising tableaux decision procedures for description logics, PhD Thesis, University of Manchester.
Massacci, F. 1994. Strongly analytic tableaux for normal modal logics. In Proc. CADE-12, ed. A. Bundy, LNAI 814: 723–737. New York: Springer.
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.
Fitting, M. 1983. Proof methods for modal and intuitionistic logics. Dordrecht; Rei-del.
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.
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.
Rescher, N., and A. Urquhart. 1971. Temporal logic. New York: Springer-Verlag.
Goldblatt, R.I. 1987. Logics of time and computation. Stanford: CSLI Lecture Notes.
Indrzejczak, A. 2003. A labelled natural deduction system for linear temporal logic. Studia Logica 75(3): 345–376.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2010 Springer Science+Business Media B.V.
About this chapter
Cite this chapter
Indrzejczak, A. (2010). Analytic Labelled ND and Proof Search. In: Natural Deduction, Hybrid Systems and Modal Logics. Trends in Logic, vol 30. Springer, Dordrecht. https://doi.org/10.1007/978-90-481-8785-0_10
Download citation
DOI: https://doi.org/10.1007/978-90-481-8785-0_10
Published:
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-8784-3
Online ISBN: 978-90-481-8785-0
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)