A relaxation approach to splitting in an automatic theorem prover

DOI10.1016/0004-3702(75)90014-4MaRDI QIDQ1215411zbMATH OpenOpenAlexFDO

Authors Arthur J. Nevins

Publication date 1975

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/1721.1/6217

Mathematics Subject Classification ID

Algorithms in computer science (68W99)

Cites work

• A Human Oriented Logic for Automatic Theorem-Proving
• A unification algorithm for typed -calculus
• Computer proofs of limit theorems
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• Experiments with a heuristic theorem-proving program for predicate calculus with equality
• Plane geometry theorem proving using forward chaining
• REF-ARF: A system for solving problems stated as procedures
• Splitting and reduction heuristics in automatic theorem proving

Cited in

(4)

• Automatic theorem proving in set theory
• Plane geometry theorem proving using forward chaining
• Non-resolution theorem proving
• \({\mathcal Z}\)-match: An inference rule for incrementally elaborating set instantiations

This page was built for publication: A relaxation approach to splitting in an automatic theorem prover

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