Abstract
Some higher-order formulas are equivalent to formulas of first-order predicate logic or even propositional logic. In applications where formulas of higherorder predicate logic occur naturally it is very useful to determine whether the given formula is in fact equivalent to a simpler formula of first-order or prepositional logic. Typical applications where this occurs are predicate minimization by circumscription, correspondence theory in non-classical logics and simple versions of set theory. In these areas we are faced with formulas of second-order predicate logic with existentially or universally quantified predicate variables and want to simplify them by computing equivalent first-order formulas.
In general this problem is not even semi-decidable, so no complete quantifier elimination algorithms for predicate quantifiers can exist. Nevertheless, some of the proposed algorithms are quite powerful and can solve hard problems in the areas mentioned above.
In this paper the implementation of the scan algorithm1 proposed by Gabbay and Ohlbach [GO92b] is described. Besides the basic quantifier elimination algorithm, interfaces for computing first-order circumscription and correspondence axioms in non-classical logics are available. The interfaces translate the given problem specification into a quantifier elimination problem and invoke the basic algorithm.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Wilhelm Ackermann. Untersuchung über das Eliminationsproblem der mathematischen Logik. Mathematische Annalen, 110:390–413, 1935.
Patrick Doherty, Witold Lukaszewics, and Andrzej Szalas. Computing circumscription revisited: A reduction algorithm. Technical Report LiTH-IDA-R-94-42, Institutionen för Datavetenskap, University of Linköping, 1994.
Dov M. Gabbay and Hans Jürgen Ohlbach. Quantifier elimination in second-order predicate logic. In Bernhard Nebel, Charles Rich, and William Swartout, editors, Principles of Knowledge Representation and Reasoning (KR92), pages 425–435. Morgan Kaufmann, 1992.
Dov M. Gabbay and Hans Jürgen Ohlbach. Quantifier elimination in second-order predicate logic. South African Computer Journal, 7:35–43, July 1992. also published in [GO92a].
G. Neelakantan Kartha and Vladimir Lifschitz. A simple formalization of actions using circumscription. In Proceedings of IJCAI 95, 1995.
William McCune. Otter 2.0. In Mark Stickel, editor, Proc. of 10th Internation Conference on Automated Deduction, LNAI 449, pages 663–664. Springer Verlag, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ohlbach, H.J. (1996). SCAN—Elimination of predicate quantifiers. In: McRobbie, M.A., Slaney, J.K. (eds) Automated Deduction — Cade-13. CADE 1996. Lecture Notes in Computer Science, vol 1104. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61511-3_77
Download citation
DOI: https://doi.org/10.1007/3-540-61511-3_77
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61511-8
Online ISBN: 978-3-540-68687-3
eBook Packages: Springer Book Archive