Christoph Benzmüller

Künstliche Intell., August, 2024

Challenges for Non-Classical Reasoning in Contemporary AI Applications.

[BibT_eX]

[DOI]

Künstliche Intell., August, 2024

Non-Classical Reasoning for Contemporary AI Applications.

[BibT_eX]

[DOI]

Künstliche Intell., August, 2024

Who finds the short proof?

[BibT_eX]

[DOI]

Log. J. IGPL, 2024

Conditional normative reasoning as a fragment of HOL (Isabelle/HOL dataset).

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2024

Check News in One Click: NLP-Empowered Pro-Kremlin Propaganda Detection.

[BibT_eX]

[DOI]

Proceedings of the 18th Conference of the European Chapter of the Association for Computational Linguistics, 2024

Verantwortung.

[BibT_eX]

[DOI]

Lukas Höper

Carsten Schulte

Proceedings of the Künstliche Intelligenz für Lehrkräfte: Eine fachliche Einführung mit didaktischen Hinweisen, 2024

Schließen aus Wissen.

[BibT_eX]

[DOI]

Ulrich Furbach

Proceedings of the Künstliche Intelligenz für Lehrkräfte: Eine fachliche Einführung mit didaktischen Hinweisen, 2024

Logikbasierte Wissensverarbeitung.

[BibT_eX]

[DOI]

Proceedings of the Künstliche Intelligenz für Lehrkräfte: Eine fachliche Einführung mit didaktischen Hinweisen, 2024

2023

Automating public announcement logic with relativized common knowledge as a fragment of HOL in LogiKEy.

[BibT_eX]

[DOI]

J. Log. Comput., August, 2023

Preface: Special Issue on Logic and Argumentation.

[BibT_eX]

[DOI]

Pietro Baroni

Yì N. Wáng

J. Log. Comput., March, 2023

Automated Multilingual Detection of Pro-Kremlin Propaganda in Newspapers and Telegram Posts.

[BibT_eX]

[DOI]

Datenbank-Spektrum, March, 2023

Normative Conditional Reasoning as a Fragment of HOL.

[BibT_eX]

[DOI]

CoRR, 2023

Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation.

[BibT_eX]

[DOI]

CoRR, 2023

Theorem Proving in Dependently-Typed Higher-Order Logic - Extended Preprint.

[BibT_eX]

[DOI]

Colin Rothgang

Florian Rabe

CoRR, 2023

Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 16th International Conference, 2023

PapagAI: Automated Feedback for Reflective Essays.

[BibT_eX]

[DOI]

Michaela Gläser-Zikuda

Tim Landgraf

Proceedings of the KI 2023: Advances in Artificial Intelligence, 2023

Solving Modal Logic Problems by Translation to Higher-Order Logic.

[BibT_eX]

[DOI]

Proceedings of the Logic and Argumentation - 5th International Conference, 2023

Theorem Proving in Dependently-Typed Higher-Order Logic.

[BibT_eX]

[DOI]

Colin Rothgang

Florian Rabe

Proceedings of the Automated Deduction - CADE 29, 2023

2022

Collaborative Speculations on Future Themes for Participatory Design in Germany.

[BibT_eX]

[DOI]

i-com, 2022

Solving QMLTP Problems by Translation to Higher-order Logic.

[BibT_eX]

[DOI]

CoRR, 2022

Who Finds the Short Proof? An Exploration of Variants of Boolos' Curious Inference using Higher-order Automated Theorem Provers.

[BibT_eX]

[DOI]

CoRR, 2022

Mathematical Proof Between Generations.

[BibT_eX]

[DOI]

CoRR, 2022

A Simplified Variant of Gödel's Ontological Argument.

[BibT_eX]

[DOI]

CoRR, 2022

Automation of Boolos' Curious Inference in Isabelle/HOL.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2022

Automated Reasoning in Non-classical Logics in the TPTP World.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC/IJCAR 2022), Haifa, Israel, August, 11, 2022

Automated Verification of Deontic Correspondences in Isabelle/HOL - First Results.

[BibT_eX]

[DOI]

Proceedings of the 4th International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2022) affiliated with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022), 2022

2021

Leo-III - A Theorem Prover for Higher-Order Logic.

[BibT_eX]

[DOI]

Dataset, January, 2021

Introduction to the Special Issue on Logic Rules and Reasoning: Selected Papers from the 2nd International Joint Conference on Rules and Reasoning (RuleML+RR 2018).

[BibT_eX]

[DOI]

Francesco Ricca

Theory Pract. Log. Program., 2021

Extensional Higher-Order Paramodulation in Leo-III.

[BibT_eX]

[DOI]

J. Autom. Reason., 2021

Modeling and Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy.

[BibT_eX]

[DOI]

CoRR, 2021

Automating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2021

Exploring Simplified Variants of Gödel's Ontological Argument in Isabelle/HOL.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2021

Value-Oriented Legal Argumentation in Isabelle/HOL.

[BibT_eX]

[DOI]

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

A German Corpus of Reflective Sentences.

[BibT_eX]

[DOI]

Proceedings of the 18th International Conference on Natural Language Processing (ICON 2021), National Institute of Technology Silchar, Silchar, India, December 16, 2021

2020

Leo-III 1.5 - A Theorem Prover for Higher-Order Logic.

[BibT_eX]

[DOI]

Dataset, October, 2020

Mechanizing Principia Logico-Metaphysica in Functional Type-Theory.

[BibT_eX]

[DOI]

Daniel Kirchner

Edward N. Zalta

Rev. Symb. Log., 2020

Automating Free Logic in HOL, with an Experimental Application in Category Theory.

[BibT_eX]

[DOI]

J. Autom. Reason., 2020

Higher-order Logic as Lingua Franca - Integrating Argumentative Discourse and Deep Logical Analysis.

[BibT_eX]

[DOI]

CoRR, 2020

Encoding Legal Balancing: Automating an Abstract Ethico-Legal Value Ontology in Preference Logic.

[BibT_eX]

[DOI]

Bertram Lomfeld

CoRR, 2020

On Reductions of Hintikka Sets for Higher-Order Logic.

[BibT_eX]

[DOI]

CoRR, 2020

A (Simplified) Supreme Being Necessarily Exists - Says the Computer!

[BibT_eX]

[DOI]

CoRR, 2020

Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support.

[BibT_eX]

[DOI]

Leendert W. N. van der Torre

Artif. Intell., 2020

A (Simplified) Supreme Being Necessarily Exists, says the Computer: Computationally Explored Variants of Gödel's Ontological Argument.

[BibT_eX]

[DOI]

Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, 2020

Positive Free Higher-Order Logic and Its Automation via a Semantical Embedding.

[BibT_eX]

[DOI]

Irina Makarenko

Proceedings of the KI 2020: Advances in Artificial Intelligence, 2020

Reasonable Machines: A Research Manifesto.

[BibT_eX]

[DOI]

Bertram Lomfeld

Proceedings of the KI 2020: Advances in Artificial Intelligence, 2020

The Higher-Order Prover Leo-III.

[BibT_eX]

[DOI]

Proceedings of the ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020, 2020

Normative Reasoning with Expressive Logic Combinations.

[BibT_eX]

[DOI]

Proceedings of the ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020, 2020

Public Announcement Logic in HOL.

[BibT_eX]

[DOI]

Proceedings of the Dynamic Logic. New Trends and Applications, 2020

Computer-Supported Analysis of Arguments in Climate Engineering.

[BibT_eX]

[DOI]

Proceedings of the Logic and Argumentation - Third International Conference, 2020

Computer-Supported Exploration of a Categorical Axiomatization of Modeloids.

[BibT_eX]

[DOI]

Proceedings of the Relational and Algebraic Methods in Computer Science, 2020

2019

Universal (meta-)logical reasoning: Recent successes.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2019

åqvist's Dyadic Deontic Logic E in HOL.

[BibT_eX]

[DOI]

Ali Farjami

FLAP, 2019

I/O Logic in HOL.

[BibT_eX]

[DOI]

FLAP, 2019

Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument.

[BibT_eX]

[DOI]

CoRR, 2019

A Computational-Hermeneutic Approach for Conceptual Explicitation.

[BibT_eX]

[DOI]

CoRR, 2019

Computer Science and Metaphysics: A Cross-Fertilization.

[BibT_eX]

[DOI]

Daniel Kirchner

Edward N. Zalta

CoRR, 2019

Designing Normative Theories of Ethical Reasoning: Formal Framework, Methodology, and Tool Support.

[BibT_eX]

[DOI]

Leendert W. N. van der Torre

CoRR, 2019

Report on the Second International Joint Conference on Rules and Reasoning.

[BibT_eX]

[DOI]

Francesco Ricca

AI Mag., 2019

Harnessing Higher-Order (Meta-)Logic to Represent and Reason with Complex Ethical Theories.

[BibT_eX]

[DOI]

Proceedings of the PRICAI 2019: Trends in Artificial Intelligence, 2019

The Higher-Order Prover Leo-III (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the KI 2019: Advances in Artificial Intelligence, 2019

Modelling the US Constitution to Establish Constitutional Dictatorship.

[BibT_eX]

[DOI]

Valeria Zahoransky

Proceedings of the 4th International Workshop on MIning and REasoning with Legal texts co-located with the 32nd International Conference on Legal Knowledge and Information Systems (JURIX 2019), 2019

Mechanised Assessment of Complex Natural-Language Arguments Using Expressive Logic Combinations.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 12th International Symposium, 2019

2018

First Experiments with a Flexible Infrastructure for Normative Reasoning.

[BibT_eX]

[DOI]

CoRR, 2018

I/O Logic in HOL - First Steps.

[BibT_eX]

[DOI]

CoRR, 2018

Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL.

[BibT_eX]

[DOI]

Ali Farjami

CoRR, 2018

Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2018

Axiom Systems for Category Theory in Free Logic.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2018

A Dyadic Deontic Logic in HOL.

[BibT_eX]

Ali Farjami

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.

[BibT_eX]

[DOI]

Proceedings of the Dynamics, 2018

A Deontic Logic Reasoning Infrastructure.

[BibT_eX]

[DOI]

Leendert W. N. van der Torre

Proceedings of the Sailing Routes in the World of Computation, 2018

System Demonstration: The Higher-Order Prover Leo-III.

[BibT_eX]

[DOI]

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

2017

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

[BibT_eX]

[DOI]

L. Weber

Logica Universalis, 2017

Cut-Elimination for Quantified Conditional Logic.

[BibT_eX]

[DOI]

J. Philos. Log., 2017

Universal Reasoning, Rational Argumentation and Human-Machine Interaction.

[BibT_eX]

[DOI]

CoRR, 2017

Computer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

Types, Tableaus and Gödel's God in Isabelle/HOL.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

Recent Successes with a Meta-Logical Approach to Universal Logical Reasoning (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Formal Methods: Foundations and Applications - 20th Brazilian Symposium, 2017

Capability Discovery for Automated Reasoning Systems.

[BibT_eX]

[DOI]

Proceedings of the IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, 2017

Going Polymorphic - TH1 Reasoning for Leo-III.

[BibT_eX]

[DOI]

Proceedings of the IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, 2017

Theorem Provers For Every Normal Modal Logic.

[BibT_eX]

[DOI]

Tobias Gleißner

Proceedings of the LPAR-21, 2017

Leo-III Version 1.1 (System description).

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the KI 2017: Advances in Artificial Intelligence, 2017

2016

Axiomatizing Category Theory in Free Logic.

[BibT_eX]

[DOI]

CoRR, 2016

Einsatz von Theorembeweisern in der Lehre.

[BibT_eX]

Proceedings of the Hochschuldidaktik der Informatik, 2016

Translating Higher-Order Modal Logic from RuleML to TPTP.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

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

Agent-Based HOL Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Software - ICMS 2016, 2016

Automating Free Logic in Isabelle/HOL.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Software - ICMS 2016, 2016

Is It Reasonable to Employ Agents in Automated Theorem Proving?.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the GCAI 2016. 2nd Global Conference on Artificial Intelligence, September 19, 2016

Effective Normalization Techniques for HOL.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

TPTP and Beyond: Representation of Quantified Non-Classical Logics.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

J. Autom. Reason., 2015

Systematic Verification of the Modal Logic Cube in Isabelle/HOL.

[BibT_eX]

[DOI]

Maximilian Claus

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.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 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

LeoPARD - A Generic Platform for the Implementation of Higher-Order Reasoners.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

There Is No Best \beta -Normalization Strategy for Higher-Order Reasoners.

[BibT_eX]

[DOI]

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

Proofs and Reconstructions.

[BibT_eX]

[DOI]

Lawrence C. Paulson

Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

Interacting with Modal Logics in the Coq Proof Assistant.

[BibT_eX]

[DOI]

Proceedings of the Computer Science - Theory and Applications, 2015

2014

Automation of Higher-Order Logic.

[BibT_eX]

[DOI]

Dale Miller

Proceedings of the Computational Logic, 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

HOL Provers for First-order Modal Logics - Experiments.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning in Quantified Non-Classical Logics, 2014

2013

Quantified Multimodal Logics in Simple Type Theory.

[BibT_eX]

[DOI]

Lawrence C. Paulson

Logica Universalis, 2013

Update report: LEO-II version 1.5

[BibT_eX]

[DOI]

CoRR, 2013

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

[BibT_eX]

[DOI]

CoRR, 2013

Sigma: An integrated development environment for formal ontology.

[BibT_eX]

[DOI]

Adam Pease

AI Commun., 2013

Gödel's God in Isabelle/HOL.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2013

HOL Based First-Order Modal Logic Provers.

[BibT_eX]

[DOI]

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

Automating Quantified Conditional Logics in HOL.

[BibT_eX]

[DOI]

Proceedings of the IJCAI 2013, 2013

A Top-down Approach to Combining Logics.

[BibT_eX]

Proceedings of the ICAART 2013, 2013

LEO-II Version 1.5.

[BibT_eX]

[DOI]

Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

2012

Higher-order aspects and context in SUMO.

[BibT_eX]

[DOI]

Adam Pease

J. Web Semant., 2012

FMLtoHOL (version 1.0): Automating First-order Modal Logics with LEO-II and Friends

[BibT_eX]

[DOI]

CoRR, 2012

Quantified Conditional Logics are Fragments of HOL

[BibT_eX]

[DOI]

Valerio Genovese

CoRR, 2012

Embedding and automating conditional logics in classical higher-order logic.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2012

Understanding LEO-II's proofs.

[BibT_eX]

[DOI]

Proceedings of the IWIL 2012: The 9th International Workshop on the Implementation of Logics, 2012

Implementing and Evaluating Provers for First-order Modal Logics.

[BibT_eX]

[DOI]

Jens Otten

Proceedings of the ECAI 2012, 2012

Implementing Different Proof Calculi for First-order Modal Logics.

[BibT_eX]

[DOI]

Jens Otten

Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012

2011

Resource-Bounded Modelling and Analysis of Human-Level Interactive Proofs.

[BibT_eX]

[DOI]

Proceedings of the Resource-Adaptive Cognitive Processes, 2011

ΩMEGA: Resource-Adaptive Processes in an Automated Reasoning System.

[BibT_eX]

[DOI]

Proceedings of the Resource-Adaptive Cognitive Processes, 2011

Combining and automating classical and non-classical logics in classical higher-order logics.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2011

2010

Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure.

[BibT_eX]

[DOI]

Geoff Sutcliffe

J. Formaliz. Reason., 2010

Multimodal and intuitionistic logics in simple type theory.

[BibT_eX]

[DOI]

Lawrence C. Paulson

Log. J. IGPL, 2010

Simple Type Theory as Framework for Combining Logics.

[BibT_eX]

[DOI]

CoRR, 2010

Combining Logics in Simple Type Theory.

[BibT_eX]

[DOI]

Proceedings of the Computational Logic in Multi-Agent Systems, 11th International Workshop, 2010

Adaptive Assertion-Level Proofs.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Evaluation Methods for Solvers, 2010

Progress in Automating Higher-Order Ontology Reasoning.

[BibT_eX]

[DOI]

Adam Pease

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).

[BibT_eX]

[DOI]

Proceedings of the Verification, Induction, Termination Analysis, 2010

2009

Jacques Herbrand: Life, Logic, and Automated Deduction.

[BibT_eX]

[DOI]

Proceedings of the Logic from Russell to Church, 2009

Automating Quantified Multimodal Logics in Simple Type Theory -- A Case Study

[BibT_eX]

[DOI]

CoRR, 2009

Lectures on Jacques Herbrand as a Logician

[BibT_eX]

[DOI]

CoRR, 2009

Cut-Simulation and Impredicativity

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2009

A remark on higher order RUE-resolution with EXTRUE

[BibT_eX]

[DOI]

CoRR, 2009

Resource Adaptive Agents in Interactive Theorem Proving

[BibT_eX]

[DOI]

CoRR, 2009

Automating Access Control Logics in Simple Type Theory with LEO-II (Techreport)

[BibT_eX]

[DOI]

CoRR, 2009

Automating Access Control Logics in Simple Type Theory with LEO-II.

[BibT_eX]

[DOI]

Proceedings of the Emerging Challenges for Security, 2009

Presenting Proofs with Adapted Granularity.

[BibT_eX]

[DOI]

Proceedings of the KI 2009: Advances in Artificial Intelligence, 2009

Proof Granularity as an Empirical Problem?

[BibT_eX]

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.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2009

Granularity-Adaptive Proof Presentation.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Math. Comput. Sci., 2008

Combined reasoning by automated cooperation.

[BibT_eX]

[DOI]

J. Appl. Log., 2008

Preface.

[BibT_eX]

[DOI]

Proceedings of the 8th International Workshop on User Interfaces for Theorem Provers, 2008

Evaluation of Systems for Higher-order Logic (ESHOL).

[BibT_eX]

[DOI]

Proceedings of the First International Workshop on Practical Aspects of Automated Reasoning, 2008

THF0 - The Core of the TPTP Language for Higher-Order Logic.

[BibT_eX]

[DOI]

Florian Rabe

Geoff Sutcliffe

Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description).

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007

Deep Inference for Automated Proof Tutoring?

[BibT_eX]

[DOI]

Dominik Dietrich

Proceedings of the KI 2007: Advances in Artificial Intelligence, 2007

2006

Computer supported mathematics with Omegamega.

[BibT_eX]

[DOI]

J. Appl. Log., 2006

Towards computer aided mathematics.

[BibT_eX]

[DOI]

J. Appl. Log., 2006

PlatOmega: A Mediator between Text-Editors and Proof Assistance Systems.

[BibT_eX]

[DOI]

Marc Wagner

Proceedings of the 7th Workshop on User Interfaces for Theorem Provers, 2006

LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL)

[BibT_eX]

[DOI]

John Harrison

Carsten Schürmann

CoRR, 2006

Omega.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Helmut Horacek

Henri Lesourd

Proceedings of the Fifth International Conference on Language Resources and Evaluation, 2006

DiaWOz-II - A Tool for Wizard-of-Oz Experiments in Mathematics.

[BibT_eX]

[DOI]

Helmut Horacek

Henri Lesourd

Proceedings of the KI 2006: Advances in Artificial Intelligence, 2006

An Agent-Based Architecture for Dialogue Systems.

[BibT_eX]

[DOI]

Mark Buckley

Proceedings of the Perspectives of Systems Informatics, 2006

Cut-Simulation in Impredicative Logics.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005

A Structured Set of Higher-Order Problems.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Knowledge Management, 4th International Conference, 2005

Natural Language Dialog with a Tutor System for Mathematical Proofs.

[BibT_eX]

[DOI]

Helmut Horacek

Manfred Pinkal

Proceedings of the Cognitive Systems, Joint Chinese-German Workshop, Shanghai, 2005

Bridging Theorem Proving and Mathematical Knowledge Retrieval.

[BibT_eX]

[DOI]

Andreas Meier

Proceedings of the Mechanizing Mathematical Reasoning, 2005

Mathematical Domain Reasoning Tasks in Natural Language Tutorial Dialog on Proofs.

[BibT_eX]

[DOI]

Quoc Bao Vo

Proceedings of the Proceedings, 2005

2004

Higher-order semantics and extensionality.

[BibT_eX]

[DOI]

J. Symb. Log., 2004

An Annotated Corpus of Tutorial Dialogs on Mathematical Theorem Proving.

[BibT_eX]

[DOI]

Quoc Bao Vo

Dimitra Tsovaltzi

Proceedings of the Fourth International Conference on Language Resources and Evaluation, 2004

Can a Higher-Order and a First-Order Theorem Prover Cooperate?.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2004

Omega: Computer Supported Mathematics.

[BibT_eX]

[DOI]

Proceedings of the KI 2004: Advances in Artificial Intelligence, 2004

2003

Automatic Learning of Proof Methods in Proof Planning.

[BibT_eX]

[DOI]

Log. J. IGPL, 2003

Interactive Theorem Proving with Tasks.

[BibT_eX]

[DOI]

Proceedings of the User Interfaces for Theorem Provers Workshop, 2003

Assertion-level Proof Representation with Under-Specification.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Knowledge Management Symposium, 2003

Assertion Application in Theorem Proving and Proof Planning.

[BibT_eX]

[DOI]

Quoc Bao Vo

Proceedings of the IJCAI-03, 2003

2002

Comparing Approaches To Resolution Based Higher-Order Theorem Proving.

[BibT_eX]

[DOI]

Synth., 2002

Proof Development with Omega-MEGA: sqrt(2) Is Irrational.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2002

Proof Development with OMEGA.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2002

2001

Experiments with an Agent-Oriented Reasoning System.

[BibT_eX]

[DOI]

Proceedings of the KI 2001: Advances in Artificial Intelligence, 2001

2000

Resource Guided Concurrent Deduction.

[BibT_eX]

[DOI]

Proceedings of the Seventh Workshop on Automated Reasoning, 2000

1999

Equality and extensionality in automated higher order theorem proving.

[BibT_eX]

[DOI]

PhD thesis, 1999

Integrating Tps and Omega.

[BibT_eX]

[DOI]

Matthew Bishop

J. Univers. Comput. Sci., 1999

L<Omega>UI: Lovely <Omega>MEGA User Interface.

[BibT_eX]

[DOI]

Formal Aspects Comput., 1999

Agent based mathematical reasoning.

[BibT_eX]

[DOI]

Proceedings of the Systems for Integrated Computation and Deduction, 1999

Critical Agents Supporting Interactive Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the Progress in Artificial Intelligence, 1999

Extensional Higher-Order Paramodulation and RUE-Resolution.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1999

1998

System Description: LEO - A Higher-Order Theorem Prover.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1998

Extensional Higher-Order Resolution.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1998

A Blackboard Architecture for Guiding Interactive Proofs.

[BibT_eX]

[DOI]