profile picture

Bruno Woltzenlogel Paleo

Education

PhD in Computer Science

TU-Vienna (Austria)
10/2007 - 11/2009

MSc in Computational Logic

TU-Dresden (Germany)
TU-Vienna (Austria)
10/2005 - 09/2007

MSc in Computer Science

ITA (Brazil)
01/2005 - 01/2008

Eng. Degree in
Electronics Engineering

ITA (Brazil)
01/2000 - 12/2004

Intro

Welcome to my website. Here you can find partial information about my software projects, publications and activities. To know more, contact me.

Current Software Projects

This is an incomplete list. Only public projects currently led by me are included below:

Scavenger - a theorem prover based on a generalization of conflict-driven clause learning to first-order logic.

Skeptik - a library of algorithms for compressing proofs generated by sat-solvers, smt-solvers and first-order theorem provers.

Agora - a library of algorithms for counting votes in elections.

Computational Philosophy - a collection of logical formalizations (in Coq, Isabelle and TPTP THF) of prominent metaphysical theories and arguments, with a special interest on those requiring higher-order modal logics.

Mind the Word - a multi-browser extension that helps people to learn any new language by partially translating random words into the language they would like to learn, while keeping the translated word in context.

Carbon Footprint - a multi-browser extension that shows how much CO2 is emitted by driving a car on routes suggested by Google Maps and other map services.

Scavenger, Skeptik and Agora are implemented in Scala with Akka (for actor-based concurrency), Scalastyle (for enforcing good coding style), Specs2 (for unit and end-to-end tests), Scalameter (for performance regression tests) and scoverage (to analyze test coverage). Mind the Word and Carbon Footprint are implemented in Javascript, HTML, CSS, using Angular and the browser extension APIs of Google Chrome, Firefox and Safari.

Ongoing and Upcoming Activities

The Encyclopedia of Proof Systems (Editor)

The AOSSIE Google Summer of Code Umbrella Organization (Founder and Org Admin)

QuaD (PC Member)

PxTP (Chair)

EPS (Chair)

Publications

All bibliographical details of my publications can be found in my Publications.bib file. Most of my publications can be downloaded from ResearchGate or Academia. Feel free to request any paper.

Author order is alphabetical by surname

2017

  1. Scavenger EP-0.1 and EP-0.2 [Abstract]. CASC-26 – the CADE-26 ATP System Competition. Itegulov, Daniyar and Padtsiolkin, Uladzislau and Woltzenlogel Paleo, Bruno.

  2. Complexity of Translations from Resolution to Sequent Calculus [Presentation-Only]. Workshop on Proof Exchange for Theorem Proving. Reis, Giselle and Woltzenlogel Paleo, Bruno.

  3. Scavenger 0.1: A Theorem Prover Based on Conflict Resolution. Automated Deduction - {CADE-26} - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings. Itegulov, Daniyar and Slaney, John and Woltzenlogel Paleo, Bruno.

  4. Greedy Pebbling for Proof Space Compression. International Journal on Software Tools for Technology Transfer. Fellner, Andreas and Woltzenlogel Paleo, Bruno.

  5. Translations from Resolution to Sequent Calculus [Abstract]. Women in Logic (WiL) Workshop, affiliated with the Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Reis, Giselle and Woltzenlogel Paleo, Bruno.

  6. NP-Completeness of Small Conflict Set Generation for Congruence Closure. Formal Methods in System Design. Fellner, Andreas and Fontaine, Pascal and Woltzenlogel Paleo, Bruno.

  7. Reducing Redundancy in Cut-Elimination by Resolution. J. Log. Comput.. Woltzenlogel Paleo, Bruno.

  8. Proof Search in the Conflict Resolution Calculus [Abstract]. Second Conference on Artificial Intelligence and Theorem Proving. Slaney, John and Woltzenlogel Paleo, Bruno.

  9. Conflict Resolution: a First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning. Journal of Automated Reasoning. Slaney, John and Woltzenlogel Paleo, Bruno.

  10. Contextual Natural Deduction. Towards an Encyclopedia of Proof Systems. Woltzenlogel Paleo, Bruno.

  11. Towards an Encyclopedia of Proof Systems. College Publications. Editor: Woltzenlogel Paleo, Bruno.

  12. Variants of Gödel’s Ontological Proof in a Natural Deduction Calculus. Studia Logica, Springer. Siders, Annika and Woltzenlogel Paleo, Bruno.

  13. Epsilon Terms in Intuitionistic Sequent Calculus. The International Federation of Computational Logic (IFCoLog) Journal of Logic and its Applications. Reis, Giselle and Woltzenlogel Paleo, Bruno.

  14. Ancient History of the Quest for Universality of Proofs [Abstract]. Dagstuhl Seminar on the Universality of Proofs. Woltzenlogel Paleo, Bruno.

  15. First-Order Conflict-Driven Clause Learning from a Proof-Theoretical Perspective [Abstract]. Dagstuhl Seminar on the Universality of Proofs. Woltzenlogel Paleo, Bruno.

2016

  1. Para-Disagreement Logics [Abstract]. Trends in Logic XVI: Consistency, Contradiction, Paraconsistency and Reasoning: 40 years of CLE. Woltzenlogel Paleo, Bruno.

  2. Contextual Natural Deduction. Towards an Encyclopedia of Proof Systems. Bruno Woltzenlogel Paleo.

  3. Towards an Encyclopedia of Proof Systems [Book]. College Publications, Mathematical Logic and Foundations. Editor: Woltzenlogel Paleo, Bruno.

  4. Leibniz’s Characteristica Universalis and Calculus Ratiocinator Today [Book Chapter]. Death and Anti-Death, Volume 14: Four Decades after Michael Polanyi, Three Centuries after G. W. Leibniz. Woltzenlogel Paleo, Bruno.

  5. Analysis of an Ontological Proof Proposed by Leibniz [Book Chapter]. Death and Anti-Death, Volume 14: Four Decades after Michael Polanyi, Three Centuries after G. W. Leibniz. Bentert, Matthias and Benzmüller, Christoph and Streit, David and Woltzenlogel Paleo, Bruno.

  6. An Object-Logic Explanation for the Inconsistency in Gödel’s Ontological Theory. KI 2016: Advances in Artificial Intelligence – Annual German Conference on AI, LNAI, Springer. Benzmüller, Christoph and Woltzenlogel Paleo, Bruno.

  7. The Inconsistency in Gödel’s Ontological Argument: A Success Story for AI in Metaphysics. International Joint Conference on Artificial Intelligence - IJCAI. Benzmüller, Christoph and Woltzenlogel Paleo, Bruno.

  8. Computer-Assisted Analysis of the Anderson-Hájek Ontological Controversy. Logica Universalis, Springer. Benzmüller, Christoph and Weber, Leon and Woltzenlogel Paleo, Bruno.

  9. Epsilon Terms in Intuitionistic Sequent Calculus. The International Federation of Computational Logic (IFCoLog) Journal of Logic and its Applications. Reis, Giselle and Woltzenlogel Paleo, Bruno.

2015

  1. On Logic Embeddings and Gödel’s God [Abstract]. Recent Trends in Algebraic Development Techniques. Benzmüller, Christoph and Woltzenlogel Paleo, Bruno.

  2. Experiments in Computational Metaphysics: Gödel’s Proof of God’s Existence. Science and Spiritual Quest: Proceedings of the 9th All India Students’ Conference on Science and Spiritual Quest (IIT Kharagpur, 30th October – 1st November). Christoph Benzmüller and Bruno Woltzenlogel Paleo .

  3. Implementation and Evaluation of Contextual Natural Deduction for Minimal Logic. Ershov Informatics Conference - Perspectives of System Informatics (PSI). Bruno Woltzenlogel Paleo.

  4. Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses. International Conference on Automated Deduction (CADE). Jan Gorzny and Bruno Woltzenlogel Paleo.

  5. Higher-Order Modal Logics: Automation and Applications [Book Chapter]. International Reasoning Web Summer School. Christoph Benzmüller and Bruno Woltzenlogel Paleo.

  6. Interacting with Modal Logics in the Coq Proof Assistant. International Computer Science Symposium in Russia (CSR). Christoph Benzmüller and Bruno Woltzenlogel Paleo.

  7. NP-Completeness of Small Conflict Set Generation for Congruence Closure [Short Paper]. International Workshop on Satisfiability Modulo Theories. Fellner, Andreas and Fontaine, Pascal and Hofferek, Georg and Woltzenlogel Paleo, Bruno.

  8. Epsilon Terms in Intuitionistic Sequent Calculus [Short Paper]. Workshop on Hilbert’s Epsilon and Tau in Logic, Informatics and Linguistics. Reis, Giselle and Woltzenlogel Paleo, Bruno.

  9. Computer-Assisted Analysis of the Anderson-Hájek Ontological Controversy [Short Paper]. World Congress on Logic and Religion. Benzmüller, Christoph and Weber, Leon and Woltzenlogel Paleo, Bruno.

  10. All about Proofs, Proofs for All [Book]. Mathematical Logic and Foundations, College Publications. Editors: Delahaye, David and Woltzenlogel Paleo, Bruno.

2014

  1. Reducing Redundancy in Cut-Elimination by Resolution. Journal of Logic and Computation. Bruno Woltzenlogel Paleo.

  2. Automating Gödel’s Ontological Proof of God’s Existence with Higher-order Automated Theorem Provers. European Conference on Artificial Intelligence (ECAI). Christoph Benzmüller and Bruno Woltzenlogel Paleo.

  3. Proceedings of the Eleventh Workshop on User Interfaces for Theorem Provers, {UITP} 2014, Vienna, Austria, 17th July 2014 [Proceedings]. EPTCS. Editors: Christoph Benzmüller and Bruno Woltzenlogel Paleo.

  4. Formalization and Automated Verification of Gödel’s Proof of God’s Existence [Abstract]. 4th World Congress on the Square of Opposition. Benzmüller, Christoph and Woltzenlogel Paleo, Bruno.

  5. On Logic Embeddings and Gödel’s God [Abstract]. 22nd International Workshop on Algebraic Development Techniques. Benzmüller, Christoph and Woltzenlogel Paleo, Bruno.

  6. The Modal Collapse as a Collapse of the Modal Square of Opposition. Studies in Universal Logic, Springer. Benzmüller, Christoph and Woltzenlogel Paleo, Bruno.

  7. Skeptik: A Proof Compression System. International Joint Conference on Automated Reasoning (IJCAR). Joseph Boudou and Andreas Fellner and Bruno Woltzenlogel Paleo.

2013

  1. Formalization, Mechanization and Automation of Gödel’s Proof of God’s Existence [Abstract]. arXiv. Christoph Benzmüller and Bruno Woltzenlogel Paleo.

  2. Gödel’s God in Isabelle/HOL. Archive of Formal Proofs. Benzmüller, Christoph and Woltzenlogel Paleo, Bruno.

  3. Gödel’s God on the Computer [Abstract]. 10th International Workshop on the Implementation of Logics. Benzmüller, Christoph and Woltzenlogel Paleo, Bruno .

  4. Compression of Propositional Resolution Proofs by Lowering Subproofs. Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux). Joseph Boudou and Bruno Woltzenlogel Paleo.

  5. Compression of Propositional Resolution Proofs by Lowering Subproofs [Short Paper]. 11th Workshop on Satisfiability Modulo Theories and 12th Workshop on Proof, Computation and Complexity. Boudou, Joseph and Woltzenlogel Paleo, Bruno .

  6. ProofTool: a {GUI} for the {GAPT} Framework. User Interfaces for Theorem Provers (UITP). Cvetan Dunchev and Alexander Leitsch and Tomer Libal and Martin Riener and Mikheil Rukhaia and Daniel Weller and Bruno Woltzenlogel Paleo.

  7. Contextual Natural Deduction. Logical Foundations of Computer Science (LFCS). Bruno Woltzenlogel Paleo

  8. Automated Verification and Reconstruction of Gödel’s Proof of God’s Existence [Short Paper]. Journal of the Austrian Computer Society. Woltzenlogel Paleo, Bruno and Benzmüller, Christoph.

2012

  1. System Feature Description: Importing Refutations into the GAPT Framework. Proof Exchange for Theorem Proving (PxTP). Cvetan Dunchev and Alexander Leitsch and Tomer Libal and Martin Riener and Mikheil Rukhaia and Daniel Weller and Bruno Woltzenlogel Paleo.

  2. Towards CERes in intuitionistic logic. Computer Science Logic (CSL). Alexander Leitsch and Giselle Reis and Bruno Woltzenlogel Paleo.

  3. Physics and Proof Theory. Journal Applied Mathematics and Computation. Bruno Woltzenlogel Paleo.

2011

  1. Exploiting Symmetry in {SMT} Problems. International Conference on Automated Deduction (CADE). David Déharbe and Pascal Fontaine and Stephan Merz and Bruno Woltzenlogel Paleo.

  2. Quantifier Inference Rules in the Proof Format of VeriT. 1st International Workshop on Proof Exchange for Theorem Proving. Deharbe, David and Fontaine, Pascal and Woltzenlogel Paleo, Bruno.

  3. Compression of Propositional Resolution Proofs via Partial Regularization. International Conference on Automated Deduction (CADE). Pascal Fontaine and Stephan Merz and Bruno Woltzenlogel Paleo.

2010

  1. System Description: The Proof Transformation System CERES. International Joint Conference on Automated Reasoning (IJCAR). Tsvetan Dunchev and Alexander Leitsch and Tomer Libal and Daniel Weller and Bruno Woltzenlogel Paleo.

  2. Exploring and Exploiting Algebraic and Graphical Properties of Resolution. Workshop on Satisfiability Modulo Theories. Pascal Fontaine and Stephan Merz and Bruno Woltzenlogel Paleo.

  3. Using Proofs to Compute Implicatures [Abstract]. Computability in Europe: Programs, Proofs, Processes: Abstract and Handout Booklet. Ekaterina Lebedeva and Bruno Woltzenlogel Paleo.

  4. Atomic Cut Introduction by Resolution: Proof Structuring and Compression. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). Bruno Woltzenlogel Paleo.

  5. Levenshtein Distance: Two Applications in Database Record Linkage and Natural Language Processing [Book]. LAP-Lambert Academic Publishing. Bruno Woltzenlogel Paleo.

  6. Proof Compression with the {CIRes} Method [Abstract]. Computability in Europe: Programs, Proofs, Processes: Abstract and Handout Booklet. Bruno Woltzenlogel Paleo.

  7. Physics and Proof Theory. International Workshop on Physics and Computation. Woltzenlogel Paleo, Bruno.

2009

  1. Resolution Refinements for Cut-Elimination based on Reductive Methods. 2nd Workshop on Structures and Deduction. Hetzl, Stefan and Leitsch, Alexander and Libal, Tomer and Weller, Daniel and Woltzenlogel Paleo, Bruno.

  2. A Clausal Approach to Proof Analysis in Second-Order Logic. Logical Foundations of Computer Science. Stefan Hetzl and Alexander Leitsch and Daniel Weller and Bruno Woltzenlogel Paleo.

  3. A General Analysis of Cut-Elimination by CERes [PhD Thesis]. Vienna University of Technology. Woltzenlogel Paleo, Bruno.

2008

  1. Cut-Elimination by Resolution and Skolemization in Second-Order Logic. Analytic Proof Systems. Stefan Hetzl and Alexander Leitsch and Daniel Weller and Bruno Woltzenlogel Paleo.

  2. Herbrand Sequent Extraction. Intelligent Computer Mathematics. Stefan Hetzl and Alexander Leitsch and Daniel Weller and Bruno Woltzenlogel Paleo.

  3. Transforming and Analyzing Proofs in the CERES-System. KEAPPA and IWIL. Stefan Hetzl and Alexander Leitsch and Daniel Weller and Bruno Woltzenlogel Paleo.

  4. Herbrand Sequent Extraction. Workshop on Classical Logic and Computation. Hetzl, Stefan and Leitsch, Alexander and Weller, Daniel and Woltzenlogel Paleo, Bruno.

  5. Proof Analysis with HLK, CERES and ProofTool – Current Status and Future Directions. Workshop on Empirically Successful Automated Reasoning for Mathematics. Hetzl, Stefan and Leitsch, Alexander and Weller, Daniel and Woltzenlogel Paleo, Bruno.

  6. Herbrand Sequent Extraction [Book]. VDM-Verlag. Woltzenlogel Paleo, Bruno.

2007

  1. An Approximate Gazetteer for {GATE} based on Levenshtein Distance. Twelfth ESSLLI (European Summer School in Logic, Language and Information) Student Section. Woltzenlogel Paleo, Bruno.

  2. Herbrand Sequent Extraction [MSc Thesis]. Technische Universität Dresden; Technische Universität Wien. Woltzenlogel Paleo, Bruno.

  3. Levenshtein Distance for Information Extraction in Databases and for Natural Language Processing [MSc Thesis]. Instituto Tecnológico de Aeronáutica. Woltzenlogel Paleo, Bruno.

2006

  1. A Modified Edit-Distance Algorithm for Record Linkage in a Database of Companies. Workshop em Algoritmos e Aplicações de Mineração de Dados. Woltzenlogel Paleo, Bruno.

2005

  1. The Brazilian Gravitational Wave Detector Mario Schenberg: Progress and Plans. Class.Quant.Grav.. O. D. Aguiar and J. C. N. de Araujo and Bruno Woltzenlogel Paleo et al.

  2. Computational Intelligence Applied to Ambiguities and Redundancies in the Brazilian Taxation Office’s Database of Foreign Companies [In Portuguese]. Segunda Conferência Sul-Americana em Ciência e Tecnologia Aplicada ao Governo Eletrônico. Bruno Woltzenlogel Paleo and Cinara Ghedini and Joubert de Castro Lima and Jorge Jambeiro Filho and Antonella S.Lanna and Carlos H.C. Ribeiro.

2004

  1. The Brazilian Spherical Detector: Progress and Plans. Class.Quant.Grav.. O. D. Aguiar and J. C. N. de Araujo and Bruno Woltzenlogel Paleo et al.

  2. Can Black Hole MACHO Binaries be Detected by the Brazilian Spherical Antenna?. Class.Quant.Grav.. Araujo, J. C. N. de and Miranda, O. D. and Castro, C. S. and Woltzenlogel Paleo, Bruno and Aguiar, O. D.

  3. Expert System for Highway Management [Dipl.-Eng. Thesis, In Portuguese]. Instituto Tecnológico de Aeronáutica. Woltzenlogel Paleo, Bruno.

  4. Expert System for Highway Management [In Portuguese]. Simpósio Internacional de Iniciação Científica da Universidade de São Paulo. Woltzenlogel Paleo, Bruno.

2002

  1. Astrophysical Sources of Gravitational Waves: Black Hole Binary Systems [In Portuguese]. Simpósio de Iniciação Científica do Instituto Nacional de Pesquisas Espaciais. Woltzenlogel Paleo, Bruno.