A Certified Polynomial-Based Decision Procedure for Propositional Logic

Medina Bulo, Inmaculada; Palomo Lozano, Francisco; Alonso Jiménez, José Antonio

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

Ponencia

dc.creator	Medina Bulo, Inmaculada	es
dc.creator	Palomo Lozano, Francisco	es
dc.creator	Alonso Jiménez, José Antonio	es
dc.date.accessioned	2019-05-21T09:25:06Z
dc.date.available	2019-05-21T09:25:06Z
dc.date.issued	2001
dc.identifier.citation	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.
dc.identifier.isbn	978-3-540-42525-0	es
dc.identifier.issn	0302-9743	es
dc.identifier.uri	https://hdl.handle.net/11441/86601
dc.description.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.	es
dc.format	application/pdf	es
dc.language.iso	eng	es
dc.publisher	Springer	es
dc.relation.ispartof	TPHOLs 2001: 14th International Conference on Theorem Proving in Higher Order Logics (2001), p 297-312
dc.rights	Attribution-NonCommercial-NoDerivatives 4.0 Internacional	*
dc.rights.uri	http://creativecommons.org/licenses/by-nc-nd/4.0/	*
dc.title	A Certified Polynomial-Based Decision Procedure for Propositional Logic	es
dc.type	info:eu-repo/semantics/conferenceObject	es
dcterms.identifier	https://ror.org/03yxnpp24
dc.type.version	info:eu-repo/semantics/submittedVersion	es
dc.rights.accessRights	info:eu-repo/semantics/openAccess	es
dc.contributor.affiliation	Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial	es
dc.relation.publisherversion	https://link.springer.com/chapter/10.1007/3-540-44755-5_21	es
dc.identifier.doi	10.1007/3-540-44755-5_21	es
idus.format.extent	16	es
dc.publication.initialPage	297	es
dc.publication.endPage	312	es
dc.eventtitle	TPHOLs 2001: 14th International Conference on Theorem Proving in Higher Order Logics	es
dc.eventinstitution	Edinburgh, Scotland	es
dc.relation.publicationplace	Berlin	es
dc.identifier.sisius	6514428	es

Ficheros	Tamaño	Formato	Ver	Descripción
A Certified Polynomial-Based ...	319.2Kb	[PDF]	Ver/Abrir

Este registro aparece en las siguientes colecciones

Ponencias (Ciencias de la Computación e Inteligencia Artificial)

Mostrar el registro sencillo del ítem

Excepto si se señala otra cosa, la licencia del ítem se describe como: Attribution-NonCommercial-NoDerivatives 4.0 Internacional