Splitting and reduction heuristics in automatic theorem proving

DOI10.1016/0004-3702(71)90004-XzbMath0221.68052OpenAlexW1996158986MaRDI QIDQ2547495

W. W. Bledsoe

Publication date: 1971

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

Full work available at URL: https://doi.org/10.1016/0004-3702(71)90004-x

Mathematics Subject Classification ID

Artificial intelligence (68T99)

Related Items

A fully automatic theorem prover with human-style output, Set theory in first-order logic: Clauses for Gödel's axioms, A structure-preserving clause form translation, Automated theorem proving in mathematics., Man-machine theorem proving in graph theory, MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics, Using tactics to reformulate formulae for resolution theorem proving, Automatic theorem proving. II, The practicality of generating semantic trees for proofs of unsatisfiability, A simplified problem reduction format, Complexity of resolution proofs and function introduction, First-Order Resolution Methods for Modal Logics, A relaxation approach to splitting in an automatic theorem prover, Non-resolution theorem proving, Milestones from the Pure Lisp Theorem Prover to ACL2, Towards the automation of set theory and its logic, Splitting and reduction heuristics in automatic theorem proving, Computer proofs of limit theorems, A man-machine theorem-proving system

Cites Work

• Splitting and reduction heuristics in automatic theorem proving
• Experiments with a heuristic theorem-proving program for predicate calculus with equality
• A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item