Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover
- 17 June 2020
- journal article
- research article
- Published by Springer Nature in Journal of Automated Reasoning
- Vol. 64 (7) , 1169-1195
Abstract
No abstract availableKeywords
Funding Information
- Danmarks Tekniske Universitet
- Horizon 2020 Framework Programme (700321)
- Deutsche Forschungsgemeinschaft (NI 491/14-1)
- Horizon 2020 Framework Programme (713999)
- Nederlandse Organisatie voor Wetenschappelijk Onderzoek (016.Vidi.189.037)
- Deutsche Forschungsgemeinschaft (1480)
This publication has 37 references indexed in Scilit:
- Lambda, the ultimate TAACM SIGPLAN Notices, 2009
- First-order theorem proving using conditional rewrite rules2005
- Combining Superposition, Sorts and Splitting2001
- Paramodulation-Based Theorem Proving2001
- Resolution Theorem Proving2001
- Ordered chaining calculi for first-order theories of transitive relationsJournal of the ACM, 1998
- Rewrite-based Equational Theorem Proving with Selection and SimplificationJournal of Logic and Computation, 1994
- Towards mechanical metamathematicsJournal of Automated Reasoning, 1985
- Proving termination with multiset orderingsCommunications of the ACM, 1979
- Proving Theorems with the Modification MethodSIAM Journal on Computing, 1975