Oriented Equational Logic Programming is Complete
Identifieur interne : 001883 ( Istex/Curation ); précédent : 001882; suivant : 001884Oriented Equational Logic Programming is Complete
Auteurs : Christopher Lynch [France]Source :
- Journal of Symbolic Computation [ 0747-7171 ] ; 1997.
English descriptors
- Teeft :
- Answer substitution, Answer substitutions, Bachmair, Basic paramodulation, Clause, Completeness, Completeness proof, Completeness result, Completeness results, Conditional, Conditional term, Convergent, Convergent sets, Convergent subset, Correct deletion rule, Deletion, Deletion rules, Dershowitz, Empty clause, Equation resolution, Equational, Equational horn clauses, Equational logic programming, Fair theorem, Fribourg, Functional programming, Ganzinger, General clauses, Goal clause, Goal clauses, Goal paramodulation, Goal paramodulation inference, Goal variables, Ground equations, Ground instance, Ground instances, Hamoen, Horn clauses, Inference, Inference rule, Inference rules, Inference system, Inference systems, Lncs, Logic programming, Model construction, Negative literals, Nieuwenhuis, Paramodulation, Proc, Program clause, Program clauses, Redundant, Redvar, Refutational completeness, Rusinowitch, Selection rule, Selection rules, Smaller clause, Smallest clause, Subgoal, Substitution, Substitution part, Subsumption, Superposition, Superposition inference, Superposition inference rule, Tautology, Tautology deletion.
Abstract
Abstract: We show the completeness of an extension of SLD-resolution to the equational setting. This proves a conjecture of Laurent Fribourg and shows the completeness of an implementation of his. It is the first completeness result for superposition of equational Horn clauses which reduces to SLD resolution in the non-equational case. The inference system proved complete is actually more general than the one of Fribourg, because it allows for a selection rule on program clauses. Our completeness result also has implications for Conditional Narrowing and Basic Conditional Narrowing.
Url:
DOI: 10.1006/jsco.1996.0075
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :001902
Links to Exploration step
ISTEX:6B6B8A0DD975B02065B8B70EFD3E908F5349A350Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Oriented Equational Logic Programming is Complete</title><author><name sortKey="Lynch, Christopher" sort="Lynch, Christopher" uniqKey="Lynch C" first="Christopher" last="Lynch">Christopher Lynch</name><affiliation wicri:level="1"><mods:affiliation>Campus Scientifique, BP 101, INRIA Lorraine et CRIN, 54602 Villers-lés-Nancy, Cedex, France</mods:affiliation><country xml:lang="fr">France</country><wicri:regionArea>Campus Scientifique, BP 101, INRIA Lorraine et CRIN, 54602 Villers-lés-Nancy, Cedex</wicri:regionArea></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:6B6B8A0DD975B02065B8B70EFD3E908F5349A350</idno><date when="1997" year="1997">1997</date><idno type="doi">10.1006/jsco.1996.0075</idno><idno type="url">https://api.istex.fr/ark:/67375/6H6-6P695PGV-G/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001902</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001902</idno><idno type="wicri:Area/Istex/Curation">001883</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Oriented Equational Logic Programming is Complete</title><author><name sortKey="Lynch, Christopher" sort="Lynch, Christopher" uniqKey="Lynch C" first="Christopher" last="Lynch">Christopher Lynch</name><affiliation wicri:level="1"><mods:affiliation>Campus Scientifique, BP 101, INRIA Lorraine et CRIN, 54602 Villers-lés-Nancy, Cedex, France</mods:affiliation><country xml:lang="fr">France</country><wicri:regionArea>Campus Scientifique, BP 101, INRIA Lorraine et CRIN, 54602 Villers-lés-Nancy, Cedex</wicri:regionArea></affiliation></author></analytic><monogr></monogr><series><title level="j">Journal of Symbolic Computation</title><title level="j" type="abbrev">YJSCO</title><idno type="ISSN">0747-7171</idno><imprint><publisher>ELSEVIER</publisher><date type="published" when="1997">1997</date><biblScope unit="volume">23</biblScope><biblScope unit="issue">1</biblScope><biblScope unit="page" from="23">23</biblScope><biblScope unit="page" to="45">45</biblScope></imprint><idno type="ISSN">0747-7171</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0747-7171</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="Teeft" xml:lang="en"><term>Answer substitution</term><term>Answer substitutions</term><term>Bachmair</term><term>Basic paramodulation</term><term>Clause</term><term>Completeness</term><term>Completeness proof</term><term>Completeness result</term><term>Completeness results</term><term>Conditional</term><term>Conditional term</term><term>Convergent</term><term>Convergent sets</term><term>Convergent subset</term><term>Correct deletion rule</term><term>Deletion</term><term>Deletion rules</term><term>Dershowitz</term><term>Empty clause</term><term>Equation resolution</term><term>Equational</term><term>Equational horn clauses</term><term>Equational logic programming</term><term>Fair theorem</term><term>Fribourg</term><term>Functional programming</term><term>Ganzinger</term><term>General clauses</term><term>Goal clause</term><term>Goal clauses</term><term>Goal paramodulation</term><term>Goal paramodulation inference</term><term>Goal variables</term><term>Ground equations</term><term>Ground instance</term><term>Ground instances</term><term>Hamoen</term><term>Horn clauses</term><term>Inference</term><term>Inference rule</term><term>Inference rules</term><term>Inference system</term><term>Inference systems</term><term>Lncs</term><term>Logic programming</term><term>Model construction</term><term>Negative literals</term><term>Nieuwenhuis</term><term>Paramodulation</term><term>Proc</term><term>Program clause</term><term>Program clauses</term><term>Redundant</term><term>Redvar</term><term>Refutational completeness</term><term>Rusinowitch</term><term>Selection rule</term><term>Selection rules</term><term>Smaller clause</term><term>Smallest clause</term><term>Subgoal</term><term>Substitution</term><term>Substitution part</term><term>Subsumption</term><term>Superposition</term><term>Superposition inference</term><term>Superposition inference rule</term><term>Tautology</term><term>Tautology deletion</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We show the completeness of an extension of SLD-resolution to the equational setting. This proves a conjecture of Laurent Fribourg and shows the completeness of an implementation of his. It is the first completeness result for superposition of equational Horn clauses which reduces to SLD resolution in the non-equational case. The inference system proved complete is actually more general than the one of Fribourg, because it allows for a selection rule on program clauses. Our completeness result also has implications for Conditional Narrowing and Basic Conditional Narrowing.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001883 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Curation/biblio.hfd -nk 001883 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Curation
|type= RBID
|clé= ISTEX:6B6B8A0DD975B02065B8B70EFD3E908F5349A350
|texte= Oriented Equational Logic Programming is Complete
}}
| This area was generated with Dilib version V0.6.33. |  |