A new method for testing decision procedures in modal logics. (English) Zbl 1430.68409
McCune, William (ed.), Automated deduction – CADE-14. 14th international conference on automated deduction, Townsville, North Queensland, Australia. July 13–17, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1249, 264-267 (1997).
For the entire collection see [Zbl 1415.68038].
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
| 03B35 | Mechanization of proofs and logical operations |
| 03B45 | Modal logic (including the logic of norms) |
Software:
TABLEAUXReferences:
| [1] | F. Baader, E. Franconi, B. Hollonder, B. Nebel, and H.J. Profitlich. An Empirical Analysis of Optimization Techniques for Terminological Representation Systems or: Making KRIS get a move on. Applied Artificial Intelligence. Special Issue on Knowledge Base Management, 4:109-132, 1994. |
| [2] | M. Buro and H. Buning. Report on a SAT competition. Technical Report 110, University of Paderborn, Germany, November 1992. · Zbl 1023.68656 |
| [3] | L. Catach. TABLEAUX: a general theorem prover for modal logics. Journal of Automated Reasoning, 7, 1991. · Zbl 0743.03008 |
| [4] | S. Demri. Uniform and Nonuniform strategies for tableaux calculi for modal logics. Journal of Applied Nonclassical Logics, 5(1):77-98, 1995. · Zbl 0826.03006 · doi:10.1080/11663081.1995.10510844 |
| [5] | F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from prepositional decision procedures — the case study of modal K. In Proc. of the 13th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, New Brunswick, NJ, USA, August 1996. Springer Verlag. Also DIST-Technical Report 96-0037 and IRST-Technical Report 9601-02. · Zbl 1415.03022 |
| [6] | F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures — the case study of modal K(m). Technical Report 9611-06, IRST, Trento, Italy, 1996. A shorter version is submitted to “Information and Computation”. · Zbl 1415.03022 |
| [7] | J. Y. Halpern. The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic. Artificial Intelligence, 75(3):361-372, 1995. · Zbl 1014.03508 · doi:10.1016/0004-3702(95)00018-A |
| [8] | J.Y. Halpern and Y. Moses. A guide to the completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence, 54(3):319-379, 1992. · Zbl 0762.68029 · doi:10.1016/0004-3702(92)90049-4 |
| [9] | S. Kirkpatrick and B. Selman. Critical behaviour in the satisfiability of random boolean expressions. Science, 264:1297-1301, 1994. · Zbl 1226.68097 · doi:10.1126/science.264.5163.1297 |
| [10] | D. Mitchell, B. Selman, and H. Levesque. Hard and Easy Distributions of SAT Problems. In Proc. of the 10th National Conference on Artificial Intelligence, pages 459-465, 1992. |
| [11] | C. P. Williams and T. Hogg. Exploiting the deep structure of constraint problems. Artificial Intelligence, 70:73-117, 1994. · Zbl 0938.68827 · doi:10.1016/0004-3702(94)90104-X |
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.
