The rue theorem-proving system: The complete set of LIM+ challenge problems

DOI10.1007/BF00881889MaRDI QIDQ1337564zbMATH OpenFDO

Authors Vincent J. Digricoli

Publication date 10 November 1994

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BF00881889

zbMATH Keywords

hyperresolutionparamodulationrestriction strategyRUE hyperrefutations

Mathematics Subject Classification ID

Recommendations

• The limits of tractability in resolution-based propositional proof systems
• The limits of tractability in resolution-based propositional proof systems
• scientific article; zbMATH DE number 4072436
• scientific article; zbMATH DE number 1762830
• AI*IA 2005: Advances in Artificial Intelligence
• The theoretical foundations of LPTP (a logic program theorem prover)
• Theorem proving with bounded rigid E-unification
• Theorem proving as constraint solving with coherent logic
• scientific article; zbMATH DE number 5305114
• scientific article; zbMATH DE number 1136087

Cites work

• Challenge problems in elementary calculus
• Completeness issues in RUE-NRF deduction: The undecidability of viability
• scientific article; zbMATH DE number 4164175 (Why is no real title available?)
• scientific article; zbMATH DE number 3688782 (Why is no real title available?)
• scientific article; zbMATH DE number 3254919 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• Problems and Experiments for and with Automated Theorem-Proving Programs
• Resolution, Refinements, and Search Strategies: A Comparative Study

This page was built for publication: The rue theorem-proving system: The complete set of LIM+ challenge problems

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