Finding resolution proofs and using duplicate goals in AND/OR trees

DOI10.1016/S0020-0255(71)80013-0zbMath0226.68043MaRDI QIDQ2549243

James R. Slagle, Deena A. Koniver

Publication date: 1971

Published in: Information Sciences (Search for Journal in Brave)

Mathematics Subject Classification ID

Software, source code, etc. for problems pertaining to computer science (68-04)

Related Items

An admissible and optimal algorithm for searching AND/OR graphs, Theorem proving with variable-constrained resolution, Representations of the language recognition problem for a theorem prover

Cites Work

• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• A Machine-Oriented Logic Based on the Resolution Principle
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Theorem-Proving for Computers: Some Results on Resolution and Renaming
• Experiments With a Multipurpose, Theorem-Proving Heuristic Program
• Experiments in automatic learning for a multipurpose hueristic program
• A Heuristic Program that Solves Symbolic Integration Problems in Freshman Calculus
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item