Refinements to depth-first iterative-deepening search in automatic theorem proving

DOI10.1016/0004-3702(89)90011-8MaRDI QIDQ582116zbMATH OpenOpenAlexFDO

Authors Xumin Nie, David A. Plaisted

Publication date 1989

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0004-3702(89)90011-8

zbMATH Keywords

complexitydepth iterative-deepening seachpriority listpriority system

Mathematics Subject Classification ID

Searching and sorting (68P10) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• Interaction and depth against nondeterminism in proof search
• Increasing the efficiency of automated theorem proving
• scientific article; zbMATH DE number 3938595
• Depth-first proof search without backtracking for free-variable clausal tableaux
• The search efficiency of theorem proving strategies
• scientific article; zbMATH DE number 1113998
• Automating Inductive Proofs Using Theory Exploration
• scientific article; zbMATH DE number 3986666
• Towards Systematic Analysis of Theorem Provers Search Spaces: First Steps
• About the Completeness of Depth-First Proof-Number Search

Cites work

• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• Complexity and related enhancements for automated theorem-proving programs
• Depth-first iterative-deepening: An optimal admissible tree search
• Hierarchical deduction
• scientific article; zbMATH DE number 4180829 (Why is no real title available?)
• scientific article; zbMATH DE number 3347627 (Why is no real title available?)
• Non-Horn clause logic programming without contrapositives
• Probabilistic analysis of the complexity of A*

Cited in

(2)

• Deep Proof Search in MELL
• Execution of logic programs by iterative-deepening A\(^*\) SLD-tree search

Describes a project that uses

Uses Software

• PARTHENON

This page was built for publication: Refinements to depth-first iterative-deepening search in automatic theorem proving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q582116)