A Certified Polynomial-Based Decision Procedure for Propositional Logic
| Autor: | Inmaculada Medina-Bulo, Francisco Palomo-Lozano, José A. Alonso-Jiménez |
|---|---|
| Přispěvatelé: | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
| Rok vydání: | 2001 |
| Předmět: |
Discrete mathematics
Propositional variable Polynomial Well-formed formula Polynomial ring ACL2 Propositional calculus Mathematical proof Algebra Automated theorem proving TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computer Science::Logic in Computer Science computer Mathematics computer.programming_language |
| Zdroj: | idUS. Depósito de Investigación de la Universidad de Sevilla instname Lecture Notes in Computer Science ISBN: 9783540425250 TPHOLs |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|