Bruno Woltzenlogel Paleo

Rodney W. Prescott

Proceedings of the Financial Cryptography and Data Security. FC 2023 International Workshops, 2023

2021

Lifting propositional proof compression algorithms to first-order logic.

[BibT_eX]

[DOI]

Jan Gorzny

Ezequiel Postan

J. Log. Comput., 2021

2020

Partial Regularization of First-Order Resolution Proofs.

[BibT_eX]

[DOI]

Jan Gorzny

Ezequiel Postan

Proceedings of the 6th Global Conference on Artificial Intelligence, 2020

2019

Greedy pebbling for proof space compression.

[BibT_eX]

[DOI]

Andreas Fellner

Int. J. Softw. Tools Technol. Transf., 2019

Complexity of translations from resolution to sequent calculus.

[BibT_eX]

[DOI]

Giselle Reis

Math. Struct. Comput. Sci., 2019

2018

Erratum to: Conflict Resolution: A First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning.

[BibT_eX]

[DOI]

John Slaney

J. Autom. Reason., 2018

Conflict Resolution: A First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning.

[BibT_eX]

[DOI]

John Slaney

J. Autom. Reason., 2018

Sensala: a Dynamic Semantics System for Natural Language Processing.

[BibT_eX]

[DOI]

Daniyar Itegulov

Ekaterina Lebedeva

Proceedings of the COLING 2018, 2018

2017

Variants of Gödel's Ontological Proof in a Natural Deduction Calculus.

[BibT_eX]

[DOI]

Annika Kanckos

Stud Logica, 2017

Computer-Assisted Analysis of the Anderson-Hájek Ontological Controversy.

[BibT_eX]

[DOI]

L. Weber

Logica Universalis, 2017

Reducing redundancy in cut-elimination by resolution.

[BibT_eX]

[DOI]

J. Log. Comput., 2017

NP-completeness of small conflict set generation for congruence closure.

[BibT_eX]

[DOI]

Andreas Fellner

Formal Methods Syst. Des., 2017

Epsilon Terms in Intuitionistic Sequent Calculus.

[BibT_eX]

[DOI]

Giselle Reis

FLAP, 2017

Scavenger 0.1: A Theorem Prover Based on Conflict Resolution.

[BibT_eX]

[DOI]

Daniyar Itegulov

John Slaney

Proceedings of the Automated Deduction - CADE 26, 2017

2016

An Expressive Probabilistic Temporal Logic.

[BibT_eX]

[DOI]

CoRR, 2016

The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, 2016

2015

Higher-Order Modal Logics: Automation and Applications.

[BibT_eX]

[DOI]

Proceedings of the Reasoning Web. Web Logic Rules - 11th International Summer School 2015, Berlin, Germany, July 31, 2015

Implementation and Evaluation of Contextual Natural Deduction for Minimal Logic.

[BibT_eX]

[DOI]

Proceedings of the Perspectives of System Informatics, 2015

Interacting with Modal Logics in the Coq Proof Assistant.

[BibT_eX]

[DOI]

Proceedings of the Computer Science - Theory and Applications, 2015

Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses.

[BibT_eX]

[DOI]

Jan Gorzny

Proceedings of the Automated Deduction - CADE-25, 2015

2014

On Logic Embeddings and Gödel's God.

[BibT_eX]

[DOI]

Proceedings of the Recent Trends in Algebraic Development Techniques, 2014

Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers.

[BibT_eX]

[DOI]

Proceedings of the ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic, 2014

Skeptik: A Proof Compression System.

[BibT_eX]

[DOI]

Joseph Boudou

Andreas Fellner

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

Formalization, Mechanization and Automation of Gödel's Proof of God's Existence.

[BibT_eX]

[DOI]

CoRR, 2013

Gödel's God in Isabelle/HOL.

[BibT_eX]

[DOI]

Christoph Benzmueller

Arch. Formal Proofs, 2013

Compression of Propositional Resolution Proofs by Lowering Subproofs.

[BibT_eX]

[DOI]

Joseph Boudou

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2013

Contextual Natural Deduction.

[BibT_eX]

[DOI]

Proceedings of the Logical Foundations of Computer Science, International Symposium, 2013

2012

PROOFTOOL: a GUI for the GAPT Framework.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 10th International Workshop On User Interfaces for Theorem Provers, 2012

Physics and proof theory.

[BibT_eX]

[DOI]

Appl. Math. Comput., 2012

System Feature Description: Importing Refutations into the GAPT Framework.

[BibT_eX]

[DOI]

Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, 2012

Towards CERes in intuitionistic logic.

[BibT_eX]

[DOI]

Giselle Reis

Proceedings of the Computer Science Logic (CSL'12), 2012

2011

Quantifier Inference Rules for SMT proofs.

[BibT_eX]

[DOI]

David Déharbe

Proceedings of the PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, 2011

Compression of Propositional Resolution Proofs via Partial Regularization.

[BibT_eX]

[DOI]

Stephan Merz

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

Exploiting Symmetry in SMT Problems.

[BibT_eX]

[DOI]

David Déharbe

Stephan Merz

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010

Atomic Cut Introduction by Resolution: Proof Structuring and Compression.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

System Description: The Proof Transformation System CERES.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009

A Clausal Approach to Proof Analysis in Second-Order Logic.

[BibT_eX]

[DOI]

Stefan Hetzl

Daniel Weller

Proceedings of the Logical Foundations of Computer Science, International Symposium, 2009

2008

Transforming and Analyzing Proofs in the CERES-System.

[BibT_eX]

[DOI]

Stefan Hetzl

Daniel Weller

Proceedings of the LPAR 2008 Workshops, 2008

Herbrand Sequent Extraction.

[BibT_eX]

[DOI]

Stefan Hetzl

Daniel Weller