Repositorio de producción científica de la Universidad de Sevilla

A Certified Polynomial-Based Decision Procedure for Propositional Logic

 

Advanced Search
 
Opened Access A Certified Polynomial-Based Decision Procedure for Propositional Logic
Cites

Show item statistics
Icon
Export to
Author: Medina Bulo, Inmaculada
Palomo Lozano, Francisco
Alonso Jiménez, José Antonio
Department: Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
Date: 2001
Published in: TPHOLs 2001: 14th International Conference on Theorem Proving in Higher Order Logics (2001), p 297-312
ISBN/ISSN: 978-3-540-42525-0
0302-9743
Document type: Presentation
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.
Cite: Medina Bulo, I., Palomo Lozano, F. y Alonso Jiménez, J.A. (2001). A Certified Polynomial-Based Decision Procedure for Propositional Logic. En TPHOLs 2001: 14th International Conference on Theorem Proving in Higher Order Logics (297-312), Edinburgh, Scotland: Springer.
Size: 319.2Kb
Format: PDF

URI: https://hdl.handle.net/11441/86601

DOI: 10.1007/3-540-44755-5_21

See editor´s version

This work is under a Creative Commons License: 
Attribution-NonCommercial-NoDerivatives 4.0 Internacional

This item appears in the following Collection(s)