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

Related Items (1)

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

This page was built for publication: Avoiding duplicate proofs with the foothold refinement