Near-Horn Prolog and the ancestry family of procedures

DOI10.1007/BF01530821zbMath0855.68014OpenAlexW2091615084MaRDI QIDQ1924724

Donald W. Loveland, David W. Reed

Publication date: 24 November 1996

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01530821

zbMATH Keywords

near-Horn Prolog procedurespositive refinement of model elimination

Mathematics Subject Classification ID

Logic programming (68N17)

Related Items

Non-Horn clause logic programming, Computing answers with model elimination, Renaming a set of non-Horn clauses

Uses Software

• SETHEO
• PARTHEO
• METEOR

Cites Work

• Unnamed Item
• Unnamed Item
• Near-Horn prolog and beyond
• Non-Horn clause logic programming without contrapositives
• An extension to linear resolution with selection function
• A simplified problem reduction format
• SETHEO: A high-performance theorem prover
• Linear resolution with selection function
• A sequent-style model elimination strategy and a positive refinement
• N-Prolog: An extension of Prolog with hypothetical implications. I.
• N-Prolog: An extension of prolog with hypothetical implication. II. Logical foundations, and negation as failure
• A comparison of three PROLOG extensions
• An Implementation of the Model Elimination Proof Procedure
• Mechanical Theorem-Proving by Model Elimination
• A Simplified Format for the Model Elimination Theorem-Proving Procedure