| Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers. C Benzmüller, BW Paleo ECAI 263, 93-98, 2014 | 115 | 2014 |
| The inconsistency in Gödel's ontological argument: A success story for ai in metaphysics C Benzmüller, BW Paleo Proceedings of the Twenty-Fifth International Joint Conference on Artificial …, 2016 | 78 | 2016 |
| Chimeric ledgers: Translating and unifying utxo-based and account-based cryptocurrencies J Zahnentferner Cryptology ePrint Archive, 2018 | 66 | 2018 |
| Exploiting symmetry in SMT problems D Déharbe, P Fontaine, S Merz, B Woltzenlogel Paleo International Conference on Automated Deduction, 222-236, 2011 | 58 | 2011 |
| Herbrand sequent extraction S Hetzl, A Leitsch, D Weller, B Woltzenlogel Paleo Intelligent Computer Mathematics: 9th International Conference, AISC 2008 …, 2008 | 50 | 2008 |
| Computer-assisted analysis of the Anderson–Hájek ontological controversy C Benzmüller, L Weber, B Woltzenlogel Paleo Logica Universalis 11 (1), 139-151, 2017 | 49 | 2017 |
| Interacting with modal logics in the coq proof assistant C Benzmüller, B Woltzenlogel Paleo International Computer Science Symposium in Russia, 398-411, 2015 | 40 | 2015 |
| Compression of propositional resolution proofs via partial regularization P Fontaine, S Merz, B Woltzenlogel Paleo Automated Deduction–CADE-23: 23rd International Conference on Automated …, 2011 | 35 | 2011 |
| Higher-order modal logics: Automation and applications C Benzmüller, B Woltzenlogel Paleo Reasoning Web International Summer School, 32-74, 2015 | 32 | 2015 |
| Gödel’s God in Isabelle/HOL C Benzmüller, BW Paleo Archive of Formal Proofs 2013, 2013 | 29 | 2013 |
| Atomic cut introduction by resolution: Proof structuring and compression B Woltzenlogel Paleo International Conference on Logic for Programming Artificial Intelligence …, 2010 | 27 | 2010 |
| Quantifier inference rules for SMT proofs D Déharbe, P Fontaine, BW Paleo First International Workshop on Proof eXchange for Theorem Proving-PxTP 2011, 2011 | 25 | 2011 |
| PROOFTOOL: a GUI for the GAPT framework C Dunchev, A Leitsch, T Libal, M Riener, M Rukhaia, D Weller, ... arXiv preprint arXiv:1307.1942, 2013 | 22 | 2013 |
| Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning J Slaney, B Woltzenlogel Paleo Journal of Automated Reasoning 60, 133-156, 2018 | 21 | 2018 |
| An approximate gazetteer for GATE based on levenshtein distance BW Paleo Twelfth ESSLLI Student Session, 197, 2007 | 21 | 2007 |
| Formalization, Mechanization and Automation of G\" odel's Proof of God's Existence C Benzmüller, BW Paleo arXiv preprint arXiv:1308.4526, 2013 | 20 | 2013 |
| Compression of propositional resolution proofs by lowering subproofs J Boudou, B Woltzenlogel Paleo International Conference on Automated Reasoning with Analytic Tableaux and …, 2013 | 19 | 2013 |
| Herbrand Sequent Extraction BW Paleo VDM Publishing, 2008 | 19 | 2008 |
| Skeptik: A proof compression system J Boudou, A Fellner, B Woltzenlogel Paleo International Joint Conference on Automated Reasoning, 374-380, 2014 | 16 | 2014 |
| An object-logic explanation for the inconsistency in Gödel’s ontological theory C Benzmüller, BW Paleo KI, 244-250, 2016 | 15 | 2016 |
