Un principe de résolution en logique modale. (French) Zbl 0566.03007

A resolution principle for the class of S5\({}^*\) formulas, which do not contain modal operators or for which the variables in the scope of a modal operator are free, is presented. Results analogous with classical ones are derived, beginning with characterizations of sets of ”clauses” by semantic trees and ending with the completeness theorem (unsatisfiability is equivalent with the existence of a refutation).
Reviewer: C.Masalagiu


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


[1] 1. R. CARNAP, Modalities and Quantification, J.S.L., vol. 11, 1946, p. 33-64. Zbl0063.00713 MR19562 · Zbl 0063.00713 · doi:10.2307/2268610
[2] 2. C. CHANG et R. LEE, Symbolic Logic and Mechanical Theorems proving, Academic Press, 1973. Zbl0263.68046 MR441028 · Zbl 0263.68046
[3] 3. G. HUGUES et M. CRESSWELL, An Introduction to Modal Logic, Methuen and co td, 1972. Zbl0205.00503 · Zbl 0205.00503
[4] 4. R. B. MARCUS, A functional Calculus of First Order Based on Strict Implications, J.S.L., vol. 11, (1946), 1-16. Zbl0063.00205 MR17229 · Zbl 0063.00205 · doi:10.2307/2269159
[5] 5. Z. MANNA et A. PNUELI, The modal Logic of Programs N-AIM-330, Stanford Ail., 1979. MR573251 · Zbl 0404.68011
[6] 6. J. A. ROBINSON, A Machine-Oriented Logic Based on the Resolution Principle, J.A.C.M., vol. 12, 1965, p. 23-41. Zbl0139.12303 MR170494 · Zbl 0139.12303 · doi:10.1145/321250.321253
[7] 7. P. TICHY, On de Dicto Modalities in Quantified S5, J. of Philo. Logic 2, 1975, p. 387-392. Zbl0268.02014 MR429493 · Zbl 0268.02014 · doi:10.1007/BF00129610
[8] 8. H. RASIOWA et R. SIKORSKI, Mathematics of Metamathematics, PWN Warszawa, 1963. Zbl0122.24311 MR163850 · Zbl 0122.24311
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.