Abstract
We present a general theorem proving system for propositional modal logics, called TABLEAUX. The main feature of the system is its generality, since it provides an unified environment for various kinds of modal operators and for a wide class of modal logics, including usual temporal, epistemic or dynamic logics. We survey the modal languages covered by TABLEAUX, which range from the basic one L(□, ◊) through a complex multimodal language including several families of operators with their transitive-closure and converse. The decision procedure we use is basically a semantic tableaux method, but with slight modifications compared to the traditional one. We emphasize the advantages of such semantical proof methods for modal logics, since we believe that the models construction they provide represents perhaps the most attractive feature of these logics for possible applications in computer science and AI. The system has been implemented in Prolog, and appears to be of reasonable efficiency for most current examples. Experimental results are given in the paper, with two lists of test examples.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Abadi, M. and Manna, Z., ‘Modal theorem proving’,Lecture Notes in Computer Science Vol. 230 (1986).
Abadi, M. and Manna, Z., ‘Temporal logic programming’,Proc. IEEE Symposium on Logic Programming (Sept. 1987) San Francisco, California, pp. 4–16.
VanBenthem J.,The Logic of Time, D. Reidel, Dordrecht (1980).
Ben-Ari, M., Manna, Z. and Pnueli, A., ‘The temporal logic of branching time’,Proc. 8th Annual ACM Symposium on Principles of Programming Languages (1981), pp. 164–176.
Bull, R. and Segerberg, K., ‘Basic modal logic’ in [28], pp. 1–88.
Burgess, J. P., ‘Decidability for branching time’,Studia Logica 39 (2/3), (1980).
Catach, L., ‘Normal multimodal logics’,Proc. AAAI'88, pp. 491–495.
Catach, L., ‘Les logiques multimodales’ (‘Multimodal logics’), Doctoral Thesis, IBM Paris Scientific Center and L.I.T.P., Paris 6 University (1989).
Clarke E. M. and Emerson E. A., ‘Design and synthesis of synchronization skeletons using branching time temporal logic’,Lecture Notes in Computer Science Vol. 131 (1982), pp. 52–71.
Clarke, E. M., Emerson, E. A., and Sistla, A. P., ‘Automatic verification of finite-state concurrent systems using temporal logic specifications’,ACM Transactions on Programming Languages and Systems,8(2) (1986).
Chellas, B. F.,Modal Logic. An Introduction, Cambridge University Press (1980).
Cavalli A. and Horn F., ‘Evaluation des spécifications formelles à l'aide des automates finis et de la logique temporelle’, Report L.I.T.P. No. 86-74, Paris VI/Paris VII University, France (1986).
Enjalbert, P. and Auffray, Y., ‘Démonstration de théorèmes en logique modale: un point de vue équationnel’,European Workshop on Logical Methods in Artificial Intelligence (JELIA'88), Roscoff, France (1988).
Enjalbert P. and Fariñas L., ‘Modal Resolution in clausal form’, Report No. RG 14-86, Greco de Programmation, Université de Bordeaux I, France (1986).
Emerson E. A. and Halpern J. Y. ‘Decision procedures and expressiveness in the temporal logic of branching time’,Journal of Computer and System Sciences 30, 1–24 (1985).
Emerson E. A., ‘Automata, tableaux and temporal logics’,Lecture Notes in Computer Science Vol. 193 (1985), pp. 79–87.
Emerson E. A. and Sistla A. P., ‘Deciding full branching time logic’,Information and Control 61, 175–201 (1984).
Fariñas Del Cerro, L., ‘Resolution modal logic’,Logique et Analyse 110–111 (1985).
Fischer M. J. and Immerman N., ‘Interpreting logics of knowledge in propositional dynamic logic with converse’,Information Processing Letters 25 175–181 (1987).
Fitting M., ‘Tableaux methods of proof for modal logics’,Notre-Dame Journal of Formal Logic 13 237–247 (1972).
Fitting, M., ‘Proof methods for modal and intuitionistic logics’, Reidel,Synthese Library Vol. 169 (1983).
Fischer M. J. and Ladner R. E., ‘Propositional dynamic logic of regular programs,Journal of Computer and System Sciences 18 194–211 (1979).
Fujita, M.et al. ‘Tokyo: logic programming language based on temporal logic’,Proc. 3th International Conference on Logic Programming, London pp. 695–709 (1986).
Gabbay, D. M., ‘Modal and temporal logic programming’, inTemporal Logics, A. Galton (ed.), Academic Press (1988).
Groeneboer, C. and Delgande, J. P., ‘Tableau-based theorem proving in normal conditional logics’,Proc. AAAI'88, pp. 171–176.
Gurevich, Y. and Shelah, S., ‘The decision problem for Branching Time Logic’,Journal of Symbolic Logic 50(3) (1985).
Halpern, J. Y., ‘Reasoning about knowledge: an overview’,Proc. Conference on Theoretical Aspects of Reasoning about Knowledge (J. Y. Halpern (ed.)), Morgan Kauffmann (1986).
‘Extensions of classical logic’,Handbook of Philosophical Logic Vol. II, D. Gabbay and F. Guenthner (eds.), D. Reidel Publishing Company (1984).
Harel, D., ‘Dynamic logic’, in [28], pp. 497–604.
Hughes G. E. and Cresswell M. J.,An Introduction to Modal Logic, Methuen, London (1968).
Halpern, J. Y. and Moses, Y., ‘A guide to the modal logics of knowledge and belief’,Proc. IJCAI pp. 480–490 (1985).
Halpern J. Y. and Shoham Y., ‘A propositional modal logic of time intervals’,Proc. IEEE Symposium on Logic in Computer Science Vol. 1 pp. 279–292 (1986).
Jackson, P. and Reichgelt, H., ‘A general proof method for first-order modal logic’,Proc. IJCAI pp. 942–944 (1987).
Jackson, P. and Reichgelt, H. ‘A general proof method for modal predicate logic without the Barcan formula’,Proc. AAAT'88, pp. 177–181 (1988).
Konolige K., ‘Resolution and quantified epistemic logics’,Lectures Notes in Computer Science Vol. 230 pp. 199–208 (1986).
Ladner R. E., ‘The computational complexity of provability in systems of modal propositional logic’,SIAM J. Computing 6(3) 467–480 (1977).
Lehmann D. and Kraus S., ‘Knowledge, belief and time’,Lecture Notes in Computer Science, Vol. 226 pp. 186–195 (1986).
Lafon, E. and Schwind, C. B., ‘A theorem prover for action performance’,Proc. ECAI'88 (1988).
Michel, M., ‘Computation of temporal operators’,Logique et Analyse 110/111 (1985).
Moszkowski, B.,Executing temporal logic of programs, Cambridge University Press (1986).
Manna, Z. and Wolper, P., ‘Synthesis of communicating processes from temporal logic specifications’, Report No. STAN-CS-81-872, Stanford University, Dept. of Computer Science (1981).
Niemela, I. and Tuominen, H., ‘Helsinki logic machine: a system for logical expertise’, Technical report Series B (No. 1), Helsinki University of Technology, Digital Systems Laboratory (1987).
Parikh R., ‘Propositional dynamic logics of programs: a survey’,Lecture Notes in Computer Science Vol. 125 pp. 102–144 (1981).
Plaisted D. A., ‘A decision procedure for combinations of propositional temporal logic and other specialized theories’,J. Automated Reasoning 2, 171–190 (1986).
Pnueli, A., ‘The temporal logic of programs’,Proc. 18th IEEE Symposium on Foundations of Computer Science pp. 46–57 (1977).
Pratt, V. R., ‘Models of program logics’,Proc. 20th IEEE Symposium on Foundations of Computer Science (1978).
IBM, VM/Programming in Logic (VM/Prolog), Program Offering 5785-ABH.
Roche Y., ‘Implémentation d'un démonstrateur de théorèmes pour les logiques modales et temporelles en Prolog’, Report GIA-GRTC, Luminy University, Marseille, France (1985).
Rescher, N. and Urquhart, A.,Temporal Logic, Springer-Verlag (1971).
Sistla, A. P. and Clarke, E. M., ‘The complexity of Propositional linear temporal logics’,J. ACM 32(3) (1985).
Schwind, C., ‘Un démonstrateur de théorèmes pour des logiques modales et temporelles en Prolog’,Proc. 5th. Congrès Reconnaissance des Formes et Intelligence Artificielle (RFIA), France pp. 897–914 (1985).
Smullyan, R. M.,First-Order Logic, Springer-Verlag (1968).
Thistlewaite P. B., McRobbie M. A., and Meyer R. K., ‘The KRIPKE automated theorem proving system’,Lecture Notes in Computer Science Vol. 230 pp. 705–706 (1986).
Venema, Y., ‘Expressiveness and completeness of an interval tense logic’, Report, Institute for Language, Logic and Information, University of Amsterdam (1988).
Yardi, M. Y. and Wolper, P., ‘Automata theoretic techniques for modal logics of programs’,Proc. ACM Symposium on Theory of Computing (1984).
Wallen, L. A., Matrix proof methods for modal logics',Proc. IJCAI pp. 917–923 (1987).
Wolper, P., ‘Temporal logic can be more expressive’,Information and Control 56 (1983).
Wolper, P., ‘The tableaux method for temporal logic: an overview’,Logique et Analyse 110–111 (1985).
Author information
Authors and Affiliations
Additional information
A preliminary version of this paper appeared in the Proceedings of the International Computer Science Conference (ICSC'88), Hong-Kong, December 19–21, 1988.
Rights and permissions
About this article
Cite this article
Catach, L. TABLEAUX: A general theorem prover for modal logics. J Autom Reasoning 7, 489–510 (1991). https://doi.org/10.1007/BF01880326
Received:
Accepted:
Issue Date:
DOI: https://doi.org/10.1007/BF01880326