Abstract
In this article a modified form of tableau calculus, calledTableau Graph Calculus, is presented for overcoming the well-known inefficiencies of the traditional tableau calculus to a large extent. This calculus is based on a compact representation of analytic tableaux by using graph structures calledtableau graphs. These graphs are obtained from the input formula in linear time and incorporate most of the rule applications of normal tableau calculus during the conversion process. The size of this representation is linear with respect to the length of the input formula and the graph closely resembles the proof tree of tableau calculi thus retaining the naturalness of the proof procedure. As a result of this preprocessing step, tableau graph calculus has only a single rule which is repeatedly applied to obtain a proof. Many optimizations for the applications of this rule, to effectively prune the search space, are presented as well. Brief details of an implemented prover called FAUST, embedded within the higher-order theorem prover called HOL, are also given. Applications of FAUST within a hardware verification context are also sketched.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Gupta, A., “Formal hardware verification methods: A survey,”Journal of Formal Methods in System Design, 1:151–238, 1992.
Lindström, J., “On extensions of elementary logic,”Theoria, 35, 1969.
Gordon, M.J.C., “Why higher-order logic is a good formalism for specifying and verifying hardware,” in G. Milne and P.A. Subrahmanyam, editors,Formal aspects of VLSI Design. North-Holand, 1986.
Hanna, F.K. and Daeche, N., “Specification and verification of digital systems using higher-order predicate logic,”IEE Proc. Pt. E, 133(3):242–254, 1986.
Joyce, J., “More reasons why higher-order logic is a good formalism for specifying and verifying hardware,” inInternational Workshop on formal Methods in VLSI Design, Miami, 1991.
Kumar, R., Schneider, K. and Kropf, Th., “Structuring and automating hardware proofs in a higher-order theorem-proving environment,”Journal of Formal System Design, 2(2):165–230, 1993.
Schneider, K., Kumar, R. and Kropf, Th., “The FAUST prover,” in D. Kapur, editor,11th Conference on Automated Deduction, number 607 in Lecture Notes in Computer Science, 766–770, Springer Verlag, Albany, New York, 1992.
Gentzen, G., “Untersuchungen über das logisches Schließen,”Mathematische Zeitschrift, 1:176–210, 1935.
Andrews, P.B., “Refutations by matings,”Journal of the ACM, 28(2):193–214, April 1981.
Bibel, W., “Matings and matrices,”Communications of the ACM, 26(11):844–852, 1983.
Ebbinghaus, H.D., Flum, J. and Thomas, W.,Einführung in die mathematische Logik, Wissenschaftliche Buchgesellschaft Darmstadt, 1978.
Shoenfield, J.R.,Mathematical Logic, Addison-Wesley, 1967.
Fitting, M.,First-Order Logic and Automated Theorem Proving, Springer Verlag, 1990.
Fitting, M.,Proof Methods for Modal and Intuitionistic Logic, Reidel Publishing Company, 1983.
Eder, E.,On the relative complexities of first order calculi, Vieweg Verlag, 1991.
Agostino, M. d., “Are Tableaux an Improvement of Truth-Tables? Cut-Free Proofs and Bivalence,”Journal of Logic, Language, and Information, 1(3):127–139, 1992.
Robinson, J.A., “A machine oriented logic based on the resolution principle,”Journal of Automated Reasoning, 12(1):23–41, 1965.
Paterson, M.S. and Wegman, M.N., “Linear unification,”Journal of Computer and System Sciences, 16:181–186, 1978.
Martelli, A. and Monanari, M., “An efficient unification algorithm,”ACM TOPLAS, 4:258–282, 1982.
Champeaux, D. de, About the Paterson-Wegman unification algorithm,Journal of Computer and System Sciences, 32:79–90, 1986.
Corbin, J. and Bidoit, M., “A rehabilitation of Robinson's unification algorithm,”Information Processing, pages 909–914, 1983.
Beth, E.W., “Semantic entailment and formal derivability,”Medlingen der Koninklijke Nederlandse Akademic van Wetenschapen, 18(13):309–342, 1955.
Smullyan, R.M.,First Order Logic, Springer Verlag, 1968.
Fitting, M.C., “First-order modal tableaux,”Journal of Automated Reasoning, 4:191–213, 1988.
Broda, K.,The Application of Semantic Tableaux with Unification to Automated Deduction. Ph.D thesis, Department of Computing, Imperial College, 1991.
Posegga, J. and Schneider, K., “Deduction with first-order BDDs,”Internal report, Max-Planck-Institut für Informatik, 1993. Proc. of Second Workshop on Theorem Proving with analytic Tableaux and Related Methods.
Schneider, K., Kumar, R. and Kropf, Th., “Hardware verification with first-order BDD's” inConference on Computer Hardware Dscription Languages, 1993.
Pelletier, F.J., “Seventy-five problems for testing automatic theorem provers.”Journal of Automated Reasoning, 2:191–216, 1986.
Kumar, R., Kropf, Th. and Schneider, K., “Integrating a first-order automatic prover in the HOL environment,” inInternational Workshop on the HOL Theorem Proving System and its Applications, pages 170–176. IEEE Press, 1991.
Hähnle, R. and Schmitt, P., “The liberalized δ-rule,”Journal of Automated Reasoning, 1993.
Kowalski, R., “A proof procedure using connection graphs,”Journal of the ACM, 22(4):572–595, 1975.
Wrightson, G., “Semantic tableaux with links,” inAI'87 Conference, 1987.
Author information
Authors and Affiliations
Additional information
This work has been partly financed by german national grant under the project Automated System Design, SFB No. 358.
Rights and permissions
About this article
Cite this article
Schneider, K., Kumar, R. & Kropf, T. Accelerating tableaux proofs using compact representations. Form Method Syst Des 5, 145–176 (1994). https://doi.org/10.1007/BF01384237
Issue Date:
DOI: https://doi.org/10.1007/BF01384237