Abstract
We present a new automated proof method for first-order classical logic, aimed at limiting the combinatorial explosion of the search. It is non-clausal, based on BDDs (binary decision diagrams) and on new strategies that control the size and traversal of the search space by controlling the amount of information, in Shannon's sense, gained at each step of the proof. Our prover does not search blindly for a proof, but thinks a lot to decide of a course of action. Practical results show that this pays off.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
P. Andrews. Theorem proving via general matings. JACM, 28(2):193–214, 1981.
W. Bibel. Automated Theorem Proving. Vieweg, 2nd, revised edition, 1987.
J.-P. Billon. Perfect normal forms for discrete functions. Technical Report 87019, Bull, 1987.
R. E. Bryant. Graph-based algorithms for boolean functions manipulation. IEEE Trans. Computers, C35(8):677–692, 1986.
J. Goubault. Implementing functional languages with fast equality, sets and maps: an exercise in hash consing. Technical report, Bull, 1992.
J. Goubault. Démonstration automatique en logique classique: complexité et méthodes. PhD thesis, école olytechnique, Palaiseau, France, 1993.
J. Goubault. The HimML reference manual. Technical report, Bull, 1993.
J. Goubault. Syntax independent connections. In D. et al.. Basin, editor, Workshop on Theorem Proving with Analytic Tableaux and Related Methods, number MPI-I-93-213. Max Planck Institut für Informatik, 1993.
J. Goubault. A BDD-based skolemization procedure. In M. D'Agostino, editor, Workshop on Theorem Proving with Analytic Tableaux and Related Methods, 1994.
J. Goubault. The complexity of resource-bounded first-order classical logic. In 11th STACS, 1994.
R. Kowalski. A proof procedure using connection graphs. JACM, 22(4):572–595, 1975.
R. Kowalski and D. Kuehner. Linear resolution with selection function. Artificial Intelligence, 2:227–260, 1971.
R. Manthey and F. Bry. SATCHMO: a theorem prover implemented in Prolog. In 9th CADE, pages 415–434, 1988.
A. Martelli and U. Montanari. An efficient unification algorithm. ACM TOPLAS, 4(2):258–282, 1982.
F. J. Pelletier. Seventy-five problems for testing automatic theorem provers. JAR, 2:191–216, 1986. Errata in JAR, 4:235–236, 1988.
F. J. Pelletier and P. Rudnicki. Non-obviousness. AAR Newsl., 6:4–5, 1986.
J. Posegga. Deduction with Shannon Graphs or: How to Lift BDDs to First-order Logic. PhD thesis, Institut für Logik, Komplexität und Deduktionssystem, Universität Karlsruhe, Karlsruhe, FRG, 1993.
C. E. Shannon and W. Weaver. The Mathematical Theory of Communication. Illinois University Press, 1949. Reprinted by Illini Books, 1963.
L. Wos, G. A. Robinson, and D. F. Carson. Efficiency and completeness of the set of support strategy in theorem proving. JACM, 12(4):536–541, 1965.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Goubault, J. (1994). Proving with BDDs and control of information. In: Bundy, A. (eds) Automated Deduction — CADE-12. CADE 1994. Lecture Notes in Computer Science, vol 814. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58156-1_36
Download citation
DOI: https://doi.org/10.1007/3-540-58156-1_36
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58156-7
Online ISBN: 978-3-540-48467-7
eBook Packages: Springer Book Archive