Avoiding duplicate proofs with the foothold refinement

DOI10.1007/BF01530763zbMath0858.68091MaRDI QIDQ1924821

Bruce D. Spencer

Publication date: 25 March 1997

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

zbMATH Keywords

automated reasoningdisjunctive logic programsSLI resolution

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27)

Related Items

Clause trees: A tool for understanding and implementing resolution in automated reasoning

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• How to avoid the derivation of redundant clauses in reasoning systems
• Seventy-five problems for testing automatic theorem provers
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• A sequent-style model elimination strategy and a positive refinement
• A fixpoint semantics for disjunctive logic programs