SLWV- A Logic Programing Theorem Prover
|
Descargar SCORM
¡Sea el primero en solicitar este recurso!
Para poder solicitar este recurso debe identificarse como usuario de la biblioteca
|
| |
Ver
Detalles del recurso
|
|
|
SLWV- A Logic Programing Theorem Prover
|
| Id. |
47166153 |
| Idioma |
inglés
|
| Titulo |
SLWV- A Logic Programing Theorem Prover |
| Autor(es) |
Luis Moniz Pereira
Luis Caires
José Alferes
Ai Centre Uninova
|
| Localización |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.65.7459
|
| Versión |
1.0 |
| Estado |
Final
|
| Descripción |
Abstract: The purpose of this work is to define a theorem prover that retains the procedural aspects of logic programing. The proof system we propose (SLWV 1 resolution) is defined for a set of clauses in the implicational form (keeping to the form of logic programs), not requiring contrapositives, and has an execution method that respects the execution order of literals in a clause, preserving the procedural flavor of logic programming. SLWV resolution can be seen as a combination of SL-resolution [Chan73] and case-analysis, that admits a form of linear derivation. We prove its soundness and completeness, give it an operational semantics by defining a standard derivation, and produce an implementation. Our work can be seen as an extension to logic programs that goes beyond normal programs, as defined in [Lloy87], and thus beyond(positive) definite clause programming, by allowing also definite negative heads. Thus we admit program clauses with both positive and (classically) negated atoms conjoined in the body, and at most one literal as its head (clauses with disjunctions of literals in the head are transformed into a single clause of that form). As this approach does not require alternative clause contrapositives, it provides for better control over the search space. We provide a method of execution keeping to the implicational clausal form of program statements typical of Prolog (without the use of clause contrapositives), adding an increased expressiveness, but at a tolerable computational cost for regular Prolog programs. The implementation relies on the source program being preprocessed into directly executable Prolog. Since preprocessing only involves the addition of three additional variables to each predicate definition while keeping the overall program structure untouched, a directly recognizable execution pattern that mimics Prolog is obtained: this can be useful in debugging.
|
| Tipo |
application/pdf
|
| Palabras clave |
Logic Programming
|
| 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://centria.di.fct.unl.pt/~lmp/publications/online-papers/elp92.pdf
[References] 10.1.1.47.3057
|
| Fecha de contribución |
25-ago-2009 |
| Contacto |
|
|
|
|
|
Valoración de los usuarios
No hay ninguna valoración para este recurso. Sea el primero en
valorar este recurso.
|
|
|
|
