Abstract
In this paper we present the formalization of a decision procedure for Propositional Logic based on polynomial normalization. This formalization is suitable for its automatic verification in an applicative logic like Acl2. This application of polynomials has been developed by reusing a previous work on polynomial rings [19], showing that a proper formalization leads to a high level of reusability. Two checkers are defined: the first for contradiction formulas and the second for tautology formulas. The main theorems state that both checkers are sound and complete. Moreover, functions for generating models and counterexamples of formulas are provided. This facility plays also an important role in the main proofs. Finally, it is shown that this allows for a highly automated proof development.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aitken, W. E., Constable, R. L., Underwood, J. L.: Metalogical Frameworks II: Developing a Reflected Decision Procedure. J. Automated Reasoning 22(2) (1999)
Boole, G. The Mathematical Analysis of Logic. Macmillan (1847)
Boyer, R. S., Moore, J S.: A Computational Logic. Academic Press (1978)
Boyer, R. S., Moore, J S.: Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures. In: Boyer, R. S., Moore, J S. (eds.): The Correctness Problem in Computer Science. Academic Press (1981)
Boyer, R. S., Moore, J S.: A Computational Logic Handbook. Academic Press. 2nd edn. (1998)
Caldwell, J. L.: Classical Propositional Decidability via Nuprl Proof Extraction. 11th International Conference on Theorem Proving in Higher Order Logics. LNCS 1479 (1998)
Chazarain, J., Riscos, A., Alonso, J. A., Briales, E.: Multi-Valued Logic and Gröbner Bases with Applications to Modal Logic. J. Symbolic Computation 11 (1991)
Harrison, J.: Metatheory and Reflection in Theorem Proving: A Survey and Critique. SRI International Cambridge Computer Science Research Centre. Technical Report CRC-053 (1995)
Harrison, J.: Binary Decision Diagrams as a HOL Derived Rule. The Computer Journal 38 (1995)
Harrison, J.: Stlmarck’s Algorithm as a HOL Derived Rule. 9th International Conference on Theorem Proving in Higher Order Logics. LNCS 1125 (1996)
Hsiang, J.: Refutational Theorem Proving using Term-Rewriting Systems. Artificial Intelligence 25 (1985)
Hsiang, J.: Rewrite Method for Theorem Proving in First-Order Theory with Equality. J. Symbolic Computation 3 (1987)
Hsiang, J., Huang, G. S.: Some Fundamental Properties of Boolean Ring Normal Forms. DIMACS series on Discrete Mathematics and Computer Science: The Satisfiability Problem. AMS (1996)
Kaufmann, M., Moore, J S.: An Industrial Strength Theorem Prover for a Logic Based on Common Lisp. IEEE Trans, on Software Engineering 23(4) (1997)
Kaufmann, M., Manolios, P., Moore, J S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers (2000)
Kaufmann, M., Manolios, P., Moore, J S.: Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers (2000)
Kapur, D., Narendran, P.: An Equational Approach to Theorem Proving in First-Order Predicate Calculus. 9th International Conference on Artificial Intelligence (1985)
Laita, L. M., Roanes-Lozano, E., Ledesma, L., Alonso, J. A.: A Computer Algebra Approach to Verification and Deduction in Many-Valued Knowledge Systems. Soft Computing 3(1) (1999)
Medina-Bulo, I., Alonso-Jiménez, J. A., Palomo-Lozano, F.: Automatic Verification of Polynomial Rings Fundamental Properties in ACL2. ACL2 Workshop 2000 Proceedings, Part A. The University of Texas at Austin, Department of Computer Sciences. Technical Report TR-00-29 (2000)
Medina-Bulo, I., Palomo-Lozano, F., Alonso-Jiménez, J. A.: A Certified Algorithm for Translating Formulas into Polynomials. An ACL2 Approach. International Joint Conference on Automated Reasoning (2001)
Moore, J S.: Introduction to the OBDD Algorithm for the ATP Community. Computational Logic, Inc. Technical Report 84 (1992)
Paulin-Mohring, C., Werner, B.: Synthesis of ML Programs in the System Coq. J. Symbolic Computation 15(5–6) (1993)
Stone, M.: The Theory of Representation for Boolean Algebra. Trans. AMS 40 (1936)
Sumners, R.: Correctness Proof of a BDD Manager in the Context of Satisfiability Checking. ACL2 Workshop 2000 Proceedings, Part A. The University of Texas at Austin, Department of Computer Sciences. Technical Report TR-00-29 (2000)
Théry, L. A Machine-Checked Implementation of Buchberger’s Algorithm. J. Automated Reasoning 26 (2001)
Wu, J., Tan, H.: An Algebraic Method to Decide the Deduction Problem in Prepositional Many-Valued Logics. International Symposium on Multiple-Valued Logics. IEEE Computer Society Press (1994)
Wu, J.: First-Order Polynomial Based Theorem Proving. In: Gao, X., Wang, D. (eds.): Mathematics Mechanization and Applications. Academic Press (1999)
Zhang, H.: A New Strategy for the Boolean Ring Based Approach to First Order Theorem Proving. Department of Computer Science. University of Iowa. Technical Report (1991)
Zhegalkin, I. I.: On a Technique of Evaluation of Propositions in Symbolic Logic. Mat. Sb. 34 (1927)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Medina-Bulo, I., Palomo-Lozano, 1., Alonso-Jiménez, J.A. (2001). A Certified Polynomial-Based Decision Procedure for Propositional Logic. In: Boulton, R.J., Jackson, P.B. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2001. Lecture Notes in Computer Science, vol 2152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44755-5_21
Download citation
DOI: https://doi.org/10.1007/3-540-44755-5_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42525-0
Online ISBN: 978-3-540-44755-9
eBook Packages: Springer Book Archive