Limited resource strategy in resolution theorem proving

DOI10.1016/S0747-7171(03)00040-3zbMath1023.68089MaRDI QIDQ1404979

Alexandre Riazanov, Andrei Voronkov

Publication date: 25 August 2003

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

resolutionautomated theorem provinglimited resource strategyOTTER saturation algorithm

Mathematics Subject Classification ID

Related Items

Vampire with a brain is a good ITP hammer, \textsf{lazyCoP}: lazy paramodulation meets neurally guided search, Eliminating models during model elimination, Cooperating Proof Attempts, Playing with AVATAR, A multi-clause dynamic deduction algorithm based on standard contradiction separation rule, Contradiction separation based dynamic multi-clause synergized automated deduction, Citius altius fortius, Automation methods for logical derivation and their application in the control of dynamic and intelligent systems, Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving, Improving ENIGMA-style clause selection while learning from history, Old or heavy? Decaying gracefully with age/weight shapes, Layered clause selection for theory reasoning (short paper), The 10th IJCAR automated theorem proving system competition – CASC-J10

Uses Software

• SETHEO
• OTTER
• VAMPIRE
• SPASS
• E-SETHEO
• Waldmeister
• DISCOUNT
• Bliksem

Cites Work

• Logic programming and automated reasoning. International conference, LPAR `92, St. Peterburg, Russia, July 15--20, 1992. Proceedings
• The CADE-16 ATP system competition
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item