Foundations of equational logic programming
From MaRDI portal
Publication:1801319
zbMath0688.68004MaRDI QIDQ1801319
Publication date: 5 June 1993
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
narrowingtransformation rulesparamodulationequational Horn theorylazy resolutionuniversal unification
Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items
An optimal narrowing strategy for general canonical systems, Knuth-bendix completion of horn clause programs for restricted linear resolution and paramodulation, Constrained equational deduction, Completeness results for basic narrowing, A Finite Representation of the Narrowing Space, Detecting redundant narrowing derivations by the LSE-SL reducibility test, On narrowing, refutation proofs and constraints, Regular substitution sets: A means of controlling E-unification, Default reasoning by deductive planning, General \(E\)-unification with eager variable elimination and a nice cycle rule, Incremental constraint satisfaction for equational logic programming, A Debugging Scheme for Functional Logic Programs1 1This work has been partially supported by CICYT under grant TIC2001-2705-C03-01, by Acción Integrada Hispano-Italiana HI2000-0161, Acción Integrada Hispano-Alemana HA2001-0059 and by Generalitat Valenciana under grant GV01-424., An integrated framework for the diagnosis and correction of rule-based programs, Linear and unit-resulting refutations for Horn theories, Higher order conditional rewriting and narrowing, An introduction to category-based equational logic, Lazy narrowing: Strong completeness and eager variable elimination (extended abstract), Cartesian closed categories of domains and the space proj(D), Modular Termination of Basic Narrowing, Conditional equational theories and complete sets of transformations, A new deductive approach to planning, A semantic framework for open processes, A compositional semantic basis for the analysis of equational Horn programs, Lazy narrowing: strong completeness and eager variable elimination, Loop detection in term rewriting using the eliminating unfoldings, Functional Logic Programming in Maude, Functional Logic Programming: From Theory to Curry, Equality and abductive residua for Horn clauses, Termination of Narrowing in Left-Linear Constructor Systems, Conditional narrowing modulo a set of equations, Termination of narrowing revisited, Declarative Debugging of Functional Logic Programs1 1This work has been partially supported by CICYT under grant TIC2001-2705-C03-01, by Accóon Integrada Hispano-Italiana HI2000-0161 and by Generalitat Valenciana under grant GV01-424., A derived algorithm for evaluating \(\varepsilon\)-expressions over abstract sets, Termination by absence of infinite chains of dependency pairs