×
Demri, Stéphane

Uniform and non uniform strategies for tableaux calculi for modal logics. (English) Zbl 0826.03006

J. Appl. Non-Class. Log. 5, No. 1, 77-96 (1995).
Logical calculi are formula manipulation methods for proving logical theorems. A very prominent class of logical calculi are the so-called tableaux systems. They can be used to refute formulae (proof by contradiction) or to show consistency by finding a model. The tableaux rules specify how a formula to be refuted must be decomposed into subformulae to be investigated. Tableaux systems usually build trees of formulae. A formula is refuted if each branch in the tree can be ‘closed’ by finding a contradiction.
Tableaux systems for standard propositional logic are confluent. This means the tableaux rules can be applied in an arbitrary order an no backtracking is necessary. For other logics this need not always be the case. A quite pathological case is the modal logic S4. Modal logic is propositional logic extended with the two modal operators box (‘necessarily’) and diamond (‘possibly’). S4 has the ‘transitivity axiom’ box \(p\) implies box box \(p\), which causes a lot of problems for automated reasoning systems. In particular the tableaux systems known so far are no longer confluent because wrong choices may cause the system to loop.
The problem of controlling the search in a tableaux system for propositional modal logics is investigated in the paper. Different backtracking and ordering strategies are proposed. Loop checking is combined with backtracking such that unnecessary choice points are avoided. The ordering strategies control the application of the tableaux rules for cases where different rules can be applied to the same node in the tree. So-called uniform strategies fix the ordering of the rule applications once and for all whereas non-uniform strategies choose the ordering according to the actual situation on the branch. Completeness is proved for the various strategies. They are tested with many examples from the literature and much empirical data is collected.
Reviewer: H.J.Ohlbach (Saarbrücken)

Cited in 4 Documents

MSC:

03B35 Mechanization of proofs and logical operations
03B45 Modal logic (including the logic of norms)

Keywords:

heuristic; tableaux systems; automated reasoning; propositional modal logics; backtracking; ordering strategies

Software:

TPTP; Minlog
PDF BibTeX XML Cite
\textit{S. Demri}, J. Appl. Non-Class. Log. 5, No. 1, 77--96 (1995; Zbl 0826.03006)
Full Text: DOI

References:

[1] DOI: 10.1007/BF00302639 · Zbl 0709.03008
[2] Bundy A., The computer modelling of mathematical reasoning. Academic Press (1983) · Zbl 0541.68067
[3] Catach L., Journal of Automated Reasoning 7 pp 489– (1991) · Zbl 0743.03008
[4] Caferra R., Journal of Symbolic Computation.
[5] Dubikajtis L., Reports on Mathematical Logic 11 pp 57– (1981)
[6] Demri S., Approches directe et par traduction en logiques modales: nouvelles stratégies et traduction inverse de preuves. PhD thesis, Institut National Polytechnique de Grenoble (1994)
[7] Demri S., JELIA-4 pp 182– (1994)
[8] Delgrande J., AAAI-7 pp 171– (1988)
[9] de Nivelle H., LPAR-4 pp 241– (1993)
[10] Fariñas del Cerro L., RAIRO 18 pp 161– (1983)
[11] Fitting M. C., Proof methods for modal and intuitionistic logics. D. Reidel Publishing Co. (1983) · Zbl 0523.03013
[12] DOI: 10.1007/BF00244394 · Zbl 0648.03004
[13] Hughes G. E., An introduction to modal logic. Methuen and Co. (1968) · Zbl 0205.00503
[14] Herzig A., Raisonnement automatique en logique modale et algorithmes d’unification. PhD thesis, Université P. Sabatier, Toulouse (1989)
[15] Hintikka J., Knowledge and Belief. (1962)
[16] Hudelmaier J., TABLEAUX-4 pp 105– (1994)
[17] Konolige K., A deduction model of belief. Pitman (1986) · Zbl 0683.68080
[18] Kowalski R., Machine Intelligence 5 pp 181– (1969)
[19] Kripke S., Modal and Many-valued logics, Acta Philosophica Fennica (1963) · Zbl 0131.00602
[20] Krishnamurty B., Acta Informatica 22 pp 253– (1985)
[21] Kaufl T., Revue d’Intelligence Artificielle, Special Issue on Automated Deduction 4 (3) pp 99– (1990)
[22] Loveland P. W., Automated Theorem Proving: A Logical Basis. North-Holland (1978) · Zbl 0364.68082
[23] Massey G., Notre Dame Journal of Formal Logic 11 (3) pp 340– (1970) · Zbl 0188.01901
[24] Massacci F., CADE-12, Nancy pp 723– (1994)
[25] McDermott D., Journal of the Association for Computing Machinery 29 (1982) · Zbl 0477.68099
[26] Mints G., International Conference on Computer Logic, Tallinn pp 198– (1988)
[27] Morgan C., IEEE Transactions on Computers 25 (8) pp 852– (1976) · Zbl 0329.68074
[28] McKinsey J., The Journal of Symbolic Logic 13 (1) pp 1– (1948) · Zbl 0037.29409
[29] Ognjanović Z., Theoretical Computer Science 129 pp 167– (1994) · Zbl 0805.03007
[30] Ohlbach H. J., CADE-9 pp 500– (1988)
[31] Pratt V., Studia Logica 39 pp 257– (1980) · Zbl 0457.03013
[32] Rautenberg W., The Journal of Philosophical Logic 12 pp 403– (1983) · Zbl 0547.03015
[33] Slaney, J. 1994. ”Minlog: a Minimal Logic Theorem Prover. Technical Report TR-ARP- 12/94, Australian National University”. To appear
[34] Smullyan R. M., First-Order Logic. Springer-Verlag (1968) · Zbl 0172.28901
[35] Sobociński B., Notre Dame Journal of Formal Logic 11 (3) pp 343– (1970) · Zbl 0188.01902
[36] Sutcliffe G., CADE-12, Nancy pp 252– (1994)
[37] Thistlewaite P. B., CADES-8 pp 705– (1986)
[38] Voronkov A., CADE-11 pp 648– (1992)
[39] Wallen L., Automated Deduction in Nonclassical Logics. (1990)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.