A weak allowedness condition that ensures completeness of SLDNF-resolution
Visualitza/Obre
Estadístiques de LA Referencia / Recolecta
Inclou dades d'ús des de 2022
Cita com:
hdl:2117/374664
Tipus de documentText en actes de congrés
Data publicació1990
EditorUniversitat Politècnica de Catalunya. Departament de Llenguatges i Sistemes Informàtics
Condicions d'accésAccés obert
Llevat que s'hi indiqui el contrari, els
continguts d'aquesta obra estan subjectes a la llicència de Creative Commons
:
Reconeixement-NoComercial-SenseObraDerivada 4.0 Internacional
Abstract
The lillowedness condition usually imposed on classes of programs for which general completeness results for SLDNF-resolution have been proved is a very restrictive one and prohibits many important programming constructs. We weaken allowedness by defining a condition that accounts for bindings that will occur when unification takes place. We prove that Kunen's completeness theorems for SLDNF-resolution still hold when allowedness is replaced by this significantly weaker condition. The condition that accounts for the variable bindings may also prove useful to the formal understanding of data.-flow analysis techniques.
CitacióCavedon, L.; Decker, H. A weak allowedness condition that ensures completeness of SLDNF-resolution. A: . Universitat Politècnica de Catalunya. Departament de Llenguatges i Sistemes Informàtics, 1990, p. 153-171.
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
1DAISD_08 A weak allowedness.doc | 346,9Kb | Microsoft Word | Visualitza/Obre |