Problems and Experiments for and with Automated Theorem-Proving Programs

DOI10.1109/TC.1976.1674696zbMath0329.68075OpenAlexW1974462798MaRDI QIDQ4095910

Lawrence A. Wos, John D. McCharen, Ross A. Overbeek

Publication date: 1976

Published in: IEEE Transactions on Computers (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1109/tc.1976.1674696

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

Related Items (19)

On solving the equality problem in theories defined by Horn clauses ⋮ The rue theorem-proving system: The complete set of LIM+ challenge problems ⋮ Automated production of traditional proofs in solid geometry ⋮ Hierarchical deduction ⋮ A learning procedure for mathematics. ⋮ Seventy-five problems for testing automatic theorem provers ⋮ The anatomy of vampire. Implementing bottom-up procedures with code trees ⋮ The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 ⋮ Automated production of traditional proofs for theorems in Euclidean geometry. I: The Hilbert intersection point theorems ⋮ The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 ⋮ A review and prospect of readable machine proofs for geometry theorems ⋮ Experiments with resolution-based theorem-proving algorithms ⋮ Retrieving geometric information from images: the case of hand-drawn diagrams ⋮ The TPTP problem library ⋮ A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ Uniform strategies: The CADE-11 theorem proving contest ⋮ The problem of reasoning by case analysis

This page was built for publication: Problems and Experiments for and with Automated Theorem-Proving Programs