A Proof System and a Decision Procedure for Equality Logic
|
Descargar SCORM
Este recurso ha sido solicitado 1 veces (0 veces en los últimos 31 días).
Para poder solicitar este recurso debe identificarse como usuario de la biblioteca
|
| |
Ver
Detalles del recurso
|
|
|
A Proof System and a Decision Procedure for Equality Logic
|
| Id. |
45700736 |
| Idioma |
inglés
|
| Titulo |
A Proof System and a Decision Procedure for Equality Logic |
| Autor(es) |
Olga Tveretina
Hans Zantema
|
| Localización |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.6017
|
| Versión |
1.0 |
| Estado |
Final
|
| Descripción |
Abstract. We give an approach for deciding satisfiability of equality logic formulas (E-SAT) in conjunctive normal form. Central in our approach is a single proof rule called equality resolution (ER). For this single rule we prove soundness and completeness. Based on this rule we propose a complete procedure for E-SAT and prove its correctness. Applying our procedure on a variation of the pigeon hole formula yields a polynomial complexity contrary to earlier approaches to E-SAT. Parts of the theory we developed for proving completeness of the proof rule and the algorithm are of interest in itself: we give techniques for removing clauses preserving unsatisfiability, and we give a general theorem globalizing a local commutation criterion for different proof systems.
|
| Tipo |
application/pdf
|
| Palabras clave |
equality logic
|
| Tipo de recurso |
Texto Narrativo
|
| Tipo de Interactividad |
Expositivo
|
| Nivel de Interactividad |
muy bajo
|
| Audiencia |
Estudiante
Profesor
Autor
|
| Estructura |
Atomic |
| Coste |
no
|
| Copyright |
sí
|
|
Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
| Formatos |
application/pdf
|
| Requerimientos técnicos |
Browser: Any
|
| Relación |
[IsBasedOn] http://alexandria.tue.nl/extra1/wskrap/publichtml/200302.pdf
[References] 10.1.1.47.3263
[References] 10.1.1.25.9103
[References] 10.1.1.52.1007
[References] 10.1.1.36.2061
[References] 10.1.1.2.6310
[References] 10.1.1.36.2580
[References] 10.1.1.3.461
[References] 10.1.1.67.2738
[References] 10.1.1.69.3090
[References] 10.1.1.122.2056
|
| Fecha de contribución |
27-sep-2009 |
| Contacto |
|
|
|
|
|
Valoración de los usuarios
No hay ninguna valoración para este recurso. Sea el primero en
valorar este recurso.
|
|
|
|
