Non-Horn clause logic programming

DOI10.1016/S0004-3702(97)00007-6zbMath1017.68507OpenAlexW2001027846MaRDI QIDQ1402738

Xumin Nie

Publication date: 28 August 2003

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0004-3702(97)00007-6

zbMATH Keywords

Logic programmingAutomated reasoningNon-Horn clause

Mathematics Subject Classification ID

Logic programming (68N17)

Related Items

Predicate Completion for non-Horn Clause Sets, Renaming a set of non-Horn clauses

Uses Software

• SETHEO

Cites Work

• Near-Horn prolog and beyond
• Depth-first iterative-deepening: An optimal admissible tree search
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• Non-Horn clause logic programming without contrapositives
• A simplified problem reduction format
• SETHEO: A high-performance theorem prover
• A Prolog technology theorem prover: A new exposition and implementation in Prolog
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• Near-Horn Prolog and the ancestry family of procedures
• A sequent-style model elimination strategy and a positive refinement
• A comparison of three PROLOG extensions
• Renaming a Set of Clauses as a Horn Set
• The search efficiency of theorem proving strategies
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item