A relaxation approach to splitting in an automatic theorem prover

DOI10.1016/0004-3702(75)90014-4zbMATH Open0301.68087OpenAlexW1995624888MaRDI QIDQ1215411FDOQ1215411

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

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

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)