Herbrand Sequent Extraction. - Stefan Hetzl; Alexander Leitsch; Daniel Weller 001; Bruno Woltzenlogel Paleo (AISC/MKM/Calculemus, 2008)

Transforming and Analyzing Proofs in the CERES-System. - Stefan Hetzl; Alexander Leitsch; Daniel Weller 001; Bruno Woltzenlogel Paleo (LPAR Workshops, 2008)

A Clausal Approach to Proof Analysis in Second-Order Logic. - Stefan Hetzl; Alexander Leitsch; Daniel Weller 001; Bruno Woltzenlogel Paleo (LFCS, 2009)

System Description: The Proof Transformation System CERES. - Tsvetan Dunchev; Alexander Leitsch; Tomer Libal; Daniel Weller 001; Bruno Woltzenlogel Paleo (IJCAR, 2010)

Atomic Cut Introduction by Resolution: Proof Structuring and Compression. - Bruno Woltzenlogel Paleo (LPAR (Dakar), 2010)

Exploiting Symmetry in SMT Problems. - David Déharbe; Pascal Fontaine; Stephan Merz; Bruno Woltzenlogel Paleo (CADE, 2011)

Compression of Propositional Resolution Proofs via Partial Regularization. - Pascal Fontaine; Stephan Merz; Bruno Woltzenlogel Paleo (CADE, 2011)

Quantifier Inference Rules for SMT proofs. - David Déharbe; Pascal Fontaine; Bruno Woltzenlogel Paleo (PxTP, 2011)

Towards CERes in intuitionistic logic. - Alexander Leitsch; Giselle Reis; Bruno Woltzenlogel Paleo (CSL, 2012)

System Feature Description: Importing Refutations into the GAPT Framework. - Cvetan Dunchev; Alexander Leitsch; Tomer Libal; Martin Riener; Mikheil Rukhaia; Daniel Weller 001; Bruno Woltzenlogel Paleo (PxTP, 2012)

Physics and proof theory. - Bruno Woltzenlogel Paleo (Appl. Math. Comput., 2012)

PROOFTOOL: a GUI for the GAPT Framework. - Cvetan Dunchev; Alexander Leitsch; Tomer Libal; Martin Riener; Mikheil Rukhaia; Daniel Weller 001; Bruno Woltzenlogel Paleo (UITP, 2012)

Contextual Natural Deduction. - Bruno Woltzenlogel Paleo (LFCS, 2013)

Compression of Propositional Resolution Proofs by Lowering Subproofs. - Joseph Boudou; Bruno Woltzenlogel Paleo (TABLEAUX, 2013)

Gödel's God in Isabelle/HOL. - Christoph Benzmueller; Bruno Woltzenlogel Paleo (Arch. Formal Proofs, 2013)

Formalization, Mechanization and Automation of Gödel's Proof of God's Existence. - Christoph Benzmüller; Bruno Woltzenlogel Paleo (CoRR, 2013)

Skeptik: A Proof Compression System. - Joseph Boudou; Andreas Fellner; Bruno Woltzenlogel Paleo (IJCAR, 2014)

Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers. - Christoph Benzmüller; Bruno Woltzenlogel Paleo (ECAI, 2014)

On Logic Embeddings and Gödel's God. - Christoph Benzmüller; Bruno Woltzenlogel Paleo (WADT, 2014)

Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses. - Jan Gorzny; Bruno Woltzenlogel Paleo (CADE, 2015)

Interacting with Modal Logics in the Coq Proof Assistant. - Christoph Benzmüller; Bruno Woltzenlogel Paleo (CSR, 2015)

Implementation and Evaluation of Contextual Natural Deduction for Minimal Logic. - Bruno Woltzenlogel Paleo (Ershov Memorial Conference, 2015)

Higher-Order Modal Logics: Automation and Applications. - Christoph Benzmüller; Bruno Woltzenlogel Paleo (Reasoning Web, 2015)

The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics. - Christoph Benzmüller; Bruno Woltzenlogel Paleo (IJCAI, 2016)

An Expressive Probabilistic Temporal Logic. - Bruno Woltzenlogel Paleo (CoRR, 2016)

Scavenger 0.1: A Theorem Prover Based on Conflict Resolution. - Daniyar Itegulov; John K. Slaney; Bruno Woltzenlogel Paleo (CADE, 2017)

Epsilon Terms in Intuitionistic Sequent Calculus. - Bruno Woltzenlogel Paleo; Giselle Reis (FLAP, 2017)

NP-completeness of small conflict set generation for congruence closure. - Andreas Fellner; Pascal Fontaine; Bruno Woltzenlogel Paleo (Formal Methods Syst. Des., 2017)

Reducing redundancy in cut-elimination by resolution. - Bruno Woltzenlogel Paleo (J. Log. Comput., 2017)

Computer-Assisted Analysis of the Anderson-Hájek Ontological Controversy. - Christoph Benzmüller; L. Weber; Bruno Woltzenlogel Paleo (Logica Universalis, 2017)

Variants of Gödel's Ontological Proof in a Natural Deduction Calculus. - Annika Kanckos; Bruno Woltzenlogel Paleo (Stud Logica, 2017)

Sensala: a Dynamic Semantics System for Natural Language Processing. - Daniyar Itegulov; Ekaterina Lebedeva; Bruno Woltzenlogel Paleo (COLING (Demos), 2018)

Conflict Resolution: A First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning. - John K. Slaney; Bruno Woltzenlogel Paleo (J. Autom. Reason., 2018)

Erratum to: Conflict Resolution: A First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning. - John K. Slaney; Bruno Woltzenlogel Paleo (J. Autom. Reason., 2018)

Complexity of translations from resolution to sequent calculus. - Giselle Reis; Bruno Woltzenlogel Paleo (Math. Struct. Comput. Sci., 2019)

Greedy pebbling for proof space compression. - Andreas Fellner; Bruno Woltzenlogel Paleo (Int. J. Softw. Tools Technol. Transf., 2019)

Partial Regularization of First-Order Resolution Proofs. - Jan Gorzny; Ezequiel Postan; Bruno Woltzenlogel Paleo (GCAI, 2020)

Lifting propositional proof compression algorithms to first-order logic. - Jan Gorzny; Ezequiel Postan; Bruno Woltzenlogel Paleo (J. Log. Comput., 2021)

Stablecoins: Past, Present, and Future. - Ali Nejadmalayeri; Leon Molchanovsky; Bruno Woltzenlogel Paleo; Rodney W. Prescott (FC Workshops, 2023)

Gluon W: A Cryptocurrency Stabilization Protocol. - Bruno Woltzenlogel Paleo; Luca D'Angelo; Mohammad Shaheer; Giselle Reis (IACR Cryptol. ePrint Arch., 2025)