Splitting and reduction heuristics in automatic theorem proving

DOI10.1016/0004-3702(71)90004-XMaRDI QIDQ2547495zbMATH OpenOpenAlexFDO

Authors 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)

Cites work

• A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
• Experiments with a heuristic theorem-proving program for predicate calculus with equality
• scientific article; zbMATH DE number 5872252 (Why is no real title available?)
• scientific article; zbMATH DE number 3142195 (Why is no real title available?)
• scientific article; zbMATH DE number 3286022 (Why is no real title available?)
• scientific article; zbMATH DE number 3339447 (Why is no real title available?)
• scientific article; zbMATH DE number 3349331 (Why is no real title available?)
• Splitting and reduction heuristics in automatic theorem proving

Cited in

(21)

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

This page was built for publication: Splitting and reduction heuristics in automatic theorem proving

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