A relaxation approach to splitting in an automatic theorem prover
From MaRDI portal
Publication:1215411
DOI10.1016/0004-3702(75)90014-4zbMath0301.68087OpenAlexW1995624888MaRDI QIDQ1215411
Publication date: 1975
Published in: Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: http://hdl.handle.net/1721.1/6217
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (4)
Plane geometry theorem proving using forward chaining ⋮ Non-resolution theorem proving ⋮ Automatic theorem proving in set theory ⋮ \({\mathcal Z}\)-match: An inference rule for incrementally elaborating set instantiations
Cites Work
- Plane geometry theorem proving using forward chaining
- A unification algorithm for typed \(\overline\lambda\)-calculus
- REF-ARF: A system for solving problems stated as procedures
- Splitting and reduction heuristics in automatic theorem proving
- Experiments with a heuristic theorem-proving program for predicate calculus with equality
- Computer proofs of limit theorems
- A Human Oriented Logic for Automatic Theorem-Proving
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
This page was built for publication: A relaxation approach to splitting in an automatic theorem prover
