Splitting and reduction heuristics in automatic theorem proving
From MaRDI portal
Publication:2547495
DOI10.1016/0004-3702(71)90004-XzbMath0221.68052OpenAlexW1996158986MaRDI QIDQ2547495
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
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
