Christoph Benzmüller

According to our database1, Christoph Benzmüller authored at least 114 papers between 1997 and 2019.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2019
Universal (meta-)logical reasoning: Recent successes.
Sci. Comput. Program., 2019

Harnessing Higher-Order (Meta-)Logic to Represent and Reason with Complex Ethical Theories.
Proceedings of the PRICAI 2019: Trends in Artificial Intelligence, 2019

The Higher-Order Prover Leo-III (Extended Abstract).
Proceedings of the KI 2019: Advances in Artificial Intelligence, 2019

Mechanised Assessment of Complex Natural-Language Arguments Using Expressive Logic Combinations.
Proceedings of the Frontiers of Combining Systems - 12th International Symposium, 2019

2018
Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL.
Archive of Formal Proofs, 2018

Axiom Systems for Category Theory in Free Logic.
Archive of Formal Proofs, 2018

A Dyadic Deontic Logic in HOL.
Proceedings of the Deontic Logic and Normative Systems - 14th International Conference, 2018

Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments.
Proceedings of the Dynamics, 2018

A Deontic Logic Reasoning Infrastructure.
Proceedings of the Sailing Routes in the World of Computation, 2018

System Demonstration: The Higher-Order Prover Leo-III.
Proceedings of the 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018) affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2018), 2018

The Higher-Order Prover Leo-III.
Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017
Computer-Assisted Analysis of the Anderson-Hájek Ontological Controversy.
Logica Universalis, 2017

Cut-Elimination for Quantified Conditional Logic.
J. Philosophical Logic, 2017

Computer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument.
Archive of Formal Proofs, 2017

Types, Tableaus and Gödel's God in Isabelle/HOL.
Archive of Formal Proofs, 2017

Recent Successes with a Meta-Logical Approach to Universal Logical Reasoning (Extended Abstract).
Proceedings of the Formal Methods: Foundations and Applications - 20th Brazilian Symposium, 2017

Capability Discovery for Automated Reasoning Systems.
Proceedings of the IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, 2017

Going Polymorphic - TH1 Reasoning for Leo-III.
Proceedings of the IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, 2017

Theorem Provers For Every Normal Modal Logic.
Proceedings of the LPAR-21, 2017

Leo-III Version 1.1 (System description).
Proceedings of the IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, 2017

Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic.
Proceedings of the KI 2017: Advances in Artificial Intelligence, 2017

2016
Einsatz von Theorembeweisern in der Lehre.
Proceedings of the Hochschuldidaktik der Informatik, 2016

Translating Higher-Order Modal Logic from RuleML to TPTP.
Proceedings of the Supplementary Proceedings of the RuleML 2016 Challenge, 2016

The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics.
Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, 2016

Agent-Based HOL Reasoning.
Proceedings of the Mathematical Software - ICMS 2016, 2016

Automating Free Logic in Isabelle/HOL.
Proceedings of the Mathematical Software - ICMS 2016, 2016

Is It Reasonable to Employ Agents in Automated Theorem Proving?.
Proceedings of the 8th International Conference on Agents and Artificial Intelligence (ICAART 2016), 2016

Tutorial on Reasoning in Expressive Non-Classical Logics with Isabelle/HOL.
Proceedings of the GCAI 2016. 2nd Global Conference on Artificial Intelligence, September 19, 2016

Effective Normalization Techniques for HOL.
Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

TPTP and Beyond: Representation of Quantified Non-Classical Logics.
Proceedings of the 2nd International Workshop Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2016) affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2016)., 2016

2015
The Higher-Order Prover Leo-II.
J. Autom. Reasoning, 2015

Systematic Verification of the Modal Logic Cube in Isabelle/HOL.
Proceedings of the Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, 2015

Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2015

Higher-Order Modal Logics: Automation and Applications.
Proceedings of the Reasoning Web. Web Logic Rules - 11th International Summer School 2015, Berlin, Germany, July 31, 2015

LeoPARD - A Generic Platform for the Implementation of Higher-Order Reasoners.
Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

There Is No Best \beta -Normalization Strategy for Higher-Order Reasoners.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Proofs and Reconstructions.
Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

Interacting with Modal Logics in the Coq Proof Assistant.
Proceedings of the Computer Science - Theory and Applications, 2015

2014
Automation of Higher-Order Logic.
Proceedings of the Computational Logic, 2014

On Logic Embeddings and Gödel's God.
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.
Proceedings of the ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic, 2014

HOL Provers for First-order Modal Logics - Experiments.
Proceedings of the Automated Reasoning in Quantified Non-Classical Logics, 2014

2013
Quantified Multimodal Logics in Simple Type Theory.
Logica Universalis, 2013

Sigma: An integrated development environment for formal ontology.
AI Commun., 2013

Gödel's God in Isabelle/HOL.
Archive of Formal Proofs, 2013

HOL Based First-Order Modal Logic Provers.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

Automating Quantified Conditional Logics in HOL.
Proceedings of the IJCAI 2013, 2013

A Top-down Approach to Combining Logics.
Proceedings of the ICAART 2013, 2013

LEO-II Version 1.5.
Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

2012
Higher-order aspects and context in SUMO.
J. Web Semant., 2012

Embedding and automating conditional logics in classical higher-order logic.
Ann. Math. Artif. Intell., 2012

Understanding LEO-II's proofs.
Proceedings of the IWIL 2012: The 9th International Workshop on the Implementation of Logics, 2012

Implementing and Evaluating Provers for First-order Modal Logics.
Proceedings of the ECAI 2012, 2012

Implementing Different Proof Calculi for First-order Modal Logics.
Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012

2011
Resource-Bounded Modelling and Analysis of Human-Level Interactive Proofs.
Proceedings of the Resource-Adaptive Cognitive Processes, 2011

ΩMEGA: Resource-Adaptive Processes in an Automated Reasoning System.
Proceedings of the Resource-Adaptive Cognitive Processes, 2011

Combining and automating classical and non-classical logics in classical higher-order logics.
Ann. Math. Artif. Intell., 2011

2010
Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure.
J. Formalized Reasoning, 2010

Multimodal and intuitionistic logics in simple type theory.
Logic Journal of the IGPL, 2010

Combining Logics in Simple Type Theory.
Proceedings of the Computational Logic in Multi-Agent Systems, 11th International Workshop, 2010

Adaptive Assertion-Level Proofs.
Proceedings of the Workshop on Evaluation Methods for Solvers, 2010

Progress in Automating Higher-Order Ontology Reasoning.
Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, 2010

Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners).
Proceedings of the Verification, Induction, Termination Analysis, 2010

2009
Jacques Herbrand: Life, Logic, and Automated Deduction.
Proceedings of the Logic from Russell to Church, 2009

Preface.
Electr. Notes Theor. Comput. Sci., 2009

Cut-Simulation and Impredicativity
Logical Methods in Computer Science, 2009

Automating Access Control Logics in Simple Type Theory with LEO-II.
Proceedings of the Emerging Challenges for Security, 2009

Presenting Proofs with Adapted Granularity.
Proceedings of the KI 2009: Advances in Artificial Intelligence, 2009

Proof Granularity as an Empirical Problem?
Proceedings of the CSEDU 2009 - Proceedings of the First International Conference on Computer Supported Education, Lisboa, Portugal, March 23-26, 2009, 2009

Progress in the Development of Automated Theorem Proving for Higher-Order Logic.
Proceedings of the Automated Deduction, 2009

Granularity-Adaptive Proof Presentation.
Proceedings of the Artificial Intelligence in Education: Building Learning Systems that Care: From Knowledge Representation to Affective Modelling, 2009

2008
Organization, Transformation, and Propagation of Mathematical Knowledge in Omegamega.
Mathematics in Computer Science, 2008

Combined reasoning by automated cooperation.
J. Applied Logic, 2008

Evaluation of Systems for Higher-order Logic (ESHOL).
Proceedings of the First International Workshop on Practical Aspects of Automated Reasoning, 2008

THF0 - The Core of the TPTP Language for Higher-Order Logic.
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description).
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007
PlatOmega: A Mediator between Text-Editors and Proof Assistance Systems.
Electr. Notes Theor. Comput. Sci., 2007

Preface.
Electr. Notes Theor. Comput. Sci., 2007

Deep Inference for Automated Proof Tutoring?
Proceedings of the KI 2007: Advances in Artificial Intelligence, 2007

2006
Computer supported mathematics with Omegamega.
J. Applied Logic, 2006

Towards computer aided mathematics.
J. Applied Logic, 2006

Omega.
Proceedings of the Seventeen Provers of the World, Foreword by Dana S. Scott, 2006

A corpus of tutorial dialogs on theorem proving; the influence of the presentation of the study-material.
Proceedings of the Fifth International Conference on Language Resources and Evaluation, 2006

DiaWOz-II - A Tool for Wizard-of-Oz Experiments in Mathematics.
Proceedings of the KI 2006: Advances in Artificial Intelligence, 2006

An Agent-Based Architecture for Dialogue Systems.
Proceedings of the Perspectives of Systems Informatics, 2006

Cut-Simulation in Impredicative Logics.
Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005
A Structured Set of Higher-Order Problems.
Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity.
Proceedings of the Mathematical Knowledge Management, 4th International Conference, 2005

Natural Language Dialog with a Tutor System for Mathematical Proofs.
Proceedings of the Cognitive Systems, Joint Chinese-German Workshop, Shanghai, 2005

Bridging Theorem Proving and Mathematical Knowledge Retrieval.
Proceedings of the Mechanizing Mathematical Reasoning, 2005

Mathematical Domain Reasoning Tasks in Natural Language Tutorial Dialog on Proofs.
Proceedings of the Proceedings, 2005

2004
Higher-order semantics and extensionality.
J. Symb. Log., 2004

Interactive Theorem Proving with Tasks.
Electr. Notes Theor. Comput. Sci., 2004

Assertion-level Proof Representation with Under-Specification.
Electr. Notes Theor. Comput. Sci., 2004

An Annotated Corpus of Tutorial Dialogs on Mathematical Theorem Proving.
Proceedings of the Fourth International Conference on Language Resources and Evaluation, 2004

Can a Higher-Order and a First-Order Theorem Prover Cooperate?.
Proceedings of the Logic for Programming, 2004

Omega: Computer Supported Mathematics.
Proceedings of the KI 2004: Advances in Artificial Intelligence, 2004

2003
Automatic Learning of Proof Methods in Proof Planning.
Logic Journal of the IGPL, 2003

Assertion Application in Theorem Proving and Proof Planning.
Proceedings of the IJCAI-03, 2003

2002
Comparing Approaches To Resolution Based Higher-Order Theorem Proving.
Synthese, 2002

Proof Development with Omega-MEGA: sqrt(2) Is Irrational.
Proceedings of the Logic for Programming, 2002


2001
Experiments with an Agent-Oriented Reasoning System.
Proceedings of the KI 2001: Advances in Artificial Intelligence, 2001

2000
Resource Guided Concurrent Deduction.
Proceedings of the Seventh Workshop on Automated Reasoning, 2000

1999
Equality and extensionality in automated higher order theorem proving.
PhD thesis, 1999

Integrating Tps and Omega.
J. UCS, 1999

LUI: Lovely MEGA User Interface.
Formal Asp. Comput., 1999

Agent based mathematical reasoning.
Electr. Notes Theor. Comput. Sci., 1999

Critical Agents Supporting Interactive Theorem Proving.
Proceedings of the Progress in Artificial Intelligence, 1999

Extensional Higher-Order Paramodulation and RUE-Resolution.
Proceedings of the Automated Deduction, 1999

1998
System Description: LEO - A Higher-Order Theorem Prover.
Proceedings of the Automated Deduction, 1998

Extensional Higher-Order Resolution.
Proceedings of the Automated Deduction, 1998

A Blackboard Architecture for Guiding Interactive Proofs.
Proceedings of the Artificial Intelligence: Methodology, 1998

1997


  Loading...