Increasing the efficiency of automated theorem proving

DOI10.1080/11663081.1995.10510841MaRDI QIDQ4835513zbMATH OpenOpenAlexFDO

Authors G. Aguilera, M. Ojeda, I. P. de Guzmán

Publication date 13 December 1995

Published in Journal of Applied Non-Classical Logics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1080/11663081.1995.10510841

zbMATH Keywords

automated theorem prover

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 3986666
• Automated theorem proving methods
• Proof simplification and automated theorem proving
• scientific article; zbMATH DE number 4043814
• Another look at automated theorem-proving
• scientific article; zbMATH DE number 49488
• scientific article; zbMATH DE number 1100750
• scientific article; zbMATH DE number 3938595
• scientific article; zbMATH DE number 3881899

Cites work

• scientific article; zbMATH DE number 3976991 (Why is no real title available?)
• scientific article; zbMATH DE number 49746 (Why is no real title available?)
• scientific article; zbMATH DE number 194631 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• scientific article; zbMATH DE number 3057869 (Why is no real title available?)
• Automated Theorem Proving: After 25 Years
• Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions
• On finding common subtrees
• Seventy-five problems for testing automatic theorem provers

Cited in

(10)

• Improving automation for higher-order proof steps
• scientific article; zbMATH DE number 4033137 (Why is no real title available?)
• scientific article; zbMATH DE number 3986666 (Why is no real title available?)
• Refinements to depth-first iterative-deepening search in automatic theorem proving
• scientific article; zbMATH DE number 4104409 (Why is no real title available?)
• Temporal reasoning over linear discrete time
• A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
• A first polynomial non-clausal class in many-valued logic
• scientific article; zbMATH DE number 4061193 (Why is no real title available?)
• scientific article; zbMATH DE number 1761418 (Why is no real title available?)

Describes a project that uses

Uses Software

• TAS

This page was built for publication: Increasing the efficiency of automated theorem proving

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