@InProceedings{C105,
author = {Palesha, Rushit and Shetty, Sujala and Benzm\"{u}ller, Christoph},
OPTeditor = {},
title = {Neuro-Symbolic Translation and Verification: Automating First-Order Logic Generation and Theorem Proving from Natural Language},
booktitle = {10th International Conference on Information System Design and Intelligent Applications (ISDIA 2026): Agentic AI \& Sustainability},
year = 2026,
OPTpublisher = {Springer Nature Singapore},
OPTseries = {Lecture Notes in Networks and Systems},
OPTvolume = {1539},
OPTaddress = {Singapore},
OPTpages = {169--183},
OPTisbn = {978-981-96-9248-4},
OPTdoi = {},
OTnote = {To appear/accepted},
OPTaddendum = {To appear/accepted},
}
@article{J71,
author = {Rothgang, Colin and Rabe, Florian and
Benzm\"{u}ller, Christoph},
title = {Dependently-Typed Higher-Order Logic},
year = 2025,
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {27},
number = {1},
pages = {1-54},
issn = {1529-3785},
doi = {10.1145/3771725},
journal = {ACM Trans. Comput. Logic},
}
@article{J69,
Author = {Alexander Steen and Christoph Benzmüller},
Title = {On Reductions of Hintikka Sets for Higher-Order
Logic},
Journal = {Journal of Applied Logics -- IfCoLoG Journal of
Logics and their Applications},
volume = {12},
number = {7},
issn = {2631-9810},
year = 2025,
pages = {1813-1834},
url = {https://www.collegepublications.co.uk/downloads/ifcolog00075.pdf},
}
@InCollection{B29,
author = {Benzm{\"u}ller, Christoph},
title = {Symbolische Kontrolle für subsymbolische Künstliche Intelligenz?},
booktitle = {K{\"{u}}nstliche Intelligenz und Wir: Stand, Nutzung und Herausforderungen der {KI}},
editor = {Schmiedchen, Frank and von Gernler, Alexander and Hafner, Martina and Kratzer, Klaus Peter},
pages = {211–226},
year = {2026},
publisher = {Springer},
address = {Berlin Heidelberg},
isbn = {978-3-662-71566-6},
doi = {10.1007/978-3-662-71567-3_11},
url = {https://doi.org/10.1007/978-3-662-71567-3_11},
}
@InProceedings{C104,
author = {Tenne, Alina and Vestrucci, Andrea and Benzm\"{u}ller, Christoph},
editor = {Vikrant Bhateja and Farhad Oroumchia and Jinshan Tang and Zaid Omar},
title = {XAI in Healthcare: Analysis and Evaluation of XAI Tools and Legal Liability for Neural Networks. A Case Study on Tumor Image Classification},
booktitle = {Information System Design: Intelligent Healthcare Informatics Proceedings of Ninth International Conference on Information System Design and Intelligent Applications (ISDIA 2025), Volume 1},
year = 2025,
publisher = {Springer Nature Singapore},
series = {Lecture Notes in Networks and Systems},
volume = {1537},
address = {Singapore},
pages = {423–434},
OPTisbn = {978-981-96-9241-5},
doi = {10.1007/978-981-96-9242-2_31},
}
@InProceedings{C103,
author = {Vestrucci, Andrea and Benzm\"{u}ller, Christoph and Evangelatos, Nikolaos},
editor = {Vikrant Bhateja and Farhad Oroumchia and Jinshan Tang and Zaid Omar},
title = {Symbolic Approach to Trustworthy AI: Exploration and Healthcare Case Study},
booktitle = {Information System Design: Intelligent Healthcare Informatics Proceedings of Ninth International Conference on Information System Design and Intelligent Applications (ISDIA 2025), Volume 1},
year = 2025,
publisher = {Springer Nature Singapore},
series = {Lecture Notes in Networks and Systems},
volume = {1537},
address = {Singapore},
pages = {367–379},
OPTisbn = {978-981-96-9241-5},
doi = {10.1007/978-981-96-9242-2_27},
}
@InProceedings{C102,
author = {Aggarwal, Radhya and Kataria, Swastika and Urolagin,
Siddhaling and Benzm{\"u}ller, Christoph},
editor = {Bhateja, Vikrant and El Barachi, May and Azar, Ahmad
Taher and Sharma, Dilip Kumar},
title = {Automatic Reasoning-Code Generation Using NLP-Based Entity Relations Identification},
booktitle = {Information System Design: Big Data Analytics and Data Science. Proceedings of Ninth International Conference on Information System Design and Intelligent Applications (ISDIA 2025), Volume 3},
year = 2025,
publisher = {Springer Nature Singapore},
series = {Lecture Notes in Networks and Systems},
volume = {1539},
address = {Singapore},
pages = {169--183},
OPTisbn = {978-981-96-9247-7},
doi = {10.1007/978-981-96-9248-4_13},
}
@inproceedings{C101,
author = {Lara Lawniczak and Luca Pasetto and Christoph Benzmüller and Xu Li and Réka Markovich},
title = {Reasoning with Epistemic Rights and Duties: Automating a Dynamic Logic of the Right to Know in LogiKEy},
booktitle = {{ECAI} 2025 - 28th European Conference on Artificial Intelligence},
OPTseries = {Frontiers in Artificial Intelligence and Applications},
publisher = {{IOS} Press},
volume = {413},
pages = {1623-1630},
doi = {10.3233/FAIA250988},
url = {https://ebooks.iospress.nl/doi/10.3233/FAIA250988},
editor = {Inês Lynce and Nello Murano and Mauro Vallati and Serena Villata and Federico Chesani and Michela Milano and Andrea Omicini and Mehdi Dastani},
year = {2025},
}
@InProceedings{W72,
author = {Luca Pasetto and Christoph Benzm{\"u}ller},
title = {Visualizing Kripke Models in LogiKEy: the Case
of SDL},
booktitle = {Joint Proceedings of the Workshops and Doctoral
Consortium of the 41st International Conference on
Logic Programming, September 9–13, 2025, Rende,
Italy},
editor = {Azzolini, Damiano and Batsakis, Sotirios and
Santana, Manuel Alejandro Borroto and Bruno,
Pierangela and Cecchi, Laura A. and Fandinno, Jorge
and Hecher, Markus and Maratea, Marco and Morales,
José F. and Muñiz, Brais and Papadakis, Emmanuel and
Robaldo, Livio and Serafini, Luciano and Lo Scudo,
Fabrizio and Tachmazidis, Ilias and Tarzariol, Alice
and Vallati, Mauro and Wyner, Adam},
publisher = {CEUR Workshop Proceedings (CEUR-WS.org, ISSN
1613-0073)},
urn = {urn:nbn:de:0074-4117-x},
volume = 4117,
pages = {1-9},
url = {https://ceur-ws.org/Vol-4117/LPLR2025_short_1.pdf},
year = 2025,
}
@InProceedings{C100,
author = {David Fuenmayor and Christoph Benzm{\"u}ller},
title = {{HOL} as a Lingua Franca for Argumentative Reasoning Agents},
booktitle = {Conference on Artificial Intelligence and Theorem Proving (AITP-2025)},
editor = {Douglas, Michael R. and Hales, Thomas C. and Kaliszyk, Cezary and Schulz, Stephan and Urban, Josef},
publisher = {},
url = {https://aitp-conference.org/2025/abstract/AITP_2025_paper_22.pdf},
series = {},
volume = {},
pages = {},
OPTdoi = {},
year = 2025,
note = {(Extended abstract)},
}
@article{C98afp,
author = {Christoph Benzmüller},
title = {Faithful Logic Embeddings in {HOL} -- Deep and Shallow ({Isabelle/HOL} dataset)},
journal = {Archive of Formal Proofs (data publication)},
year = {2025},
OPTissn = {2150-914x},
url = {https://www.isa-afp.org/entries/FaithfulPMLinHOL.html},
}
@unblished{C99,
author = {Luca Pasetto and Liuwen Yu and Davide Liga and Christoph Benzm{\"u}ller},
title = {Generating Mental States for the Fatio Dialogue Protocol},
booktitle = {The Second International Conference of Bridges between Logic, Ethics and Social Sciences (BLESS), 20-22 June 2025, School of Philosophy, Shanxi University, Taiyuan, China},
editor = {Piotr Kulicki and Tomasz Jarmuzek and Fengkui Ju},
OPTdoi = {},
year = 2025,
OPTnote = {To appear/accepted},
}
@InProceedings{W74,
author = {Luca Pasetto and Christoph Benzm{\"u}ller},
title = {The Fatio Protocol for Formal Dialogue in Isabelle/HOL},
booktitle = {Workshop on Theorem Proving and Machine Learning in the age of LLMs: SoA and Future Perspectives, Edinburgh, Scotland, UK, April 7th-8th 2025},
editor = {Ekaterina Komendantskaya and Elizabeth Polgreen and Christian Saemann and Kathrin Stark and Michael Rawson},
publisher = {},
address = {},
series = {},
volume = {},
pages = {},
OPTdoi = {},
url = {https://europroofnet.github.io/_pages/WG5/Edinburgh25/abstracts/20.pdf},
year = 2025,
}
@inproceedings{C98,
author = {Christoph Benzmüller},
title = {Faithful Logic Embeddings in {HOL} --- Deep and Shallow},
booktitle = {Automated Deduction -- {CADE-30} -- 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings},
pages = {280--302},
year = 2025,
editor = {Clark Barrett and Uwe Waldmann},
series = {Lecture Notes in Computer Science},
doi = {10.1007/978-3-031-99984-0_16},
OPTurl = {https://doi.org/10.1007/978-3-031-99984-0},
url = {https://people.mpi-inf.mpg.de/~uwe/tmp/CADE-30-Proc.pdf},
volume = 15943,
publisher = {Springer},
note = {(preprint: {arXiv:2502.19311})},
}
@inproceedings{C97,
author = {Lara Lawniczak and Christoph Benzmüller},
title = {Logical Modalities within the European AI Act: An Analysis},
booktitle = {ICAIL '25: Proceedings of the Twentieth International Conference on Artificial Intelligence and Law},
editor = {Juliano Maranhão},
publisher = {ACM, New York, NY, USA},
pages = {348-353},
doi = {10.1145/3769126.3769202},
year = {2025},
note = {(preprint: arXiv:2501.19112)},
}
@inproceedings{W73,
author = {David Fuenmayor and Christoph Benzmüller},
title = {Searching for Wormholes in Proof-Space},
booktitle = {Proceedings of the 14th and 15th International Workshops on the Implementation of Logics},
editor = {Konstantin Korovin and Stephan Schulz and Michael Rawson},
series = {Kalpa Publications in Computing},
volume = {21},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2515-1762},
OPTurl= {https://easychair.org/publications/paper/scqG/},
doi = {10.29007/fc89},
pages = {15-17},
year = {2025}}
@misc{R80,
Author = {Christoph Benzm{\"u}ller},
Title = {Faithful Logic Embeddings in HOL -- Deep and Shallow (extended preprint)},
OPTUrl = {https://arxiv.org/abs/2502.19311},
Doi = {10.48550/arXiv.2502.19311},
OPTPublisher = {arXiv:2502.19311},
Note = {arXiv:2502.19311},
Year = {2025},
}
@misc{R79,
Author = {Lara Lawniczak and Christoph Benzm{\"u}ller},
Title = {Logical Modalities within the European AI Act: An Analysis (extended preprint)},
OPTUrl = {https://doi.org/10.48550/arXiv.2501.19112},
Doi = {10.48550/arXiv.2501.19112},
OPTPublisher = {arXiv:2501.19112},
Note = {arXiv:2501.19112},
Year = {2025},
}
@misc{R78,
Author = {Robert Wasenm{\"u}ller and Kevin Hilbert and Christoph Benzm{\"u}ller},
Title = {Script-Based Dialog Policy Planning for LLM-Powered Conversational Agents: A Basic Architecture for an "AI Therapist"},
OPTUrl = {http://arxiv.org/abs/2412.15242},
Doi = {10.48550/arXiv.2412.15242},
Publisher = {arXiv:2412.15242},
OPTNote = {Preprint},
Year = {2024},
}
@article{J70afp,
author = {Christoph Benzmüller and Scott, Dana S.},
title = {Notes on Gödel's and Scott's Variants of the Ontological Argument ({Isabelle/HOL} dataset)},
journal = {Archive of Formal Proofs (data publication)},
OPTvolume = {2025},
year = {2025},
url = {https://www.isa-afp.org/entries/Notes_On_Goedels_Ontological_Argument.html},
}
@article{J70,
title = {Notes on {Gödel's} and {Scott's} Variants of the Ontological Argument},
author = {Christoph Benzmüller and Scott, Dana S.},
year = 2025,
journal = {Monatshefte für Mathematik},
volume = {208},
pages = {569–611},
doi = {10.1007/s00605-025-02078-x},
}
@article{J72,
author = {Cordelia M{\"u}hlenbeck and Benzm{\"u}ller, Christoph},
Title = {On the maximality of positive properties and modal
collapse in variants of Gödel’s ontological proof of God},
journal = {Logic and Logical Philosophy},
url={https://apcz.umk.pl/LLP/article/view/55901},
doi = {10.12775/LLP.2026.007},
year = {2026},
OPTmonth = {3},
pages={1–21},
}
@InCollection{B28,
author = {Cordelia M{\"u}hlenbeck and Benzm{\"u}ller, Christoph},
title = {On Absolute Infinity and Modal Collapse in {Gödel's} Ontological Proof of {God}},
booktitle = {Logic, Knowledge, and Tradition: Essays in Honor of Srećko Kovač},
editor = {Filip Grgic and Kordula Swietorzecka and Anna Brozek},
OPTurl = {},
year = {2026},
publisher = {Brill},
addendum = {In print},
note = {In print},
isbn = {978-90-04-75635-9},
}
@article{J68,
Author = {Alexander Steen and Geoff Sutcliffe and Christoph Benzmüller},
Title = {Solving Quantified Modal Logic Problems by Translation to Classical Logics},
Journal = {Journal of Logic and Computation},
Doi = {10.1093/logcom/exaf006},
OPTEditor = {Andreas Herzig and Jieting Luo and Pere Pardo},
Publisher = {Oxford University Press},
volume = {35},
number = {4},
pages = {1-23},
year = {2025},
}
@article{J67,
author = {Alexander Steen and Christoph Benzm{\"u}ller},
title = {Non-Classical Reasoning for Contemporary AI Applications},
journal = {K{\"{u}}nstliche Intelligenz},
volume = {38},
number = {1-2},
pages = {3-5},
year = {2024},
OPTurl = {https://link.springer.com/article/10.1007/s13218-024-00857-6},
doi = {10.1007/s13218-024-00857-6},
}
@article{J66,
author = {Alexander Steen and Christoph Benzm{\"u}ller},
title = {Challenges for Non-Classical Reasoning in Contemporary AI
Applications},
journal = {K{\"{u}}nstliche Intelligenz},
volume = {38},
number = {1-2},
pages = {7-16},
year = {2024},
OPTurl = {https://link.springer.com/article/10.1007/s13218-024-00855-8},
doi = {10.1007/s13218-024-00855-8},
}
@inproceedings{W71,
Keywords = {own, Normative Reasoning, Machine Ethics},
Author = {Luca Pasetto and Christoph Benzm{\"u}ller},
Editor = {Christoph Benzm{\"u}ller and Jens Otten and Revantha Ramanayake},
booktitle = {Proceedings of the 5th International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2024), Nancy, France, July 1, 2024},
Title = {Implementing the {Fatio} Protocol for Multi-Agent Argumentation in {LogiKEy}},
publisher = {{CEUR} Workshop Proceedings, CEUR-WS.org},
address = {Nancy, Fance},
volume = {CEUR-3875},
url = {https://ceur-ws.org/Vol-3875/ARQNL2024_paper4.pdf},
pages = {38-47},
year = {2024},
urn = {urn:nbn:de:0074-3875-4},
issn = {1613-0073},
}
@book{E32,
Keywords = {own, Quantified Non-Classical Logics},
Author = {Christoph Benzm{\"u}ller and Jens Otten and Revantha Ramanayake},
Title = {Proceedings of the 5th International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2024), Nancy, France, July 1, 2024},
publisher = {{CEUR} Workshop Proceedings, CEUR-WS.org},
address = {Nancy, Fance},
volume = {CEUR-3875},
year = {2024},
url = {https://ceur-ws.org/Vol-3875/},
urn = {urn:nbn:de:0074-3875-4},
issn = {1603-0073},
pages = {1-107},
}
@inproceedings{W70,
author = {Zhang, Chengming and Solopova, Veronika and Romeike, Ralf and Gläser-Zikuda, Michaela and Benzmüller, Christoph and Landgraf, Tim and Hofmann, Florian and Schie{ß}l, Jessica and Plö{ß}l, Lea and Witte, Sascha},
booktitle = {Annual Conference of the European Teacher Education Network (ETEN) “Teacher Education – Connecting Glocal”},
title = {{PetraKIP}: {Personal} transparency {AI}-based portfolio for teacher education},
venue = {Nuremberg},
year = {2023},
url = {https://cris.fau.de/publications/296078483/}
}
@inproceedings{W69,
author = {Zhang, Chengming and Schie{ß}l, Jessica and Plö{ß}l, Lea and Hofmann, Florian and Gläser-Zikuda, Michaela and Solopova, Veronika and Romeike, Ralf and Benzmüller, Christoph and Landgraf, Tim and Witte, Sascha},
booktitle = {Annual Conference of the European Teacher Education Network (ETEN) “Teacher Education – Connecting Glocal”},
title = {{AI}-powered automatic feedback on reflective writing},
venue = {Nuremberg},
year = {2023},
url = {https://cris.fau.de/publications/296077264/}
}
@book{E31,
Keywords = {own, Argumentation, Logic},
editor = {Steen, Alexander and Benzmüller, Christoph},
title = {Special Issue on Non-Classical Reasoning for Contemporary AI Applications},
publisher = {KI -- Künstliche Intelligenz},
year = 2024,
url = {https://link.springer.com/journal/13218/volumes-and-issues/38-1},
}
@inproceedings{R77,
Author = {Benzm{\"u}ller, Christoph and Fuenmayor, David},
Title = {The {LogiKEy} Methodology: Applications in AI Ethics \& Prospects
for Logic Education},
OPTEditor = {},
Booktitle = {Formal Methods and Science in Philosophy V, International Conference,
Book of Abstracts},
Year = 2024,
Month = 5,
Publisher = {Institute of Philosophy, University of Zagreb},
Pages = {9--10},
Adress = {Inter-University Centre, Ul. don Frana Bulica 4, Dubrovnik, Croatia},
Url = {https://iuc.hr/file/1802},
}
@inproceedings{R76,
Author = {Cordelia M{\"u}hlenbeck and Benzm{\"u}ller, Christoph},
Title = {On the maximum of positive properties and modal collapse in Gödel's ontological argument compared to its variants},
OPTEditor = {},
Booktitle = {Formal Methods and Science in Philosophy V, International Conference,
Book of Abstracts},
Year = 2024,
Month = 5,
Pages = {31--32},
Adress = {Inter-University Centre, Ul. don Frana Bulica 4, Dubrovnik, Croatia},
Url = {https://iuc.hr/file/1802},
}
@article{J65,
author = {Christoph Benzm{\"u}ller and David Fuenmayor and Bertram Lomfeld},
title = {Modelling Value-oriented Legal Reasoning in {LogiKEy}},
journal = {Logics},
year = {2024},
volume = 2,
number = 1,
pages = {31-78},
doi = {10.3390/logics2010003},
OPTnote = {(Preprint arXiv:2006.12789)},
OPTaddendum = {(Preprint arXiv:2006.12789)}
}
@article{J64,
author = {Xavier Parent and Christoph Benzm{\"u}ller},
title = {Conditional Normative Reasoning as a Fragment of {HOL}},
journal = {Journal of Applied Non-Classical Logics},
year = {2024},
volume = {34},
number = {4},
pages = {561–592},
doi = {10.1080/11663081.2024.2386917},
OPTurl = {https://www.tandfonline.com/doi/full/10.1080/11663081.2024.2386917},
publisher = {Taylor \& Francis},
address = {London},
pages = {1-32},
}
@article{J64afp,
author = {Xavier Parent and Christoph Benzm{\"u}ller},
title = {Conditional Normative Reasoning as a Fragment of {HOL} ({Isabelle/HOL} dataset)},
journal = {Archive of Formal Proofs (data publication)},
OPTvolume = {2024},
year = {2024},
url = {https://www.isa-afp.org/entries/CondNormReasHOL.html},
}
@InCollection{B27,
author = {Benzm{\"u}ller, Christoph and Andrews, Peter},
title = {{Church’s Type Theory}},
booktitle = {The {Stanford} Encyclopedia of Philosophy},
editor = {Edward N. Zalta and Uri Nodelman},
url = {https://plato.stanford.edu/archives/spr2024/entries/type-theory-church/},
year = {2024},
edition = {{S}pring 2024},
publisher = {Metaphysics Research Lab, Stanford University},
addendum = {(substantive revision Jan 2024)},
}
@inproceedings{C96,
author = {Veronika Solopova and Viktoriia Herman and Christoph Benzm{\"u}ller and Tim Landgraf},
editor = {Nikolaos Aletras and Orph{\'{e}}e De Clercq},
title = {Check News in One Click: NLP-Empowered Pro-Kremlin Propaganda Detection},
booktitle = {Proceedings of the 18th Conference of the European Chapter of the
Association for Computational Linguistics, {EACL} 2024 - System Demonstrations,
St. Julians, Malta, March 17-22, 2024},
pages = {44--51},
publisher = {Association for Computational Linguistics},
year = {2024},
url = {https://aclanthology.org/2024.eacl-demo.6},
}
@misc{R75arxiv,
Author = {Veronika Solopova and Viktoriia Herman and Christoph Benzm{\"u}ller and Tim Landgraf},
Title = {Check News in One Click: NLP-Empowered Pro-Kremlin Propaganda Detection (preprint)},
OPTUrl = {https://arxiv.org/abs/2401.15717},
Doi = {10.48550/arXiv.2401.15717},
Publisher = {arXiv:2401.15717},
OPTNote = {Preprint},
Year = {2024},
}
@proceedings{E30,
Keywords = {own, Automated Reasoning, Logic},
editor = {Benzm{\"u}ller, Christoph and Heule, Marijn J.H. and Schmidt, Renate A.},
title = {Automated Reasoning -- 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part I},
publisher = {Springer},
address = {Cham},
year = 2024,
series = {LNAI},
volume = {14739},
Pages = {1-482},
OPTurl = {},
doi = {10.1007/978-3-031-63498-7},
isbn = {978-3-031-63497-0},
issn = {0302-9743},
}
@proceedings{E29,
Keywords = {own, Automated Reasoning, Logic},
editor = {Benzm{\"u}ller, Christoph and Heule, Marijn J.H. and Schmidt, Renate A.},
title = {Automated Reasoning -- 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part II},
publisher = {Springer},
address = {Cham},
year = 2024,
series = {LNAI},
volume = {14740},
Pages = {1-424},
OPTurl = {},
doi = {10.1007/978-3-031-63501-4},
isbn = {978-3-031-63501-4},
issn = {0302-9743},
}
@article{J63,
author = {Alexander Steen and Christoph Benzm{\"u}ller},
title = {What are Non-Classical Logics and why do we need them? An extended interview with Dov Gabbay and Leon van der Torre},
journal = {K{\"{u}}nstliche Intelligenz},
volume = {38},
number = {1-2},
pages = {17–23},
year = {2024},
doi = {10.1007/s13218-023-00824-7},
}
@incollection{B26,
author = {Lukas H{\"o}per and Carsten Schulte and Christoph Benzm{\"u}ller},
title = {Verantwortung},
booktitle = {Künstliche Intelligenz für Lehrkräfte -- Eine fachliche Einführung mit didaktischen Hinweisen},
editor = {Ulrich Furbach and Emanuel Kitzelmann and Tilmann Michaeli and Ute Schmid},
publisher = {Springer Vieweg},
address = {Wiesbaden},
year = 2024,
pages = {219-236},
doi = {10.1007/978-3-658-44248-4_16},
OPTurl = {https://link.springer.com/chapter/10.1007/978-3-658-44248-4_16},
}
@incollection{B25,
author = {Uli Furbach and Christoph Benzm{\"u}ller},
title = {Schlie{ß}en aus Wissen},
booktitle = {Künstliche Intelligenz für Lehrkräfte -- Eine fachliche Einführung mit didaktischen Hinweisen},
editor = {Ulrich Furbach and Emanuel Kitzelmann and Tilmann Michaeli and Ute Schmid},
publisher = {Springer Vieweg},
address = {Wiesbaden},
year = 2024,
pages = {39-50},
doi = {10.1007/978-3-658-44248-4_4},
OPTurl = {https://link.springer.com/chapter/10.1007/978-3-658-44248-4_4},
}
@incollection{B24,
author = {Christoph Benzm{\"u}ller},
title = {Logikbasierte Wissensverarbeitung},
booktitle = {Künstliche Intelligenz für Lehrkräfte -- Eine fachliche Einführung mit didaktischen Hinweisen},
editor = {Ulrich Furbach and Emanuel Kitzelmann and Tilmann Michaeli and Ute Schmid},
publisher = {Springer Vieweg},
address = {Wiesbaden},
year = 2024,
pages = {139-162},
doi = {10.1007/978-3-658-44248-4_11},
OPTurl = {https://link.springer.com/chapter/10.1007/978-3-658-44248-4_11},
}
@incollection{B23,
author = {Vestrucci, Andrea and Benzm{\"u}ller, Christoph},
title = {{Kurt Gödel} and the Logical Existence of God},
booktitle = {Divined Explanations. The Theological and Philosophical Context for the Development of the Sciences (1600-2000)},
editor = {Flavia Marcacci and Paul Allen},
publisher = {Brill},
series = {Philosophical Studies in Science and Religion},
year = 2024,
doi = {10.1163/9789004701908_013},
pages = {255–285},
}
@inproceedings{R75,
Author = {Christoph Benzmüller},
Title = {Is {HOL} (as a metalogic) all we need for flexible normative reasoning?},
Booktitle = {Normative Reasoning for AI},
Editor = {Ciabattoni, Agata and Horty, John F. and Slavkovik, Marija and van der Torre, Leendert and Knoks, Alex},
OPTUrl = {https://drops.dagstuhl.de/opus/volltexte/2023/19236/},
Doi = {10.4230/DagRep.13.4.1},
Pages = {22-23},
Publisher = {DROPS},
Note = {Talk abstract},
Year = 2023,
}
@article{J62,
author = {Bayer, Jonas and Benzm{\"u}ller, Christoph and
Buzzard, Kevin and David, Marco and Lamport, Leslie
and Matiyasevich, Yuri and Paulson, Lawrence and
Schleicher, Dierk and Stock, Benedikt and Zelmanov,
Efim},
title = {Mathematical Proof Between Generations},
journal = {Notices of the AMS},
doi = {10.1090/noti2860},
OPTurl = {https://www.ams.org/notices/202401/rnoti-p79.pdf},
number = {1},
volume = {71},
pages = {79-92},
year = 2024,
}
@incollection{B22,
Author = {Christoph Benzm{\"u}ller},
Keywords = {own, Computational Metaphysics, OntologicalArgument},
Title = {A Simplified Variant of {Gödel's} Ontological Argument},
Year = 2023,
OPTPages = {271-286},
Doi = {10.1007/978-3-031-42127-3_19},
url = {https://www.researchgate.net/publication/358607847},
Editor = {Andrea Vestrucci},
booktitle = {Beyond Babel: Religions and Linguistic Pluralism},
publisher = {Springer},
address = {Cham},
series = {Sophia Studies in Cross-cultural Philosophy of Traditions and Cultures},
volume = 43,
year = 2023,
}
@article{J61,
author = {Benzmüller, Christoph and Fuenmayor, David and Steen, Alexander and Sutcliffe, Geoff},
title = {Who Finds the Short Proof?},
journal = {Logic Journal of the IGPL},
publisher = {Oxford University Press},
volume = {32},
number = {3},
pages = {442–464},
doi = {10.1093/jigpal/jzac082},
OPTurl = {https://www.researchgate.net/publication/367464450_Who_Finds_the_Short_Proof},
year = 2024,
note = {(preprint: arXiv.2208.06879)},
}
@article{J61afp,
author = {Christoph Benzm{\"{u}}ller and
David Fuenmayor and Alexander Steen and Geoff Sutcliffe},
title = {Automation of Boolos' Curious Inference in Isabelle/HOL},
journal = {Archive of Formal Proofs (data publication)},
volume = {2022},
year = {2022},
url = {https://www.isa-afp.org/entries/Boolos_Curious_Inference_Automated.html},
}
@InProceedings{C91,
author = {Colin Rothgang and Florian Rabe and Christoph Benzmüller},
title = {Theorem Proving in Dependently-Typed Higher-Order Logic},
booktitle = {Automated Deduction - CADE 29. CADE 2023},
editor = {Brigitte Pientka and Cesare Tinelli},
publisher = {Springer},
address = {Cham},
series = {Lecture Notes in Artificial Intelligence},
volume = {14132},
pages = {438–455},
doi = {10.1007/978-3-031-38499-8_25},
year = 2023,
}
@InProceedings{C95,
Author = {Veronika Solopova and Eiad Rostom and Fritz Cremer and Adrian
Gruszczynski and Sascha Witte and Chengming Zhang and Lea Pl{\"o}{ß}l and Ralf Romeike and Michaela Gl{\"a}ser-Zikuda and Christoph Benzmüller and Tim Landgraf},
Title = {PapagAI: Automated Feedback for Reflective Essays},
OPTUrl = {https://link.springer.com/chapter/10.1007/978-3-031-42608-7_16},
Doi = {10.1007/978-3-031-42608-7_16},
Booktitle = {{KI} 2023: Advances in Artificial Intelligence --
46th German Conference on Artificial Intelligence,
Berlin, Germany, September 26-29, 2023,
Proceedings},
editor = {Dietmar Seipel and Alexander Steen},
series = {Lecture Notes in Artificial Intelligence},
volume = {14236},
pages = {198–206},
publisher = {Springer, Cham},
year = 2023,
}
@inproceedings{C94,
Author = {Alexander Steen and Geoff Sutcliffe and Tobias Scholl and Christoph Benzmüller},
Title = {Solving Modal Logic Problems by Translation to Higher-order Logic},
Booktitle = {Logic and Argumentation, 5th International
Conference, CLAR 2023, Hangzhou, China, September 2023, Proceedings},
OPTUrl = {https://link.springer.com/chapter/10.1007/978-3-031-40875-5_3},
Doi = {10.1007/978-3-031-40875-5_3},
Editor = {Andreas Herzig and Jieting Luo and Pere Pardo},
Pages = {25-43},
Publisher = {Springer},
Series = {Lecture Notes in Artificial Intelligence},
Volume = 14156,
Year = 2023,
addendum = {Best Paper Award},
}
@misc{R88arxiv,
Author = {Xavier Parent and Christoph Benzmüller},
Title = {Normative Conditional Reasoning as a Fragment of {HOL}},
OPTUrl = {https://arxiv.org/abs/2308.10686},
Doi = {10.48550/arXiv.2308.10686},
Publisher = {arXiv:2308.10686},
Note = {Preprint},
Year = 2023,
}
@misc{R87arxiv,
Author = {Veronika Solopova and Eiad Rostom and Fritz Cremer and Adrian
Gruszczynski and Sascha Witte and Chengming Zhang and Lea Pl{\"o}{ß}l and Ralf Romeike and Michaela Gl{\"a}ser-Zikuda and Christoph Benzmüller and Tim Landgraf},
Title = {PapagAI: Automated Feedback for Reflective Essays (Preprint)},
OPTUrl = {https://arxiv.org/abs/2307.07523},
Doi = {10.48550/arXiv.2307.07523},
publisher = {arXiv:2307.07523},
note = {Preprint},
year = 2023,
}
@inproceedings{C93,
author = {Christoph Benzmüller},
title = {Reasonable, Trusted AI through Symbolic Ethico-legal Control and Reflection? (Keynote Abstract)},
year = {2023},
publisher = {LibraryPress@UF},
address = {Florida},
journal = {The Florida Artificial Interlligence Research Society},
volume = {2023},
number = {36},
booktitle = {Proceedings of FLAIRS-36, May 14-17, 2023, Clearwater Beach, FL},
OPTurl = {https://journals.flvc.org/FLAIRS/article/view/133952/137945},
OPTurl = {https://fis.uni-bamberg.de/handle/uniba/59598},
doi = {10.32473/flairs.36},
issn = {2334-0762},
}
@misc{R86arxiv,
OPTdoi = {10.48550/arXiv.2305.15382},
url = {https://arxiv.org/abs/2306.09074},
author = {Jonas Bayer and Aleksey Gonus and Christoph Benzmüller and Dana S. Scott},
Title = {Category Theory in {Isabelle/HOL} as a Basis for Meta-logical Investigation -- Preprint},
publisher = {arXiv:2306.09074},
note = {Preprint},
year = 2023,
}
@inproceedings{C92,
Author = {Jonas Bayer and Aleksey Gonus and Christoph Benzmüller and Dana S. Scott},
Title = {Category Theory in {Isabelle/HOL} as a Basis for Meta-logical Investigation},
Booktitle = {Intelligent Computer Mathematics - International
Conference, {CICM} 2023, September 4–8, 2023, Cambridge, UK, Proceedings},
Doi = {10.1007/978-3-031-42753-4_5},
Editor = {Catherine Dubois and Manfred Kerber},
Pages = {69–83},
Publisher = {Springer},
Series = {Lecture Notes in Computer Science},
Volume = 14101,
Year = 2023,
}
@misc{R85arxiv,
doi = {10.48550/arXiv.2305.15382},
OPTurl = {https://arxiv.org/abs/2305.15382},
author = {Colin Rothgang and Florian Rabe and Christoph Benzmüller},
title = {Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint},
publisher = {arXiv:2305.15382},
note = {Extended Preprint},
year = 2023,
}
@InProceedings{C90,
Author = {Christoph Benzm{\"u}ller and David Fuenmayor},
Title = {Mathematical Proof Assistants for Teaching Logic: The {LogiKEy} Methodology},
Booktitle = {Book of Abstracts --- V Congress Tools for Teaching Logic},
year = 2023,
Address = {Madrid, Spain, March 23-24 2023},
doi = {10.13140/RG.2.2.24708.74888},
OPTUrl = {https://www.researchgate.net/publication/371044093}
}
@inproceedings{W68,
keywords = {own, Normative Reasoning, Machine Ethics},
author = {Veronica Solopova and Christoph Benzm{\"u}ller and Tim Landgraf},
editor = {Romanyshyn, Mariana},
booktitle = {Proceedings of the Second Ukrainian Natural Language Processing Workshop (UNLP 2023)},
title = {The evolution of Pro-Kremlin propaganda from Machine Learning and linguistic perspective},
publisher = {Association for Computational Linguistics},
doi = {10.18653/v1/2023.unlp-1.5},
year = {2023},
isbn = {978-1-959429-52-4},
pages = {40-48},
}
@article{J60,
author = {Solopova, Veronika and Popescu, Oana-Iuliana and Benzm{\"u}ller, Christoph and Landgraf, Tim},
title = {Automated multilingual detection of {Pro-Kremlin} propaganda in newspapers and {Telegram} posts},
journal = {Datenbank Spektrum},
publisher = {Springer},
volume = {23},
number = {1},
pages = {5-14},
year = 2023,
doi = {10.1007/s13222-023-00437-2},
OPTurl = {https://link.springer.com/article/10.1007/s13222-023-00437-2},
}
@misc{R84arxiv,
author = {Solopova, Veronika and Popescu, Oana-Iuliana and Benzm{\"u}ller, Christoph and Landgraf, Tim},
title = {Automated multilingual detection of {Pro-Kremlin} propaganda in newspapers and {Telegram} posts},
publisher = {arXiv:2301.10604},
note = {Preprint},
year = 2023,
doi = {10.48550/arXiv.2301.10604},
OPTurl = {https://arxiv.org/abs/2301.10604},
}
@misc{R83arxiv,
doi = {10.48550/arXiv.2212.09570},
OPTurl = {https://arxiv.org/abs/2212.09570},
author = {Steen, Alexander and Sutcliffe, Geoff and Glei{ß}ner, Tobias and Benzmüller, Christoph},
title = {Solving QMLTP Problems by Translation to Higher-order Logic},
publisher = {arXiv:2212.09570},
note = {Preprint},
year = 2022,
}
@article{J59,
keywords = {own, Argumentation, Logic},
author = {Baroni, Pietro and Benzmüller, Christoph and N Wáng, Yì},
title = {Preface: Special Issue on Logic and Argumentation},
journal = {Journal of Logic and Computation},
volume = {33},
number = {2},
page = {189-191},
year = {2023},
issn = {0955-792X},
doi = {10.1093/logcom/exac091},
OPTurl = {https://doi.org/10.1093/logcom/exac091},
OPTeprint = {https://academic.oup.com/logcom/advance-article-pdf/doi/10.1093/logcom/exac091/48747721/exac091.pdf},
}
@book{E27,
Keywords = {own, Argumentation, Logic},
editor = {Baroni, Pietro and Benzmüller, Christoph and N Wáng, Yì},
title = {Special Issue on Logic and Argumentation},
publisher = {Journal of Logic and Computation. Oxford University Press},
year = 2023,
OPTurl = {https://academic.oup.com/logcom/issue/33/2},
doi = {10.1093/logcom/exac091},
}
@book{E26,
Keywords = {own, Kurt Goedel, Philosophy, Physics},
editor = {Oliver Passon and Christoph Benzm{\"u}ller and Brigitte Falkenburg},
title = {On Gödel and the Nonexistence of Time – Gödel und die Nichtexistenz der Zeit},
publisher = {Springer Spektrum Berlin},
address = {Heidelberg},
year = 2023,
pages = {1-153},
isbn = {978-3-662-67044-6},
doi = {10.1007/978-3-662-67045-3},
OPTurl = {https://link.springer.com/book/9783662670446},
url_website = {https://kurtgoedel.de/press-release-2021/},
}
@misc{J61arxiv,
doi = {10.48550/arXiv.2208.06879},
OPTurl = {https://arxiv.org/abs/2208.06879},
author = {Benzmüller, Christoph and Fuenmayor, David and Steen, Alexander and Sutcliffe, Geoff},
title = {Who Finds the Short Proof? An Exploration of Variants of Boolos' Curious Inference using Higher-order Automated Theorem Provers},
publisher = {arXiv},
note = {Preprint},
year = 2022,
}
@misc{J62arxiv,
doi = {10.48550/ARXIV.2207.04779},
OPTurl = {https://arxiv.org/abs/2207.04779},
author = {Bayer, Jonas and Benzm{\"u}ller, Christoph and
Buzzard, Kevin and David, Marco and Lamport, Leslie
and Matiyasevich, Yuri and Paulson, Lawrence and
Schleicher, Dierk and Stock, Benedikt and Zelmanov,
Efim},
keywords = {History and Overview (math.HO), FOS: Mathematics,
FOS: Mathematics},
title = {Mathematical Proof Between Generations},
publisher = {arXiv},
note = {Preprint},
year = 2022,
copyright = {arXiv.org perpetual, non-exclusive license},
}
@article{J57,
author = {Henrik Mucha and Ana Correia de Barros and Jesse Josua Benjamin and Christoph Benzmüller and Andreas Bischof and Sandra Buchmüller and Alexandra de Carvalho and Anna-Katharina Dhungel and Claude Draude and Marc-Julian Fleck and Juliane Jarke and Stefanie Klein and Caroline Kortekaas and Albrecht Kurze and Diane Linke and Franzisca Maas and Nicola Marsden and Ricardo Melo and Susanne Michel and Claudia Müller-Birn and Monika Pröbster and Katja Antonia Rie{ß}enberger and Mirko Tobias Schäfer and Peter Sörries and Julia Stilke and Torben Volkmann and Anne Weibert and Wilhelm Weinhold and Sara Wolf and Isabel Zorn and Michael Heidt and Arne Berger},
doi = {10.1515/icom-2021-0030},
OPTurl = {https://doi.org/10.1515/icom-2021-0030},
title = {Collaborative Speculations on Future Themes for
Participatory Design in Germany},
journal = {i-com},
number = 2,
volume = 21,
year = 2022,
pages = {283--298},
}
@article{J56,
Author = {Christoph Benzm{\"u}ller},
Journal = {Zygon(r)},
Keywords = {Artificial Intelligence, Ontological Argument},
Title = {Symbolic {AI} and {Gödel's} Ontological Argument},
Year = 2022,
Issn = {05912385, 14679744},
Volume = {57},
number = {4},
pages = {953-962},
OPTurl = {https://onlinelibrary.wiley.com/doi/abs/10.1111/zygo.12830},
OPTeprint = {https://onlinelibrary.wiley.com/doi/pdf/10.1111/zygo.12830},
doi = {10.1111/zygo.12830}
}
@book{E28,
Keywords = {own, Quantified Non-Classical Logics},
Author = {Christoph Benzm{\"u}ller and Jens Otten},
Title = {ARQNL 2022: Automated Reasoning in Quantified Non-Classical Logics. 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). Haifa, Israel, August 11, 2022},
publisher = {{CEUR} Workshop Proceedings, CEUR-WS.org},
volume = {3326},
year = {2023},
url = {https://ceur-ws.org/Vol-3326},
urn = {urn:nbn:de:0074-3326-4},
issn = {1613-0073},
pages = {1-108},
}
@inproceedings{W67,
Keywords = {own, Normative Reasoning, Machine Ethics},
Author = {Xavier Parent and Christoph Benzm{\"u}ller},
Editor = {Christoph Benzm{\"u}ller and Jens Otten},
booktitle = {ARQNL 2022: Automated Reasoning in Quantified Non-Classical Logics. 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). Haifa, Israel, August 11, 2022},
Title = {Automated Verification of Deontic Correspondences in
{Isabelle/HOL} -- First Results},
publisher = {{CEUR} Workshop Proceedings, CEUR-WS.org},
volume = {3326},
year = {2023},
url = {https://ceur-ws.org/Vol-3326/},
urn = {urn:nbn:de:0074-3326-4},
issn = {1613-0073},
pages = {92-108},
}
@inproceedings{W66,
author = {Alexander Steen and
David Fuenmayor and
Tobias Glei{ß}ner and
Geoff Sutcliffe and
Christoph Benzm{\"{u}}ller},
editor = {Boris Konev and
Claudia Schon and
Alexander Steen},
title = {Automated Reasoning in Non-classical Logics in the {TPTP} World},
booktitle = {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 - 12, 2022},
series = {{CEUR} Workshop Proceedings},
volume = {3201},
publisher = {CEUR-WS.org},
year = {2022},
url = {http://ceur-ws.org/Vol-3201/paper11.pdf},
}
@misc{W66arxiv,
doi = {10.48550/arXiv.2202.09836},
OPTurl = {https://arxiv.org/abs/2202.09836},
author = {Alexander Steen and
David Fuenmayor and
Tobias Glei{ß}ner and
Geoff Sutcliffe and
Christoph Benzm{\"{u}}ller},
title = {Automated Reasoning in Non-classical Logics in the {TPTP} World},
year = {2022},
OPTurl = {https://arxiv.org/abs/2202.09836},
publisher = {arXiv},
note = {Preprint},
}
@inproceedings{W65,
Keywords = {own, Normative Reasoning, Machine Ethics},
Author = {David Fuenmayor and Christoph Benzm{\"u}ller},
Editor = {Beishui Liao and Reka Markovich and W\'ang, Y\`i N.},
Booktitle = {Logics for New-Generation AI. Second International
Workshop. 10-12 June 2022, Zhuhai},
Title = {Higher-order Logic as a Lingua Franca for
Logico-Pluralist Argumentation},
pages = {83-94},
isbn = {978-1-84890-406-4},
publisher = {College Publications},
url =
{http://www.collegepublications.co.uk/downloads/LNGAI00002.pdf},
Year = 2022,
}
@misc{J59arxiv,
doi = {10.48550/ARXIV.2006.12789},
OPTurl = {https://arxiv.org/abs/2006.12789},
author = {Benzm{\"u}ller, Christoph and Fuenmayor, David and
Lomfeld, Bertram},
title = {Modelling Value-oriented Legal Reasoning in {LogiKEy}},
publisher = {arXiv},
note = {Preprint},
year = 2020,
copyright = {arXiv.org perpetual, non-exclusive license}
}
@misc{B22arxiv,
doi = {10.48550/ARXIV.2202.06264},
OPTurl = {https://arxiv.org/abs/2202.06264},
author = {Benzm{\"u}ller, Christoph},
title = {A Simplified Variant of Gödel's Ontological
Argument},
publisher = {arXiv},
note = {Preprint},
year = 2022,
copyright = {arXiv.org perpetual, non-exclusive license}
}
@article{J58,
Author = {Christoph Benzm{\"u}ller and Sebastian Reiche},
Journal = {Journal of Logic and Computation},
Keywords = {own, Artificial Intelligence, Non-Classical Logics,
Semantical Embedding, Common Knowledge},
Title = {Automating Public Announcement Logic with
Relativized Common Knowledge as a Fragment of {HOL} in
{LogiKEy}},
Year = 2023,
Volume = {33},
Number = {6},
Pages = {1243–1269},
url = {https://www.researchgate.net/publication/355872829},
OPTurl = {https://doi.org/10.1093/logcom/exac029},
doi = {10.1093/logcom/exac029}
}
@misc{J58arxiv,
doi = {10.48550/ARXIV.2111.01654},
OPTurl = {https://arxiv.org/abs/2111.01654},
author = {Benzm{\"u}ller, Christoph and Reiche, Sebastian},
title = {Automating Public Announcement Logic with
Relativized Common Knowledge as a Fragment of {HOL} in
{LogiKEy}},
publisher = {arXiv},
note = {Preprint},
year = 2021,
copyright = {arXiv.org perpetual, non-exclusive license}
}
@inproceedings{C89,
author = {Solopova, Veronika and
Popescu, Oana-Iuliana and
Chikobava, Margarita and
Romeike, Ralf and
Landgraf, Tim and
Benzm{\"u}ller, Christoph},
editor = {Bandyopadhyay, Sivaji and Devi, Sobha Lalitha and Bhattacharyya, Pushpak},
title = {A {G}erman Corpus of Reflective Sentences},
booktitle = {Proceedings of the 18th International Conference on Natural Language Processing (ICON)},
month = 12,
year = 2021,
address = {National Institute of Technology Silchar, Silchar, India},
publisher = {NLP Association of India (NLPAI)},
url = "https://aclanthology.org/2021.icon-main.72",
pages = "593--600",
}
@article{J55,
Author = {Christoph Benzm{\"u}ller and Sebastian Reiche},
Journal = {Archive of Formal Proofs (data publication)},
Keywords = {own, Artificial Intelligence, Non-Classical Logics,
Semantical Embedding, Common Knowledge},
Title = {Automating Public Announcement Logic and the Wise
Men Puzzle in {Isabelle/HOL}},
Url = {https://www.isa-afp.org/entries/PAL.html},
Year = 2021,
Pages = {1-5},
}
@inproceedings{C88,
Keywords = {own, Ethical and Legal Reasoning},
Author = {Benzm{\"u}ller, Christoph and Fuenmayor, David},
Editor = {Liron Cohen and Cezary Kaliszyk},
doi = {10.4230/LIPIcs.ITP.2021.7},
Title = {Value-oriented Legal Argumentation in
{Isabelle/HOL}},
Booktitle = {{International Conference on Interactive Theorem
Proving (ITP), Proceedings}},
series = {LIPIcs},
volume = 193,
number = 23,
pages = {23:1-23:18},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r
Informatik},
url = {https://dx.doi.org/10.13140/RG.2.2.21514.80320},
Year = 2021,
}
@techreport{R74,
Keywords = {own, Logic, Mathematics, Set Theory},
Author = {Benzm{\"u}ller, Christoph and Fuenmayor, David},
Institution = {University of Bamberg},
doi = {10.13140/RG.2.2.31069.95201/1},
Title = {Cantor's Theorem without Reductio Ad Absurdum},
url = {https://dx.doi.org/10.13140/RG.2.2.31069.95201/1},
Year = 2021,
}
@book{E25,
Keywords = {own, Kurt Goedel, Reductionism, Philosophy, Physics},
editor = {Oliver Passon and Christoph Benzm{\"u}ller},
title = {Wider den Reduktionismus -- Ausgewählte Beiträge zum
Kurt Gödel Preis 2019},
publisher = {Springer Spektrum},
year = 2021,
pages = {1--150},
isbn = {978-3-662-63187-4},
doi = {10.1007/978-3-662-63187-4},
OPTurl = {https://www.springer.com/de/book/9783662631867},
url_website = {https://kurtgoedel.de/kurt-goedel-prize-2019/},
url = {https://www.researchgate.net/publication/349493659},
}
@Proceedings{E24,
Keywords = {own, Argumentation, Logic},
editor = {Pietro Baroni and Christoph Benzm{\"u}ller and
W\'ang, Y\`i N.},
title = {Logic and Argumentation, 4th International
Conference, CLAR 2021, Hangzhou, China, October
20–22, 2021, Proceedings},
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
year = 2021,
pages = {1-552},
OPTurl = {https://link.springer.com/book/10.1007/978-3-030-89391-0},
doi = {10.1007/978-3-030-89391-0},
isbn = {978-3-030-89390-3},
issn = {0302-9743}
}
@book{E23,
Keywords = {own, AI, Ethics},
editor = {Sabine Ammon and Birgit Beck and Christoph
Benzm{\"u}ller and Aljoscha Burchardt and Marie Lena
Heidingsfelder and Simone Kaiser and Bertram Lomfeld
and Rainer M{\"u}hlhoff and Peter Remmers and
Martina Schraudner},
title = {KI als Laboratorium? Ethik als Aufgabe!},
isbn = {978-3-939818-93-9},
publisher = {Interdisziplin{\"a}re Arbeitsgruppe Verantwortung:
Maschinelles Lernen und K{\"u}nstliche Intelligenz},
series = {\#VerantwortungKI - K{\"u}nstliche Intelligenz und
gesellschaftliche Folgen},
number = 3,
pages = 52,
year = 2020,
url = {https://edoc.bbaw.de/frontdoor/index/index/docId/3449}
}
@Article{J52,
keywords = {own, Artificial Intelligence, Ethical and Legal
Issues},
title = {Tr{\"a}umen vernünftige Maschinen von Gr{\"u}nden?
Eine reale Utopie},
author = {Christoph Benzm{\"u}ller and Bertram Lomfeld},
journal = {VerantwortungKI – Künstliche Intelligenz und
gesellschaftliche Folgen (Berlin-Brandenburgische
Akademie der Wissenschaften)},
publisher = {Interdisziplinäre Arbeitsgruppe Verantwortung:
Maschinelles Lernen und Künstliche Intelligenz der
Berlin-Brandenburgischen Akademie der
Wissenschaften},
volume = 3,
year = 2020,
isbn = {978-3-939818-90-8},
url = {https://www.bbaw.de/files-bbaw/user_upload/publikationen/BBAW_Verantwortung-KI-3-2020_PDF-A-1b.pdf},
annote = {Open access},
}
@incollection{B21,
Keywords = {own, Higher Order Logic, Deontic Logic, Automated
Reasoning, Universal Reasoning},
Author = {Benzm{\"u}ller, Christoph and Farjami, Ali and
Parent, Xavier},
editor = {Shahid Rahman and Matthias Armgardt and Nordtveit
Kvernenes and Hans Christian},
booktitle = {New Developments in Legal Reasoning and Logic: From
Ancient Law to Modern Legal Systems},
series = {Logic, Argumentation \& Reasoning},
title = {Dyadic Deontic Logic in {HOL}: Faithful Embedding and
Meta-Theoretical Experiments},
volume = 23,
publisher = {Springer Nature Switzerland AG},
year = 2022,
doi = {10.1007/978-3-030-70084-3_14},
url = {https://doi.org/10.13140/RG.2.2.35175.88487},
isbn = {978-3-030-70083-6},
issn = {2214-9120},
}
@InProceedings{C87,
Keywords = {own, Artificial Intelligence, Non-Classical Logics},
Author = {Sebastian Reiche and Christoph Benzm{\"u}ller},
Title = {Public Announcement Logic in {HOL}},
url = {https://arxiv.org/abs/2010.00810},
OPTurl = {https://doi.org/10.1007/978-3-030-65840-3_14},
Doi = {10.1007/978-3-030-65840-3_14},
Booktitle = {Dynamic Logic. New Trends and Applications. DaLi
2020},
editor = {Martins, Manuel A. and Sedl\'{a}r Igor},
series = {Lecture Notes in Computer Science},
volume = 12569,
publisher = {Springer, Cham},
year = 2020,
isbn = {978-3-030-65839-7},
}
@misc{C87arxiv,
doi = {10.48550/ARXIV.2010.00810},
OPTurl = {https://arxiv.org/abs/2010.00810},
author = {Reiche, Sebastian and Benzm{\"u}ller, Christoph},
title = {Public Announcement Logic in {HOL}},
publisher = {arXiv},
note = {Preprint},
year = 2020,
copyright = {arXiv.org perpetual, non-exclusive license}
}
@InProceedings{C86,
Author = {Benzm{\"u}ller, Christoph and Parent, Xavier and van
der Torre, Leendert},
Keywords = {own, Normative Reasoning, Deontic Logic, Machine
Ethics, Formal Methods, Automated Reasoning, ProoF
Assistants, Explainable AI},
Title = {Designing Normative Theories for Ethical and Legal
Reasoning: {LogiKEy} Framework, Methodology, and Tool
Support (extended abstract)},
Booktitle = {17th Conference on Principles of Knowledge
Representation and Reasoning (KR 2020), Recently
Published Research track},
Year = 2020,
url = {https://www.researchgate.net/publication/343676062},
}
@misc{R81arxiv,
doi = {10.48550/ARXIV.2007.01019},
OPTurl = {https://arxiv.org/abs/2007.01019},
author = {Fuenmayor, David and Benzm{\"u}ller, Christoph},
title = {Higher-order Logic as Lingua Franca -- Integrating
Argumentative Discourse and Deep Logical Analysis},
publisher = {arXiv},
note = {Preprint},
year = 2020,
copyright = {arXiv.org perpetual, non-exclusive license}
}
@InProceedings{C85,
Keywords = {own, Artificial Intelligence, Ethical and Legal
Issues},
Author = {Christoph Benzm{\"u}ller and David Fuenmayor and
Bertram Lomfeld},
Title = {Encoding Legal Balancing: Automating an Abstract
Ethico-Legal Value Ontology in Preference Logic},
Booktitle = {Workshop on Models of Legal Reasoning, hosted by
17th Conference on Principles of Knowledge
Representation and Reasoning (KR 2020)},
Editor = {Juliano Maranhao and Giovanni Sartor},
url_arxiv = {https://arxiv.org/abs/2006.12789},
url = {https://www.researchgate.net/publication/342380027},
year = 2020,
}
@InProceedings{C84,
Keywords = {own, Artificial Intelligence, Ethical and Legal
Issues},
Author = {Christoph Benzm{\"u}ller and Bertram Lomfeld},
Title = {Reasonable Machines: A Research Manifesto},
url = {https://dx.doi.org/10.13140/RG.2.2.28918.63045},
OPTurl = {https://doi.org/10.1007/978-3-030-58285-2_20},
Doi = {10.1007/978-3-030-58285-2_20},
Booktitle = {{KI} 2020: Advances in Artificial Intelligence --
43rd German Conference on Artificial Intelligence,
Bamberg, Germany, September 21–25, 2020,
Proceedings},
editor = {Ute Schmid and Franziska Klügl and Diedrich Wolter},
series = {Lecture Notes in Artificial Intelligence},
volume = 12352,
pages = {251--258},
publisher = {Springer, Cham},
year = 2020,
isbn = {978-3-030-30178-1},
}
@InProceedings{C83,
Keywords = {own, Artificial Intelligence, Free Logic, Higher
Order Logic},
Author = {Irina Makarenko and Christoph Benzm{\"{u}}ller},
Title = {Positive Free Higher-Order Logic and its Automation
via a Semantical Embedding},
Note = {EasyChair Preprint no. 3621, EasyChair},
OPTurl = {https://doi.org/10.1007/978-3-030-58285-2_9},
Doi = {10.1007/978-3-030-58285-2_9},
Booktitle = {{KI} 2020: Advances in Artificial Intelligence --
43rd German Conference on Artificial Intelligence,
Bamberg, Germany, September 21–25, 2020,
Proceedings},
editor = {Ute Schmid and Franziska Kl{\"{u}}gl and Diedrich
Wolter},
series = {Lecture Notes in Artificial Intelligence},
volume = 12352,
publisher = {Springer, Cham},
year = 2020,
pages = {116--131},
isbn = {978-3-030-30178-1},
}
@InProceedings{C82,
Keywords = {own, Ontological Argument, Computational
Metaphysics, Higher Order Logic, Semantic Embedding,
Modal Logics, Automated Reasoning, Ontology
Reasoning},
title = {{A (Simplified) Supreme Being Necessarily Exists,
says the Computer: Computationally Explored Variants
of Gödel's Ontological Argument}},
author = {Benzm{\"u}ller, Christoph},
booktitle = {{Proceedings of the 17th International Conference on
Principles of Knowledge Representation and
Reasoning, KR 2020}},
pages = {779--789},
year = 2020,
month = 9,
doi = {10.24963/kr.2020/80},
OPTurl = {https://doi.org/10.24963/kr.2020/80},
publisher = {IJCAI organization},
}
@article{J54,
author = {Christoph Benzm{\"{u}}ller and Xavier Parent and
Francesco Ricca},
title = {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)},
journal = {Theory and Practice of Logic Programmming},
volume = 21,
number = 1,
pages = {1--3},
year = 2021,
OPTurl = {https://doi.org/10.1017/S1471068420000113},
doi = {10.1017/S1471068420000113},
}
@incollection{B20,
Author = {Christoph Benzm{\"u}ller},
Title = {Studies in Computational Metaphysics, Results of an
Interdisciplinary Research Project},
Booktitle = {Tópicos em História e Filosofia da Computação},
Editor = {Cukierman, Henrique and Bertato, Fabio},
Keywords = {own, Ontology Reasoning, Automated Reasoning, Higher
Order Logic, Computational Metaphysics},
Volume = {87},
Series = {COLEÇÃO CLE},
Publisher = {Centre for Logic, Epistemology and the History of
Science (CLE), University of Campinas (UNICAMP)},
Year = 2020,
url = {https://www.cle.unicamp.br/ebooks/index.php/publicacoes/catalog/book/31},
ISSN = {0103-3247},
OPTISBN = {978-65-88097-04-5},
pages = {129-160},
}
@techreport{R73,
Author = {Benzm{\"u}ller, Christoph and Reiche, Sebastian},
Keywords = {own, Higher Order Logic, Hintikka Sets, Completeness
Proofs},
Title = {Automating Public Announcement Logic with
Relativized Common Knowledge as a Fragment of {HOL} in
{LogiKEy}},
Institution = {CoRR},
Number = {arXiv:2111.01654},
eprint = {2111.01654},
Url = {https://arxiv.org/abs/2111.01654},
Year = 2021
}
@misc{R78arxiv,
doi = {10.48550/ARXIV.2004.07506},
OPTurl = {https://arxiv.org/abs/2004.07506},
author = {Steen, Alexander and Benzm{\"u}ller, Christoph},
title = {On Reductions of Hintikka Sets for Higher-Order
Logic},
publisher = {arXiv},
note = {Preprint},
year = 2020,
copyright = {arXiv.org perpetual, non-exclusive license}
}
@Proceedings{E22,
Keywords = {own},
editor = {Christoph Benzm{\"u}ller and Bruce Miller},
title = {Intelligent Computer Mathematics - 13th
International Conference, {CICM} 2020, Bertinoro,
Italy, July 26-31, 2020, Proceedings},
series = {Lecture Notes in Artificial Intelligence},
volume = 12236,
publisher = {Springer},
year = 2020,
pages = {1--337},
OPTurl = {https://doi.org/10.1007/978-3-030-53518-6},
doi = {10.1007/978-3-030-53518-6},
isbn = {978-3-030-53517-9},
issn = {0302-9743}
}
@article{J51,
Keywords = {own, Normative Reasoning, Deontic Logic, Machine
Ethics, Formal Methods, Automated Reasoning, ProoF
Assistants, Explainable AI},
Author = {Benzm{\"u}ller, Christoph and Farjami, Ali and
Fuenmayor, David and Meder, Paul and Parent, Xavier
and Steen, Alexander and van der Torre, Leendert and
Zahoransky, Valeria},
Journal = {Data in Brief (data publication)},
Publisher = {Elsevier},
Title = {{LogiKEy} Workbench: Deontic Logics, Logic
Combinations and Expressive Ethical and Legal
Reasoning ({Isabelle/HOL} Dataset)},
Volume = 33,
Number = 106409,
Year = 2020,
OPTUrl = {https://doi.org/10.1016/j.dib.2020.106409},
Doi = {10.1016/j.dib.2020.106409},
Pages = {1-10},
}
@inproceedings{C81,
Keywords = {own, Normative Reasoning, Deontic Logic, Machine
Ethics, Formal Methods, Automated Reasoning, ProoF
Assistants, Explainable AI},
Author = {David Fuenmayor and Christoph Benzm{\"u}ller},
Booktitle = {Logic and Argumentation, Fourth International
Conference, {CLAR} 2021, Hangzhou, China, April 6-9,
2020, Proceedings},
Editor = {Dastani, Mehdi and Dong, Huimin and van der Torre,
Leon},
Series = {Lecture Notes in Computer Science},
volume = 12061,
pages = {104-115},
Publisher = {Springer, Cham},
Year = 2020,
Title = {Computer-supported Analysis of Arguments in Climate
Engineering},
OPTurl =
{https://link.springer.com/chapter/10.1007/978-3-030-44638-3_7},
url = {https://www.researchgate.net/publication/338829452},
doi = {10.1007/978-3-030-44638-3_7},
}
@inproceedings{C80,
Keywords = {own, Normative Reasoning, Deontic Logic, Machine
Ethics, Formal Methods, Automated Reasoning, ProoF
Assistants, Explainable AI},
Author = {David Fuenmayor and Christoph Benzm{\"u}ller},
Booktitle = {{ECAI} 2020 -- 24th European Conference on
Artificial Intelligence, June 8-12, Santiago de
Compostela, Spain},
Editor = {De Giacomo, G. and Catala, A. and Dilkina, B. and
Milano, M. and Barro, S. and Bugarín, A. and Lang,
J.},
Series = {Frontiers in Artificial Intelligence and
Applications},
volume = 325,
Publisher = {{IOS} Press},
Year = 2020,
OPTurl = {https://dx.doi.org/10.3233/FAIA200445},
Title = {Normative Reasoning with Expressive Logic
Combinations},
url = {https://www.researchgate.net/publication/339413206},
pages = {2903-2904},
doi = {10.3233/FAIA200445},
}
@inproceedings{C79,
Keywords = {own, Higher Order Logic, Automated Reasoning, LEO
Prover},
Author = {Alexander Steen and Christoph Benzm{\"u}ller},
Booktitle = {{ECAI} 2020 -- 24th European Conference on
Artificial Intelligence, June 8-12, Santiago de
Compostela, Spain},
Editor = {De Giacomo, G. and Catala, A. and Dilkina, B. and
Milano, M. and Barro, S. and Bugarín, A. and Lang,
J.},
Series = {Frontiers in Artificial Intelligence and
Applications},
volume = 325,
Publisher = {{IOS} Press},
Year = 2020,
Title = {The Higher-Order Prover {Leo-III}},
OPTurl = {https://dx.doi.org/10.3233/FAIA200462},
url = {https://www.researchgate.net/publication/339413198},
pages = {2937-2938},
doi = {10.3233/FAIA200462},
}
@InProceedings{C77,
Keywords = {own, Automated Reasoning, Higher Order Logic, Legal
Reasoning, Formal Methods},
Author = {Valeria Zahoransky and Christoph Benzm{\"u}ller},
title = {Modelling the US Constitution to establish
constitutional dictatorship},
booktitle = {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)},
year = 2019,
publisher = {CEUR Workshop Proceedings, Vol-2632},
Url = {http://ceur-ws.org/Vol-2632/MIREL-19_paper_1.pdf},
}
@InProceedings{C78,
Keywords = {own, Automated Reasoning, Free Logic, Higher Order
Logic, Category Theory, Algebraic Structures,
Modeloids},
Author = {Lucca Tiemens and Dana S. Scott and Christoph
Benzm{\"u}ller and Miroslav Benda},
title = {Computer-supported Exploration of a Categorical
Axiomatization of Modeloids},
booktitle = {Relational and Algebraic Methods in Computer Science
-- 18th International Conference, {RAMiCS 2020},
Palaiseau, France, April 8--11, 2020, Proceedings},
editors = {Uli Fahrenberg and Peter Jipsen and Michael Winter},
year = 2020,
series = {Lecture Notes in Computer Science},
OPTurl =
{https://www.springerprofessional.de/computer-supported-exploration-of-a-categorical-axiomatization-o/17853766},
publisher = {Springer},
volume = 12062,
pages = {302--317},
doi = {10.1007/978-3-030-43520-2_19},
url = {https://www.researchgate.net/publication/336838722},
}
@misc{C78arxiv,
doi = {10.48550/ARXIV.1910.12863},
OPTurl = {https://arxiv.org/abs/1910.12863},
author = {Tiemens, Lucca and Scott, Dana S. and
Benzm{\"u}ller, Christoph and Benda, Miroslav},
title = {Computer-supported Exploration of a Categorical
Axiomatization of Modeloids},
publisher = {arXiv},
note = {Preprint},
year = 2019,
copyright = {arXiv.org perpetual, non-exclusive license}
}
@article{J50afp,
Author = {Christoph Benzm{\"u}ller},
Journal = {Archive of Formal Proofs (data publication)},
Keywords = {own},
Title = {Exploring Simplified Variants of Gödel’s Ontological Argument in {Isabelle/HOL}},
Url = {https://www.isa-afp.org/entries/SimplifiedOntologicalArgument.html},
Year = 2021,
Pages = {1-15},
}
@article{J50,
Author = {Christoph Benzm{\"u}ller and David Fuenmayor},
Journal = {Bulletin of the Section of Logic},
Publisher = {Department of Logic, University of Lodz},
Keywords = {own, Ontological Argument, Computational
Metaphysics, Higher Order Logic, Semantic Embedding,
Modal Logics, Automated Reasoning, Ontology
Reasoning},
Title = {Computer-supported Analysis of Positive Properties,
Ultrafilters and Modal Collapse in Variants of
{G\"odel's} Ontological Argument},
OPTUrl = {https://czasopisma.uni.lodz.pl/bulletin/article/view/7976},
Year = 2020,
Volume = 49,
Number = 2,
Doi = {10.18778/0138-0680.2020.08},
url = {https://www.researchgate.net/publication/336742445},
Pages = {127-148},
}
@misc{J50arxiv,
doi = {10.48550/ARXIV.1910.08955},
OPTurl = {https://arxiv.org/abs/1910.08955},
author = {Benzm{\"u}ller, Christoph and Fuenmayor, David},
title = {Computer-supported Analysis of Positive Properties,
Ultrafilters and Modal Collapse in Variants of
Gödel's Ontological Argument},
publisher = {arXiv},
note = {Preprint},
year = 2019,
copyright = {arXiv.org perpetual, non-exclusive license}
}
@article{J53,
Author = {Steen, Alexander and Benzm{\"u}ller, Christoph},
title = {Extensional Higher-Order Paramodulation in {Leo-III}},
journal = {Journal of Automated Reasoning},
volume = {65},
number = {6},
pages = {775--807},
year = {2021},
OPTOPTurl = {https://doi.org/10.1007/s10817-021-09588-x},
doi = {10.1007/s10817-021-09588-x}
}
@misc{J53arxiv,
doi = {10.48550/ARXIV.1907.11501},
OPTurl = {https://arxiv.org/abs/1907.11501},
author = {Steen, Alexander and Benzm{\"u}ller, Christoph},
title = {Extensional Higher-Order Paramodulation in {Leo-III}},
publisher = {arXiv},
note = {Preprint},
year = 2019,
copyright = {arXiv.org perpetual, non-exclusive license}
}
@misc{W64,
Author = {Benzm{\"u}ller, Christoph and Sutcliffe, Geoff},
Keywords = {own, Normative Reasoning, Machine Ethics},
Note = {The Second International ARCADE (Automated
Reasoning: Challenges, Applications, Directions,
Exemplary Achievements) Workshop.},
url = {http://christoph-benzmueller.de/papers/W64.pdf},
Title = {Explicit Normative Reasoning and Machine Ethics},
Year = 2019,
}
@article{J49,
Author = {Kirchner, Daniel and Benzm{\"u}ller, Christoph and
Zalta, Edward N.},
Keywords = {own, Higher Order Logic, Higher Order Modal Logic,
Universal Reasoning, Computational Metaphysics},
Title = {Mechanizing Principia Logico-Metaphysica in
Functional Type Theory},
Journal = {Review of Symbolic Logic},
Volume = 13,
Number = 1,
Publisher = {Cambridge University Press},
Doi = {10.1017/S1755020319000297},
pages = {206-218},
url = {https://www.researchgate.net/publication/321160582},
Year = 2020,
}
@incollection{B18,
Keywords = {own, Computational Hermeneutics, Higher Order Logic,
Universal Reasoning, Rational Argumentation,
Human-Machine Interaction},
Author = {Fuenmayor, David and Benzm{\"u}ller, Christoph},
Title = {A Computational-Hermeneutic Approach for Conceptual
Explicitation},
Booktitle = {Model-Based Reasoning in Science and
Technology. Inferential Models for Logic, Language,
Cognition and Computation},
Editor = {A. Nepomuceno and L. Magnani and F. Salguero and
C. Bares and M. Fontaine},
Publisher = {Springer},
Series = {SAPERE},
Volume = 49,
Pages = {441-469},
Year = 2019,
Doi = {10.1007/978-3-030-32722-4_25},
url = {http://doi.org/10.13140/RG.2.2.30869.78564},
}
@misc{B18arxiv,
doi = {10.48550/ARXIV.1906.06582},
OPTurl = {https://arxiv.org/abs/1906.06582},
author = {Fuenmayor, David and Benzm{\"u}ller, Christoph},
title = {A Computational-Hermeneutic Approach for Conceptual
Explicitation},
publisher = {arXiv},
note = {Preprint},
year = 2019,
copyright = {arXiv.org perpetual, non-exclusive license}
}
@InProceedings{C76,
Keywords = {own, Higher Order Logic, Universal Reasoning, Logic
Combinations, Machine Ethics},
author = {Fuenmayor, David and Benzm{\"u}ller, Christoph},
title = {Mechanised Assessment of Complex Natural-Language
Arguments using Expressive Logic Combinations},
booktitle = {Frontiers of Combining Systems, 12th International
Symposium, FroCoS 2019, London, September 4-6},
editor = {Andreas Herzig and AndreiPopescu},
year = 2019,
series = {Lecture Notes in Artificial Intelligence},
volume = 11715,
publisher = {Springer Nature Switzerland AG},
doi = {10.1007/978-3-030-29007-8_7},
url = {http://doi.org/10.13140/RG.2.2.20803.45608/1},
pages = {112--128},
}
@InProceedings{C75,
Keywords = {own, Higher Order Logic, Deontic Logic, Automated
Reasoning, Universal Reasoning, Machine Ethics},
author = {Fuenmayor, David and Benzm{\"u}ller, Christoph},
editor = {Abhaya Nayak and Alok Sharma},
title = {Harnessing Higher-Order (Meta-)Logic to Represent
and Reason with Complex Ethical Theories},
booktitle = {PRICAI 2019: Trends in Artificial Intelligence},
year = 2019,
series = {Lecture Notes in Artificial Intelligence},
volume = 11670,
publisher = {Springer, Cham},
url = {http://arxiv.org/abs/1903.09818},
pages = {418--432},
doi = {10.1007/978-3-030-29908-8_34},
}
@misc{C75arxiv,
doi = {10.48550/ARXIV.1903.09818},
OPTurl = {https://arxiv.org/abs/1903.09818},
author = {Fuenmayor, David and Benzm{\"u}ller, Christoph},
title = {Harnessing Higher-Order (Meta-)Logic to Represent
and Reason with Complex Ethical Theories},
publisher = {arXiv},
note = {Preprint},
year = 2019,
copyright = {arXiv.org perpetual, non-exclusive license}
}
@proceedings{E21,
title = {Selected Student Contributions and Workshop Papers
of LuxLogAI 2018},
editor = {Christoph Benzm{\"u}ller and Xavier Parent and
Alexander Steen},
series = {Kalpa Publications in Computing},
volume = 10,
year = 2019,
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2515-1762},
url =
{https://easychair.org/publications/volume/LuxLogAI_2018},
}
@article{J46,
Author = {Benzm{\"u}ller, Christoph and Parent, Xavier and
Ricca, Francesco},
Keywords = {own, Artificial Intelligence, Rules and Reasoning},
Journal = {AI Magazine},
Title = {Report on the Second International Joint Conference
on Rules and Reasoning},
Year = 2019,
Volume = 40,
Number = 2,
Pages = {73-74},
Doi = {10.1609/aimag.v40i2.2888},
url =
{http://page.mi.fu-berlin.de/cbenzmueller/papers/J49.pdf},
}
@inproceedings{R72,
Author = {Benzm{\"u}ller, Christoph},
Title = {Computational Metaphysics: New Insights on
{G{\"o}del's} Ontological Argument and Modal
Collapse},
Editor = {Srecko Kovac and Kordula Swietorzecka},
Booktitle = {Formal Methods and Science in Philosophy III,
Informal Proceedings},
Year = 2019,
Pages = {3--4},
Adress = {Dubrovnik, Croatia},
Url =
{http://christoph-benzmueller.de/papers/2019-FMSPh-Proceedings.pdf},
}
@article{J48,
Author = {Benzm{\"u}ller, Christoph and Parent, Xavier and van
der Torre, Leendert},
Keywords = {own, Trustworthy and responsible AI, Knowledge
representation and reasoning, Automated theorem
proving, Model finding, Normative reasoning,
Normative systems, Ethical issues, Semantical
embedding, Higher-order logic},
Journal = {Artificial Intelligence},
Publisher = {Elsevier},
Title = {Designing Normative Theories for Ethical and Legal
Reasoning: {LogiKEy} Framework, Methodology, and
Tool Support},
Year = 2020,
Volume = 287,
Pages = 103348,
issn = {0004-3702},
Doi = {10.1016/j.artint.2020.103348},
OPTUrl = {https://doi.org/10.1016/j.artint.2020.103348},
url = {https://www.researchgate.net/publication/342146653},
url_arxiv = {https://arxiv.org/abs/1903.10187},
}
@misc{J48arxiv,
doi = {10.48550/ARXIV.1903.10187},
OPTurl = {https://arxiv.org/abs/1903.10187},
author = {Benzm{\"u}ller, Christoph and Parent, Xavier and van
der Torre, Leendert},
keywords = {Artificial Intelligence (cs.AI), FOS: Computer and
information sciences, FOS: Computer and information
sciences, I.2.3; I.2.4; I.2.0; F.4, 03B60, 03B15,
68T27, 68T30, 68T15},
title = {Designing Normative Theories for Ethical and Legal
Reasoning: {LogiKEy} Framework, Methodology, and Tool
Support},
publisher = {arXiv},
note = {Preprint},
year = 2019,
copyright = {arXiv.org perpetual, non-exclusive license}
}
@InProceedings{C74,
Author = {David Fuenmayor and Christoph Benzm{\"u}ller},
Keywords = {own, Formal Ethics, Machine Ethics, Knowledge
Representation and Reasoning, Higher Order Logic,
Universal Reasoning},
Title = {Automated Reasoning with Complex Ethical Theories--A
Case Study Towards Responsible AI},
Booktitle = {16th International Congress on Logic, Methodology
and Philosophy of Science and Technology (CLMPST
2019) --- Bridging across Academic Cultures, Book of
Abstracts},
pages = {183-184},
year = 2019,
Address = {Prague, Czechia, August 5-10, 2019},
Url =
{http://clmpst2019.flu.cas.cz/wp-content/uploads/2019/08/BoA_CLMPST2019_web.pdf}
}
@article{J45,
Keywords = {own, Higher Order Logic, Higher Order Modal Logic,
Universal Reasoning, Computational Metaphysics,
Philosophy},
Author = {Kirchner, Daniel and Benzm{\"u}ller, Christoph and
Zalta, Edward N.},
Journal = {Open Philosophy},
Title = {Computer Science and Metaphysics: A
Cross-Fertilization},
Editor = {Patrick Grim},
Year = 2019,
Volume = 2,
number = 1,
Pages = {230–251},
Doi = {10.1515/opphil-2019-0015},
url = {http://doi.org/10.13140/RG.2.2.25229.18403},
OPTurl = {https://arxiv.org/abs/1905.00787},
}
@article{J44,
Author = {Christoph Benzm{\"u}ller and Ali Farjami and Paul
Meder and Xavier Parent},
Journal = {Journal of Applied Logics -- IfCoLoG Journal of
Logics and their Applications (Special Issue:
Reasoning for Legal AI)},
Editor = {Robaldo, Livio and van der Torre, Leon},
Title = {{I/O} Logic in {HOL}},
Pages = {715--732},
Volume = 6,
Number = 5,
url = {https://www.researchgate.net/publication/332786587},
Url =
{https://www.collegepublications.co.uk/ifcolog/?00034},
Year = 2019,
}
@article{J43,
Author = {Christoph Benzm{\"u}ller and Ali Farjami and Xavier
Parent},
Journal = {Journal of Applied Logics -- IfCoLoG Journal of
Logics and their Applications (Special Issue:
Reasoning for Legal AI)},
Editor = {Robaldo, Livio and van der Torre, Leon},
Title = {{{\AA}qvist's} Dyadic Deontic Logic {E} in {HOL}},
Volume = 6,
Number = 5,
Pages = {733--755},
url = {https://www.researchgate.net/publication/332786724},
Url =
{https://www.collegepublications.co.uk/ifcolog/?00034},
Year = 2019,
}
@Proceedings{E20,
editor = {Christoph Benzm{\"u}ller and Heiner Stuckenschmidt},
title = {{KI} 2019: Advances in Artificial Intelligence --
42nd German Conference on AI, Kassel, Germany,
September 23-26, 2019, Proceedings},
series = {Lecture Notes in Artificial Intelligence},
volume = 11793,
publisher = {Springer},
year = 2019,
pages = {1--355},
OPTurl = {https://doi.org/10.1007/978-3-030-30179-8},
doi = {10.1007/978-3-030-30179-8},
isbn = {978-3-030-30178-1},
}
@article{J42,
Author = {Christoph Benzm{\"u}ller},
Journal = {Data in Brief (data publication)},
Keywords = {own, Universal Logical Reasoning},
Title = {Universal (Meta-)Logical Reasoning: The Wise Men
Puzzle ({Isabelle/HOL Dataset})},
Year = 2019,
Volume = 24,
Pages = {1--5},
Number = 103823,
Note = {Open Access},
Doi = {10.1016/j.dib.2019.103823},
}
@InCollection{J41,
author = {Benzm{\"u}ller, Christoph and Andrews, Peter},
title = {Church's Type Theory},
booktitle = {The Stanford Encyclopedia of Philosophy},
editor = {Edward N. Zalta},
year = 2019,
edition = {Summer 2019},
pages = {1--62 (in pdf version)},
publisher = {Metaphysics Research Lab, Stanford University},
url =
{https://plato.stanford.edu/entries/type-theory-church/},
}
@misc{R73arxiv,
Keywords = {own, Formal Proof, Mathematical Proof
Assistant, Higher Order Logic, Universal Reasoning},
Author = {Christoph Benzm{\"u}ller},
Publisher = {arXiv},
Title = {What is a proof? What should it be?},
url = {https://www.researchgate.net/publication/330310239},
OPTurl = {http://arxiv.org/abs/1904.06332},
Doi = {10.13140/RG.2.2.13405.87521/1},
year = 2019,
}
@InCollection{B17,
author = {David Fuenmayor and Christoph Benzm{\"u}ller},
Keywords = {own, Computational Hermeneutics, Higher Order Logic,
Universal Reasoning, Rational Argumentation,
Human-Machine Interaction},
title = {Computational Hermeneutics: An Integrated Approach
for the Logical Analysis of Natural-Language
Arguments},
booktitle = {Dynamics, Uncertainty and Reasoning -- The Second
Chinese Conference on Logic and Argumentation},
publisher = {Springer Singapore},
pages = {187--207},
doi = {10.1007/978-981-13-7791-4_9},
year = 2019,
editor = {Liao, Beishui and Agotnes, Thomas and Wang, Yi N.},
series = {Logic in Asia: Studia Logica Library},
url = {http://doi.org/10.13140/RG.2.2.11784.26881},
}
@article{J39,
Author = {David Fuenmayor and Christoph Benzm{\"u}ller},
Journal = {Archive of Formal Proofs (data publication)},
Keywords = {own, Machine Ethics, Ethics, Artificial General
Intelligence, Dyadic Deontic Logic, Higher Order
Logic, Computational Metaphysics, Semantical
Embedding},
Title = {Formalisation and Evaluation of {Alan Gewirth's}
Proof for the {Principle of Generic Consistency} in
{Isabelle/HOL}},
Url =
{https://www.isa-afp.org/entries/GewirthPGCProof.html},
Year = 2018,
Pages = {1-15},
}
@article{J40,
author = {Christoph Benzm{\"u}ller},
title = {Universal (Meta-)Logical Reasoning: Recent
Successes},
journal = {Science of Computer Programming},
year = 2019,
volume = 172,
pages = {48-62},
url = {http://doi.org/10.13140/RG.2.2.11039.61609/2},
doi = {10.1016/j.scico.2018.10.008},
}
@article{J47,
author = {Christoph Benzm{\"u}ller and Scott, Dana S.},
Keywords = {own, Automated Reasoning, Free Logic, Higher Order
Logic, Category Theory},
title = {Automating Free Logic in {HOL}, with an Experimental
Application in Category Theory},
volume = 64,
number = 1,
pages = {53--72},
year = 2020,
OPTurl = {http://doi.org/10.13140/RG.2.2.11432.83202},
journal = {Journal of Automated Reasoning},
publisher = {Springer Netherlands},
doi = {10.1007/s10817-018-09507-7},
url = {http://doi.org/10.13140/RG.2.2.11432.83202},
}
@misc{W63,
Author = {Farjami, Ali and Meder, Paul and Parent, Xavier and
Benzm{\"u}ller, Christoph},
Booktitle = {MIREL 2018},
Keywords = {own, Input/Output Logic, Higher Order Logic,
Semantic Embedding, Automated Reasoning, General
Data Protection Regulation},
Note = {MIREL 2018 workshop on MIning and REasoning with
Legal texts.},
url = {http://orbilu.uni.lu/handle/10993/37013},
Title = {{I/O} Logic in {HOL}},
Year = 2018,
Pages = {1--18},
}
@misc{W62,
Author = {Benzm{\"u}ller, Christoph and Farjami, Ali and
Parent, Xavier},
Booktitle = {MIREL 2018},
Keywords = {own, Dyadic Deontic Logic E, Preference Models,
Higher Order Logic, Semantic Embedding, Automated
Reasoning},
Note = {MIREL 2018 workshop on MIning and REasoning with
Legal texts.},
url = {http://orbilu.uni.lu/handle/10993/37014},
Title = {Aqvist's Dyadic Deontic Logic {E} in {HOL}},
Year = 2018,
}
@inproceedings{C73,
Author = {Christoph Benzm{\"u}ller and Fuenmayor, David},
Booktitle = {Mathematics and Reality, Proceedings of the 11th All
India Students' Conference on Science \& Spiritual
Quest (AISSQ), 6-7 October, 2018, IIT Bhubaneswar,
Bhubaneswar, India},
Editor = {Gosh, Sudipto and Uppalari, Ramgopal and Rao,
K. Vasudeva and Agarwal, Varun and Sharma, Sushant},
Keywords = {own, Ontological Argument, Computational
Metaphysics, Higher Order Logic, Semantic Embedding,
Modal Logics, Automated Reasoning, Ontology
Reasoning},
Publisher = {The Bhaktivedanta Institute, Kolkata,
\url{www.binstitute.org}},
Title = {Can Computers Help to Sharpen our Understanding of
Ontological Arguments?},
url = {http://doi.org/10.13140/RG.2.2.31921.84323},
pages = {195-226},
isbn = {81-89635-31-X},
Year = 2018,
}
@techreport{R70,
Author = {Benzm{\"u}ller, Christoph and Farjami, Ali and
Parent, Xavier},
Keywords = {own, Higher Order Logic, Deontic Logic, Automated
Reasoning, Universal Reasoning},
Note = {Poster presented at the 6th World Congress and
School on Universal Logic, 16-26 June, Vichy,
France},
Title = {A Faithful Semantic Embedding of the Dyadic Deontic
Logic {E} in {HOL}},
Institution = {University of Luxembourg},
url = {http://christoph-benzmueller.de/papers/R59.pdf},
Year = 2018,
}
@techreport{R69,
Author = {Benzm{\"u}ller, Christoph and Farjami, Ali and
Parent, Xavier},
Keywords = {own, Higher Order Logic, Deontic Logic, Automated
Reasoning, Universal Reasoning},
Note = {10th edition of PhDs in Logic, Institute of
Philosophy of the Czech Academy of Sciences, Prague
on May 1–4 2018},
Title = {Implementation of Dyadic Deontic Logic {E} in
{Isabelle/HOL}},
Institution = {University of Luxembourg and Freie Universität Berlin},
url = {http://christoph-benzmueller.de/papers/R58.pdf},
Year = 2018,
}
@techreport{R68,
Author = {David Fuenmayor and Benzm{\"u}ller (PhD Advisor),
Christoph},
Keywords = {own, Computational Hermeneutics, Higher Order Logic,
Universal Reasoning, Rational Argumentation,
Human-Machine Interaction},
Title = {Computational Hermeneutics: Using Automated
Reasoning for the Logical Analysis of
Natural-Language Arguments (Abstract)},
Institution = {University of Luxembourg and Freie Universität Berlin},
Note = {Deduktionstreffen, LuxLogAI 2018},
url = {http://christoph-benzmueller.de/papers/R69.pdf},
year = 2018,
}
@techreport{R67,
Author = {David Fuenmayor and Benzm{\"u}ller (PhD Advisor),
Christoph},
Keywords = {own, Computational Hermeneutics, Higher Order Logic,
Universal Reasoning, Rational Argumentation,
Human-Machine Interaction},
Title = {Computational Hermeneutics: Using Automated
Reasoning for the Logical Analysis of
Natural-Language Arguments (Abstract)},
Institution = {University of Luxembourg and Freie Universität Berlin},
Note = {Doctoral Consortium, RuleML+RR 2018},
url = {http://christoph-benzmueller.de/papers/R68.pdf},
year = 2018,
}
@techreport{R66,
Author = {David Fuenmayor and Christoph Benzm{\"u}ller},
Keywords = {own, Computational Hermeneutics, Higher Order Logic,
Universal Reasoning, Rational Argumentation,
Human-Machine Interaction},
Title = {Computational Hermeneutics: Using Computers for the
Logical Analysis of Natural-Language Arguments
(Abstract)},
Institution = {University of Luxembourg},
Note = {MBR18 SPAIN --- Model-Based Reasoning in Science and
Technology: Inferential Models for Logic, Language,
Cognition and Computation},
url = {http://christoph-benzmueller.de/papers/R67.pdf},
year = 2018,
}
@Proceedings{E19,
title = {Rules and Reasoning, Second International Joint
Conference, RuleML+RR 2018, Luxembourg, Luxembourg,
September 18-21, 2018, Proceedings},
Editor = {Christoph Benzm{\"u}ller and Francesco Ricca and
Xavier Parent and Dumitru Roman},
Publisher = {Springer},
Series = {Lecture Notes in Computer Science},
Volume = 11092,
Year = 2018,
doi = {10.1007/978-3-319-99906-7},
isbn = {978-3-319-99905-0},
issn = {0302-9743},
}
@article{J38,
Author = {Christoph Benzm{\"u}ller and Scott, Dana S.},
Keywords = {own, Automated Reasoning, Free Logic, Higher Order
Logic, Category Theory},
Journal = {Archive of Formal Proofs (data publication)},
Keywords = {own, Category Theory, Free Logic, Higher Order
Logic, Semantical Embedding},
Title = {Axiom Systems for Category Theory in Free Logic},
Url =
{https://www.isa-afp.org/entries/AxiomaticCategoryTheory.html},
Year = 2018,
Pages = {1--12},
}
@incollection{B19,
Author = {David Fuenmayor and Christoph Benzm{\"u}ller},
Booktitle = {Beyond Faith and Rationality: Essays on Logic,
Religion and Philosophy},
Editor = {Silvestre, Ricardo and G\"{o}cke, Benedikt and
B\'{e}ziau, Jean-Yves and Bilimoria, Purushottama},
Keywords = {own, Automated Reasoning, Interactive Proof,
Ontology Reasoning, Higher Order Logic,
Computational Metaphysics},
Publisher = {Springer Nature Switzerland AG},
Series = {Sophia Studies in Cross-cultural Philosophy of
Traditions and Cultures},
Volume = 34,
Chapter = 12,
Title = {A Case Study On Computational Hermeneutics:
{E.~J.~Lowe's} Modal Ontological Argument},
Year = 2020,
Doi = {10.1007/978-3-030-43535-6_12},
}
@article{J37,
Author = {David Fuenmayor and Christoph Benzm{\"u}ller},
Journal = {Journal of Applied Logic - IfCoLoG Journal of Logics
and their Applications (special issue on Formal
Approaches to the Ontological Argument)},
Volume = 5,
Number = 7,
Pages = {1567-1603},
Editors = {Silvestre, Ricardo and B\'{e}ziau, Jean-Yves},
Keywords = {own, Automated Reasoning, Interactive Proof,
Ontology Reasoning, Higher Order Logic,
Computational Metaphysics},
Title = {A Case Study On Computational Hermeneutics:
{E.~J.~Lowe's} Modal Ontological Argument},
Year = 2018,
Note = {Published also as chapter in the book 'Beyond
Faith and Rationality: Essays on Logic, Religion and
Philosophy' printed in the Springer book series
'Sophia Studies in Cross-cultural Philosophy of
Traditions and Cultures'},
url = {https://www.researchgate.net/publication/333804824},
}
@inproceedings{W61,
Author = {Alexander Steen and Christoph Benzm{\"u}ller},
Booktitle = {ARQNL 2018. Automated Reasoning in Quantified
Non-Classical Logics},
Editor = {Christoph Benzm{\"u}ller and Jens Otten},
Keywords = {own, Higher Order Logic, Leo Prover},
Publisher = {CEUR Workshop Proceedings, http://ceur-ws.org},
Url = {http://ceur-ws.org/Vol-2095/paper5.pdf},
Volume = 2095,
Title = {System Demonstration: The Higher-Order Prover
{Leo-III}},
Pages = {79-85},
Year = 2018,
}
@proceedings{E18,
url_website = {http://www.iltp.de/ARQNL-2016/},
Editor = {Christoph Benzm{\"u}ller and Jens Otten},
Issn = {1613-0073},
Publisher = {CEUR Workshop Proceedings},
Title = {ARQNL 2018. Automated Reasoning in Quantified
Non-Classical Logics},
Url = {http://ceur-ws.org/Vol-2095/},
Volume = 2095,
Year = 2018,
}
@techreport{R71,
Author = {David Fuenmayor and Christoph Benzm{\"u}ller},
Keywords = {own, Computational Hermeneutics, Higher Order Logic,
Universal Reasoning, Rational Argumentation,
Human-Machine Interaction},
Title = {Computational Hermeneutics: Using Computers for the
Logical Analysis of Natural-Language Arguments},
Note = {2nd Chinese Conference on Logic and Argumentation,
16-17 June, Hangzhou, China, 2018, Informal
Proceedings},
Institution = {University of Luxembourg and Freie Universität Berlin},
url = {http://christoph-benzmueller.de/papers/R71.pdf},
year = 2018,
}
@inproceedings{C72,
Author = {Benzm{\"u}ller, Christoph},
Booktitle = {Deontic Logic and Normative Systems --- 14th
International Conference, DEON 2018, Utrecht, The
Netherlands, 3-6 July, 2018},
Editor = {Jan Broersen and Cleo Condoravdi and Shyam Nair and
Gabriella Pigozzi},
Keywords = {own, Higher Order Logic, Deontic Logic, Automated
Reasoning, Universal Reasoning},
Publisher = {College Publications},
pages = 7,
Title = {A Flexible Infrastructure for Normative Reasoning
(invited keynote abstract)},
url = {http://doi.org/10.13140/RG.2.2.27972.48007},
Volume = 9706,
Year = 2018,
isbn = {978-1-84890-278-7},
}
@inproceedings{C71,
Author = {Benzm{\"u}ller, Christoph and Farjami, Ali and
Parent, Xavier},
Booktitle = {Deontic Logic and Normative Systems --- 14th
International Conference, DEON 2018, Utrecht, The
Netherlands, 3-6 July, 2018},
Editor = {Jan Broersen and Cleo Condoravdi and Shyam Nair and
Gabriella Pigozzi},
Keywords = {own, Higher Order Logic, Deontic Logic, Automated
Reasoning, Universal Reasoning},
Publisher = {College Publications},
pages = {33-50},
Title = {A Dyadic Deontic Logic in {HOL}},
url = {https://tinyurl.com/y9wp4p6s},
Volume = 9706,
Year = 2018,
isbn = {978-1-84890-278-7},
addendum = {John-Jules Meyer Best Paper Award},
}
@misc{R65,
doi = {10.48550/ARXIV.1804.02929},
OPTurl = {https://arxiv.org/abs/1804.02929},
author = {Benzm{\"u}ller, Christoph and Parent, Xavier},
title = {First Experiments with a Flexible Infrastructure for
Normative Reasoning},
publisher = {arXiv},
note = {Preprint},
year = 2018,
copyright = {arXiv.org perpetual, non-exclusive license}
}
@inproceedings{C70,
Author = {Alexander Steen and Christoph Benzm{\"u}ller},
Booktitle = {Automated Reasoning. IJCAR 2018},
Editor = {Didier Galmiche and Stephan Schulz and Roberto
Sebastiani},
Keywords = {own, Higher Order Logic, Automated Reasoning, LEO
Prover},
Publisher = {Springer},
Series = {LNCS},
Title = {The Higher-Order Prover {Leo-III}},
url = {https://tinyurl.com/y7wg5w5w},
volume = 10900,
pages = {108-116},
doi = {10.1007/978-3-319-94205-6_8},
isbn = {978-3-319-94204-9},
Year = 2018,
}
@inproceedings{C69,
Author = {Benzm{\"u}ller, Christoph and Parent, Xavier and van
der Torre, Leendert},
Keywords = {own, Automated Reasoning, Intensional Higher-Order
Modal Logic, Higher Order Logic},
Title = {A Deontic Logic Reasoning Infrastructure},
Booktitle = {14th Conference on Computability in Europe, CiE
2018, Kiel, Germany, July 30-August, 2018,
Proceedings},
Publisher = {Springer},
editor = {Manea, Florin and Miller, Russell G. and Nowotka,
Dirk},
series = {LNCS},
Year = 2018,
volume = 10936,
Pages = {60-69},
isbn = {978-3-319-67189-5},
Doi = {10.1007/978-3-319-94418-0_6},
url = {https://tinyurl.com/y7tgoft9},
}
@misc{R64,
doi = {10.48550/ARXIV.1803.09681},
OPTurl = {https://arxiv.org/abs/1803.09681},
author = {Benzm{\"u}ller, Christoph and Parent, Xavier},
title = {{I/O} Logic in {HOL} --- First Steps},
publisher = {arXiv},
note = {Preprint},
year = 2018,
copyright = {arXiv.org perpetual, non-exclusive license}
}
@techreport{R63,
Author = {Benzm{\"u}ller, Christoph},
Keywords = {own, Computational Metaphysics, Universal Reasoning,
Higher Order Logic},
Title = {Studies in Computational Metaphysics --- Results of
an Interdisciplinary Research Project},
Institution = {University of Luxembourg and Freie Universität Berlin},
url = {http://christoph-benzmueller.de/papers/R64.pdf},
Year = 2018
}
@techreport{R62,
Author = {Benzm{\"u}ller, Christoph and Farjami, Ali and
Parent, Xavier},
Keywords = {own, Higher Order Logic, Deontic Logic, Automated
Reasoning, Universal Reasoning},
Title = {Faithful Semantical Embedding of a Dyadic Deontic
Logic in {HOL}},
Institution = {CoRR},
Number = {arXiv:1802.08454},
Url = {https://arxiv.org/abs/1802.08454},
Year = 2018
}
@inproceedings{W60,
Author = {David Fuenmayor and Christoph Benzm{\"u}ller},
Keywords = {own, Computational Hermeneutics, Higher Order Logic,
Universal Reasoning, Rational Argumentation,
Human-Machine Interaction},
Title = {Computational Hermeneutics: Using Computers to
Interpret Philosophical Arguments (Abstract)},
Booktitle = {Logical Correctness, Workshop at UNILOG'2018,
UNILOG'2018 Book of Abstracts},
year = 2018,
url = {http://christoph-benzmueller.de/papers/W60.pdf},
}
@misc{R61,
doi = {10.48550/ARXIV.1802.02732},
OPTurl = {https://arxiv.org/abs/1802.02732},
author = {Steen, Alexander and Benzm{\"u}ller, Christoph},
title = {The Higher-Order Prover {Leo-III} (Extended Version)},
publisher = {arXiv},
note = {Preprint},
year = 2018,
copyright = {arXiv.org perpetual, non-exclusive license}
}
@inproceedings{C68,
Author = {Daniel Kirchner and Christoph Benzm{\"u}ller and
Zalta, Edward N.},
Keywords = {own, Higher Order Logic, Higher Order Modal Logic,
Universal Reasoning, Computational Metaphysics},
Title = {Mechanizing Principia Logico-Metaphysica in
Functional Type Theory (Extended Abstract)},
editor = {Hales, Thomas C. and Kaliszyk, Cezary and Schulz,
Stephan and Urban, Josef},
Booktitle = {3rd Conference on Artificial Intelligence and
Theorem Proving (AITP 2018), Book of Abstracts},
year = 2018,
pages = {42--44},
Url =
{http://aitp-conference.org/2018/aitp18-proceedings.pdf},
}
@inproceedings{C67,
Author = {Christoph Benzm{\"u}ller and Scott, Dana S.},
Keywords = {own, Automated Reasoning, Free Logic, Higher Order
Logic, Category Theory},
Title = {Some Reflections on a Computer-aided Theory
Exploration Study in Category Theory (Extended
Abstract)},
editor = {Hales, Thomas C. and Kaliszyk, Cezary and Schulz,
Stephan and Urban, Josef},
Booktitle = {3rd Conference on Artificial Intelligence and
Theorem Proving (AITP 2018), Book of Abstracts},
year = 2018,
pages = {7--8},
Url =
{http://aitp-conference.org/2018/aitp18-proceedings.pdf},
}
@article{J36,
Author = {David Fuenmayor and Christoph Benzm{\"u}ller},
Journal = {Archive of Formal Proofs (data publication)},
Keywords = {own, Automated Reasoning, Interactive Proof,
Ontology Reasoning, Higher Order Logic,
Computational Metaphysics},
Title = {{Computer-assisted Reconstruction and Assessment of
E. J. Lowe's Modal Ontological Argument}},
Url =
{https://www.isa-afp.org/entries/Lowe_Ontological_Argument.html},
Year = 2017,
Pages = {1--19},
}
@techreport{R60a,
Author = {Christoph Benzm{\"u}ller and Hanna Lachnitt and Maximilian Claus},
Keywords = {own},
Title = {Systematic Verification of the Intuitionistic Modal Logic Cube in Isabelle/HOL},
Institution = {Freie Universität Berlin},
Doi = {10.13140/RG.2.2.26232.56325},
Year = 2017
}
@techreport{R60,
Author = {David Fuenmayor and Christoph Benzm{\"u}ller},
Keywords = {own, Computational Hermeneutics, Higher Order Logic,
Universal Reasoning, Rational Argumentation,
Human-Machine Interaction},
Title = {A Case Study on Computational Hermeneutics:
E.~J.~Lowe's Modal Ontological Argument},
Institution = {PhilPapers},
Url = {https://philpapers.org/rec/FUEACS},
Year = 2017
}
@inproceedings{C66,
Author = {Christoph Benzm{\"u}ller},
Keywords = {own, Automated Reasoning, Universal Reasoning,
Semantic Embedding, Higher Order Logic},
Title = {Recent Successes with a Meta-Logical Approach to
Universal Logical Reasoning (Invited Extended
Abstract)},
editor = {Simone Andr{\'{e}} da Costa Cavalheiro and
Jos{\'{e}} Luiz Fiadeiro},
Booktitle = {Formal Methods: Foundations and Applications - 20th
Brazilian Symposium, {SBMF} 2017, Recife, Brazil,
November 29 - December 1, 2017, Proceedings},
pages = {7--11},
year = 2017,
series = {Lecture Notes in Computer Science},
volume = 10623,
publisher = {Springer},
url = {http://christoph-benzmueller.de/papers/C66.pdf},
}
@inproceedings{W59,
Address = {Belgrade, Serbia},
author = {Benzm{\"u}ller, Christoph and Farjami, Ali and
Parent, Xavier and van der Torre, Leendert},
title = {Implementation of Carmo and Jones Dyadic Deontic
Logic in {Isabelle/HOL}},
booktitle = {Workshop on Computational Aspects of Arguments and
LogiC (CAALC 2017)},
year = 2017,
url = {http://christoph-benzmueller.de/papers/W59.pdf},
Keywords = {own, Dyadic Logic, Higher-Order Logic},
}
@Article{J35,
Keywords = {own, Automated Reasoning, Intensional Higher-Order
Modal Logic, Higher Order Logic},
author = {Christoph Benzm{\"u}ller and Woltzenlogel Paleo,
Bruno},
title = {Experiments in {Computational Metaphysics}:
{G\"odel's} Proof of {God's} Existence},
journal = {Savijnanam: scientific exploration for a spiritual
paradigm. Journal of the Bhaktivedanta Institute},
year = 2017,
volume = 9,
pages = {43-57},
url =
{https://sites.google.com/binstitute.org/journal/article-3-page-43},
issn = {0972-6586},
url = {https://www.researchgate.net/publication/334519782},
}
@inproceedings{C65,
Author = {David Fuenmayor and Christoph Benzm{\"u}ller},
Keywords = {own, Automated Reasoning, Intensional Higher-Order
Modal Logic, Higher Order Logic},
Title = {Automating Emendations of the Ontological Argument
in Intensional Higher-Order Modal Logic},
Booktitle = {KI 2017: Advances in Artificial Intelligence, 40th
Annual German Conference on AI, Dortmund, Germany,
September 25-29, 2017, Proceedings},
Publisher = {Springer},
Series = {LNAI},
Year = 2017,
Volume = 10505,
Pages = {114-127},
isbn = {978-3-319-67189-5},
OPTurl = {https://doi.org/10.1007/978-3-319-67190-1_9},
Doi = {10.1007/978-3-319-67190-1_9},
url = {http://christoph-benzmueller.de/papers/C65.pdf},
}
@article{J34,
Author = {David Fuenmayor and Christoph Benzm{\"u}ller},
Journal = {Archive of Formal Proofs (data publication)},
Keywords = {own, Automated Reasoning, Interactive Proof,
Ontology Reasoning, Higher Order Logic,
Computational Metaphysics},
Title = {Types, Tableaus and {G{\"o}del's} God in
{Isabelle/HOL}},
Url =
{http://afp.sourceforge.net/entries/Types_Tableaus_and_Goedels_God.shtml},
Year = 2017,
Pages = {1--34},
}
@misc{R59,
doi = {10.48550/ARXIV.1703.09620},
OPTurl = {https://arxiv.org/abs/1703.09620},
author = {Benzm{\"u}ller, Christoph},
title = {Universal Reasoning, Rational Argumentation and
Human-Machine Interaction},
publisher = {arXiv},
note = {Preprint},
year = 2017,
copyright = {arXiv.org perpetual, non-exclusive license}
}
@inproceedings{W58,
Address = {Maun, Botswana},
Author = {Alexander Steen and Max Wisniewski and Hans-J{\"o}rg
Schurr and Christoph Benzm{\"u}ller},
Keywords = {own, LEO Prover, Higher Order Logic, Polymorphism,
Automated Reasoning},
title = {Capability Discovery for Automated Reasoning
Systems},
Booktitle = {IWIL@LPAR 2017 Workshop and {LPAR-21} Short
Presentations, Maun, Botswana, May 7-12, 2017},
Editor = {Thomas Eiter and David Sands and Geoff Sutcliffe and
Andrei Voronkov},
series = {Kalpa Publications in Computing},
volume = 1,
publisher = {EasyChair},
year = 2017,
OPTurl = {https://easychair.org/publications/paper/SfX},
doi = {10.29007/fsv3},
}
@inproceedings{W57,
Address = {Maun, Botswana},
Author = {Alexander Steen and Max Wisniewski and Christoph
Benzm{\"u}ller},
Keywords = {own, LEO Prover, Higher Order Logic, Polymorphism,
Automated Reasoning},
title = {Going Polymorphic - {TH1} Reasoning for {Leo-III}},
Booktitle = {IWIL@LPAR 2017 Workshop and {LPAR-21} Short
Presentations, Maun, Botswana, May 7-12, 2017},
Editor = {Thomas Eiter and David Sands and Geoff Sutcliffe and
Andrei Voronkov},
series = {Kalpa Publications in Computing},
pages = {100-112},
volume = 1,
publisher = {EasyChair},
year = 2017,
OPTurl = {https://easychair.org/publications/paper/CNN},
Doi = {10.29007/jgkw},
}
@inproceedings{C64,
Address = {Maun, Botswana},
Author = {Christoph Benzm{\"u}ller and Alexander Steen and Max
Wisniewski},
Keywords = {own, LEO Prover, Higher Order Logic, Polymorphism,
Automated Reasoning},
title = {{Leo-III} Version 1.1 (System description)},
Booktitle = {IWIL@LPAR 2017 Workshop and {LPAR-21} Short
Presentations, Maun, Botswana, May 7-12, 2017},
Editor = {Thomas Eiter and David Sands and Geoff Sutcliffe and
Andrei Voronkov},
series = {Kalpa Publications in Computing},
pages = {11-61},
volume = 1,
publisher = {EasyChair},
year = 2017,
doi = {10.29007/grmx},
OPTurl = {https://easychair.org/publications/paper/sl},
}
@inproceedings{C63,
Author = {David Fuenmayor and Christoph Benzm{\"u}ller and
Alexander Steen and Max Wisniewski},
Booktitle = {Handbook of the 2nd World Congress on Logic and
Religion, Warsaw, Poland},
Editor = {Stanislaw Krajewski and Piotr Balcerowicz},
Keywords = {own, Automated Reasoning, Interactive Proof,
Ontology Reasoning, LEO Prover, Higher Order Logic,
Computational Metaphysics},
Pages = 3,
Title = {The Virtues of Automated Theorem Proving in
Metaphysics --- A Case Study: {E. J. Lowe's} Modal
Ontological Argument},
url = {http://christoph-benzmueller.de/papers/C63.pdf},
Year = 2017,
}
@inproceedings{C62,
Address = {Maun, Botswana},
Author = {Tobias Glei{ß}ner and Alexander Steen and
Christoph Benzm{\"u}ller},
Booktitle = {LPAR-21. 21st International Conference on Logic for
Programming, Artificial Intelligence and Reasoning},
Editor = {Thomas Eiter and David Sands},
Keywords = {own, Modal Logic, Higher Order Modal Logic, Higher
Order Logic, Automated Reasoning},
Publisher = {EasyChair},
issn = {2398-7340},
Series = {EPiC Series in Computing},
Volume = 46,
Pages = {14-30},
Doi = {10.29007/jsb9},
Title = {Theorem Provers for Every Normal Modal Logic},
OPTurl = {https://easychair.org/publications/paper/6bjv},
doi = {10.29007/jsb9},
Year = 2017,
}
@incollection{B16,
Author = {Bentert, Matthias and Benzm{\"u}ller, Christoph and
Streit, David and Woltzenlogel Paleo, Bruno},
Booktitle = {Death and Anti-Death, Volume 14: Four Decades after
Michael Polanyi, Three Centuries after G.W. Leibniz},
Editor = {Tandy, Charles},
Keywords = {own, Automated Reasoning, Interactive Proof,
Semantic Embedding, Higher Order Logic, Higher Order
Modal Logic, Computational Metaphysics},
Publisher = {Ria University Press},
Title = {Analysis of an Ontological Proof Proposed by
{Leibniz}},
Isbn = {978-1934297254},
Url = {https://philpapers.org/rec/TANDAA-10},
Year = 2016,
url = {https://www.researchgate.net/publication/311456135},
}
@techreport{J30,
Author = {Christoph Benzm{\"u}ller and Alexander Steen and Max
Wisniewski},
Title = {News --- 25th International Conference on Automated
Deduction (CADE-25)},
doi = {10.1007/s13218-015-0402-z},
Year = 2015,
note = {K\"unstliche Intelligenz 29(4):451-452; non-reviewed
conference report},
}
@inproceedings{C61,
Address = {Berlin, Germany},
Author = {Alexander Steen and Max Wisniewski and Christoph
Benzm{\"u}ller},
Title = {Tutorial on Reasoning in Expressive Non-Classical
Logics with {Isabelle/HOL}},
Booktitle = {GCAI 2016, 2nd Global Conference on Artificial
Intelligence},
Editor = {Christoph Benzm{\"u}ller and Raul Rojas and Geoff
Sutcliffe},
Keywords = {own, Automated Reasoning, Interactive Proof,
Semantic Embedding, Higher Order Logic, Mulimodal
Logic},
Publisher = {EasyChair},
Series = {EPiC Series in Computing},
issn = {2398-7340},
Doi = {10.29007/4dsr},
OPTurl = {https://easychair.org/publications/paper/dw51},
Volume = 41,
Year = 2016,
Pages = {1-10}
}
@misc{R58,
doi = {10.48550/ARXIV.1609.01493},
OPTurl = {https://arxiv.org/abs/1609.01493},
author = {Benzm{\"u}ller, Christoph and Scott, Dana S.},
title = {Axiomatizing Category Theory in Free Logic},
publisher = {arXiv},
note = {Preprint},
year = 2016,
copyright = {arXiv.org perpetual, non-exclusive license}
}
@proceedings{E17,
Title = {GCAI 2017. 3rd Global Conference on Artificial
Intelligence},
Editor = {Christoph Benzm{\"u}ller and Christine Lisetti and
Martin Theobald},
Publisher = {EasyChair},
Series = {EPiC Series in Computing},
Url =
{http://www.easychair.org/publications/volume/GCAI_2017},
Volume = 50,
Year = 2017,
issn = {2398-7340},
}
@proceedings{E16,
Title = {GCAI 2016. 2nd Global Conference on Artificial
Intelligence},
Editor = {Christoph Benzm{\"u}ller and Geoff Sutcliffe and
Raul Rojas},
Publisher = {EasyChair},
Series = {EPiC Series in Computing},
Url =
{http://www.easychair.org/publications/volume/GCAI_2016},
Volume = 41,
issn = {2398-7340},
Year = 2016
}
@proceedings{E15,
OPTComment = {event-website},
Editor = {Christoph Benzm{\"u}ller and Jens Otten},
Issn = {1613-0073},
Pages = {1-86},
Publisher = {CEUR Workshop Proceedings, http://ceur-ws.org},
Title = {ARQNL 2016. Automated Reasoning in Quantified
Non-Classical Logics},
Url = {http://ceur-ws.org/Vol-1770/},
Volume = 1770,
Year = 2016
}
@inproceedings{C60,
Address = {Berlin, Germany},
Author = {Christoph Benzm{\"u}ller and Woltzenlogel Paleo,
Bruno},
Booktitle = {KI 2016: Advances in Artificial Intelligence,
Proceedings},
Editor = {Malte Helmert and Franz Wotawa},
Keywords = {own, Automated Reasoning, Interactive Proof,
Semantic Embedding, Higher Order Logic, Higher Order
Modal Logic, Computational Metaphysics},
doi = {10.1007/978-3-319-46073-4},
Publisher = {Springer},
Series = {LNCS},
Title = {An Object-Logic Explanation for the Inconsistency in
{G\"odel's} Ontological Theory (Extended Abstract,
Sister Conferences)},
url = {https://www.researchgate.net/publication/311455987},
Year = 2016,
Pages = {244-250}
}
@inproceedings{C59,
Author = {Harold Boley and Christoph Benzm{\"u}ller and Meng
Luan and Zhendong Sha},
Booktitle = {Proceedings of the RuleML 2016 Challenge, the
Special Industry Track and the RuleML 2016 Doctoral
Consortium hosted by the 10th International Web Rule
Symposium (RuleML 2016)},
Editor = {Giurca, A. and Van Woensel, W. and Gr{\"u}tter,
R. and Teymourian, K. and Athan, T. and Proctor, M.},
Keywords = {own, Higher Order Logic, Higher Order Modal Logic},
Issn = {1613-0073},
Publisher = {CEUR-WS.org},
Volume = {Vol-1620},
Series = {CEUR Workshop Proceedings},
Title = {Translating Higher-Order Modal Logic from {RuleML}
to {TPTP}},
Url = {http://ceur-ws.org/Vol-1620/paper6.pdf},
Year = 2016
}
@inproceedings{W56,
Author = {Max Wisniewski and Alexander Steen and Christoph
Benzm{\"u}ller},
Booktitle = {ARQNL 2016. Automated Reasoning in Quantified
Non-Classical Logics},
Editor = {Christoph Benzm{\"u}ller and Jens Otten},
Keywords = {own, Higher Order Logic, Higher Order Modal Logic},
Publisher = {CEUR Workshop Proceedings, http://ceur-ws.org},
Url = {http://ceur-ws.org/Vol-1770/},
Volume = 1770,
Title = {{TPTP} and Beyond: Representation of Quantified
Non-Classical Logics},
Pages = {51-65},
Year = 2016
}
@inproceedings{C58,
Address = {Potsdam, Germany},
Author = {Max Wisniewski and Alexander Steen and Christoph
Benzm{\"u}ller},
Editor = {Andreas Schwill and Ulrike Lucke},
Booktitle = {Hochschuldidaktik der Informatik: 7. Fachtagung des
GI-Fachbereichs Informatik und Ausbildung/Didaktik
der Informatik; 13.-14. September 2016 an der
Universit{\"a}t Potsdam},
Keywords = {own, Computational Metaphysics},
isbn = {978-3-86956-376-3},
issn = {1868-0844},
Publisher = {Universit{\"a}tsverlag Potsdam},
Series = {Commentarii informaticae didacticae (CID)},
Title = {{Einsatz von Theorembeweisern in der Lehre}},
Pages = {81-92},
Url =
{https://publishup.uni-potsdam.de/opus4-ubp/frontdoor/index/index/docId/9485},
Year = 2016
}
@article{J31,
Author = {Steen, Alexander and Benzm{\"u}ller, Christoph},
Journal = {Logic and Logical Philosophy},
Volume = 25,
Pages = {535-554},
Issn = {1425-3305},
Keywords = {own, Multi-Valued Logic, Semantic Embedding, Higher
Order Logic, ERIH PLUS},
OPTurl = {http://christoph-benzmueller.de/papers/J33.pdf},
doi = {10.12775/LLP.2016.021},
Title = {Sweet {SIXTEEN}: Automation via Embedding into
Classical Higher-Order Logic},
Year = 2016
}
@inproceedings{C57,
Address = {Berlin, Germany},
Author = {Christoph Benzm{\"u}ller and Scott, Dana S.},
Booktitle = {Mathematical Software -- ICMS 2016, 5th
International Congress, Proceedings},
Editor = {G.-M. Greuel and T. Koch and P. Paule and
A. Sommese},
Isbn = {978-3-319-42431-6},
Keywords = {own, Higher Order Logic, Automated Reasoning, LEO
Prover},
doi = {10.1007/978-3-319-42432-3_6},
Publisher = {Springer},
Series = {LNCS},
Title = {Automating Free Logic in {Isabelle/HOL}},
url = {http://christoph-benzmueller.de/papers/C57.pdf},
Volume = 9725,
Year = 2016,
Pages = {43-50},
}
@inproceedings{C56,
Address = {Berlin, Germany},
Author = {Alexander Steen and Max Wisniewski and Christoph
Benzm{\"u}ller},
Booktitle = {Mathematical Software -- ICMS 2016, 5th
International Congress, Proceedings},
Editor = {G.-M. Greuel and T. Koch and P. Paule and
A. Sommese},
Isbn = {978-3-319-42431-6},
Keywords = {own, Higher Order Logic, Automated Reasoning, LEO
Prover},
doi = {10.1007/978-3-319-42432-3_10},
Publisher = {Springer},
Series = {LNCS},
Title = {Agent-Based {HOL} Reasoning},
url = {https://www.researchgate.net/publication/304919080},
Volume = 9725,
Year = 2016,
Pages = {75-81},
}
@inproceedings{C55,
Author = {Christoph Benzm{\"u}ller and Woltzenlogel Paleo,
Bruno},
OPTNote = {(Acceptance rate $\leq 25\%$)},
Booktitle = {IJCAI 2016},
Comment = {poster, proceedings-version},
Keywords = {own, Automated Reasoning, Interactive Proof,
Ontology Reasoning, LEO Prover, Higher Order Logic,
Computational Metaphysics, DFG-2501-Selected},
publisher = {AAAI Press},
Volume = {1-3},
Editor = {Subbarao Kambhampati},
Title = {The Inconsistency in {G{\"o}del's} Ontological
Argument: A Success Story for {AI} in Metaphysics},
url = {http://www.ijcai.org/Proceedings/16/Papers/137.pdf},
url = {https://www.researchgate.net/publication/301295955},
Isbn = {978-1-57735-770-4},
Year = 2016,
Pages = {936-942},
}
@inproceedings{C54,
Author = {Max Wisniewski and Alexander Steen and Kim Kern and
Christoph Benzm{\"u}ller},
Booktitle = {Automated Reasoning --- 8th International Joint
Conference, IJCAR 2016, Coimbra, Portugal, June 27
-- July 2, 2016, Proceedings},
Doi = {10.1007/978-3-319-40229-1_25},
Editor = {Nicola Olivetti and Ashish Tiwari},
Isbn = {978-3-319-40228-4},
Keywords = {own, Higher Order Logic, Automated Reasoning, LEO
Prover},
Pages = {362-370},
Publisher = {Springer},
Series = {LNCS},
Title = {Effective Normalization Techniques for {HOL}},
url = {http://christoph-benzmueller.de/papers/C54.pdf},
Volume = 9706,
Year = 2016,
}
@incollection{B15,
Author = {Benzm{\"u}ller, Christoph and Woltzenlogel Paleo,
Bruno},
Booktitle = {The Square of Opposition: A Cornerstone of Thought
(Collection of papers related to the World Congress
on the Square of Opposition IV, Vatican, 2014)},
OPTurl = {http://www.springer.com/us/book/9783319450612},
Doi = {10.1007/978-3-319-45062-9_18},
Pages = {307-313},
Editor = {B\'{e}ziau, Jean-Yves and Basti, Gianfranco},
Keywords = {own, Automated Reasoning, Interactive Proof,
Semantic Embedding, Higher Order Logic, Higher Order
Modal Logic, Computational Metaphysics},
Publisher = {Birkh\"auser Basel},
Series = {Studies in Universal Logic},
Title = {The Modal Collapse as a Collapse of the Modal Square
of Opposition},
url = {https://www.researchgate.net/publication/268211774},
Year = 2016,
}
@article{J33,
Author = {Benzm{\"u}ller, Christoph and Weber, Leon and
Woltzenlogel Paleo, Bruno},
Journal = {Logica Universalis},
Keywords = {own, Automated Reasoning, Interactive Proof,
Semantic Embedding, Higher Order Logic, Higher Order
Modal Logic, Computational Metaphysics,
DFG-2501-Selected},
Volume = 11,
Number = 1,
Pages = {139-151},
Doi = {10.1007/s11787-017-0160-9},
OPTurl = {http://christoph-benzmueller.de/papers/J32.pdf},
title = {Computer-Assisted Analysis of the
{Anderson-H\'{a}jek} Controversy},
Year = 2017,
url = {https://www.researchgate.net/publication/313943927},
}
@article{J32,
Author = {Christoph Benzm{\"u}ller},
Doi = {10.1007/s10992-016-9403-0},
Journal = {Journal of Philosophical Logic},
Volume = 46,
Number = 3,
Pages = {333-353},
Keywords = {own, Conditional Logic, Cut-Elimination, Semantic
Embedding, DFG-2501-Selected, ERIH PLUS},
Title = {Cut-Elimination for Quantified Conditional Logic},
url = {https://www.researchgate.net/publication/293488069},
Comment = {Springer Nature
Link},
Year = 2017,
}
@techreport{R57,
Author = {Christoph Benzm{\"u}ller and Max Wisniewski and
Alexander Steen},
Keywords = {own, Computational Metaphysics},
Title = {{Computational Metaphysics}},
Note = {This lecture course proposal received the 2015
central teaching award of FU Berlin},
Institution = {Freie Universität Berlin},
url = {https://dx.doi.org/10.13140/RG.2.1.3535.2568},
Year = 2015,
doi = {10.13140/RG.2.1.3535.2568}
}
@inproceedings{C53,
Address = {Rome, Italy},
Author = {Max Wisniewski and Christoph Benzm{\"u}ller},
Booktitle = {Proceedings of the 8th International Conference on
Agents and Artificial Intelligence (ICAART 2016) --
Volume 1, pages 281-286},
Doi = {10.5220/0005824702810286},
Editor = {van den Heerik, Jan and Filipe, Joaquim},
Isbn = {978-989-758-172-4},
Keywords = {own, Automated Reasoning, LEO Prover, Higher Order
Logic, Agents},
Pages = {281-286},
Publisher = {SCITEPRESS -- Science and Technology Publications,
Lda},
Title = {Is it Reasonable to Employ Agents in Theorem
Proving?},
url = {http://christoph-benzmueller.de/papers/C53.pdf},
Volume = 1,
Year = 2016,
}
@inproceedings{C52,
Author = {Christoph Benzm{\"u}ller and Woltzenlogel Paleo,
Bruno},
Booktitle = {Science \& Spiritual Quest, Proceedings of the 9th
All India Students' Conference, 30th October -- 1
November, 2015, IIT Kharagpur, India},
Comment = {slides},
Editor = {Mishram, Subhash C. and Uppaluri, Ramgopal and
Agarwal, Varun},
Keywords = {own, Higher Order Logic, Semantic Embedding, Modal
Logics, Automated Reasoning, Ontology Reasoning,
Computational Metaphysics},
Note = {(Invited paper)},
Pages = {23-40},
Publisher = {Bhaktivedanta Institute, Kolkata,
\url{www.binstitute.org}},
Title = {Experiments in Computational Metaphysics:
{G\"odel's} Proof of God's Existence},
url = {https://www.researchgate.net/publication/311587544},
Year = 2015,
}
@inproceedings{C51,
Address = {Suva, Fiji},
Author = {Alexander Steen and Christoph Benzm{\"u}ller},
Booktitle = {Logic for Programming, Artificial Intelligence, and
Reasoning (LPAR)},
Doi = {10.1007/978-3-662-48899-7_23},
Editor = {M. Davis and A. Fehnker and A. McIver and
A. Voronkov},
Isbn = {978-3-662-48898-0},
Keywords = {own, Higher Order Logic, Automated Reasoning, LEO
Prover},
Pages = {329-339},
Publisher = {Springer},
Series = {LNAI},
Title = {There Is No Best Beta-Normalization Strategy for
Higher-Order Reasoners},
url = {http://christoph-benzmueller.de/papers/C51.pdf},
Volume = 9450,
Year = 2015,
}
@inproceedings{C50,
Address = {Wroclaw, Poland},
Author = {Christoph Benzm{\"u}ller},
Booktitle = {TABLEAUX 2015},
Doi = {10.1007/978-3-319-24312-2_15},
Editor = {Hans De Nivelle},
Keywords = {own, Higher Order Logic, Semantic Embedding,
Automated Reasoning, Ontology Reasoning,
Computational Metaphysics},
Note = {(Invited paper)},
Pages = {213-220},
Publisher = {Springer},
Series = {LNAI},
Title = {Invited Talk: On a (Quite) Universal Theorem Proving
Approach and Its Application in Metaphysics},
url = {http://christoph-benzmueller.de/papers/C50.pdf},
Volume = 9323,
Year = 2015,
}
@inproceedings{C49,
Author = {Alexander Steen and Christoph Benzm{\"u}ller},
Booktitle = {7th International Conference Non-Classical Logic --
Theory and Applications, Torun, Poland},
Keywords = {own, Higher Order Logic, Semantic Embedding, Multi
Valued Logics, Automated Reasoning},
Title = {Sweet SIXTEEN: Automation via Embedding into
Classical Higher-Order Logic},
url = {http://christoph-benzmueller.de/papers/C49.pdf},
Year = 2015,
}
@techreport{R56,
Author = {Christoph Benzm{\"u}ller and Woltzenlogel Paleo,
Bruno},
Comment = {complete-formalisation},
publisher = {arXiv},
note = {Preprint},
Title = {Formalization, Mechanization and Automation of
{G{\"o}del's} Proof of {God's} Existence},
OPTurl = {http://arxiv.org/abs/1308.4526},
Doi = {10.48550/arXiv.1308.4526},
Year = 2013,
}
@article{J29,
Author = {Christoph Benzm{\"u}ller and Nik Sultana and
Paulson, Lawrence C. and Frank Theiss},
Doi = {10.1007/s10817-015-9348-y},
Journal = {Journal of Automated Reasoning},
publisher = {Springer Netherlands},
Keywords = {own, Automated Reasoning, Interactive Proof,
Ontology Reasoning, LEO Prover, Higher Order Logic,
DFG-2501-Selected},
Number = 4,
Pages = {389-404},
Title = {The Higher-Order Prover {LEO-II}},
url = {https://www.researchgate.net/publication/280986731},
Volume = 55,
Year = 2015,
}
@inproceedings{C48,
Address = {Wroclaw, Poland},
Author = {Nik Sultana and Christoph Benzm{\"u}ller and
Paulson, Lawrence C.},
Booktitle = {FroCoS 2015},
Doi = {10.1007/978-3-319-24246-0_16},
Editor = {Carsten Lutz and Silvio Ranise},
Keywords = {own, Automated Reasoning, Interactive Proof,
Ontology Reasoning, LEO Prover, Higher Order Logic},
Pages = {256-271},
Publisher = {Springer},
Series = {LNAI},
Title = {Proofs and reconstructions},
url = {http://christoph-benzmueller.de/papers/C48.pdf},
Volume = 9322,
Year = 2015,
}
@inproceedings{C47,
Address = {Berlin, Germany},
Author = {Christoph Benzm{\"u}ller and Maximilian Claus and
Nik Sultana},
Booktitle = {PxTP 2015},
Comment = {slides},
Doi = {10.4204/EPTCS.186.5},
Editor = {Cezary Kaliszyk and Andrei Paskevich},
Issn = {2075-2180},
Keywords = {own, Automated Reasoning, Interactive Proof,
Ontology Reasoning, LEO Prover, Higher Order Logic},
Pages = {27-41},
Publisher = {EPTCS},
Title = {Systematic Verification of the Modal Logic Cube in
{Isabelle/HOL}},
url = {http://christoph-benzmueller.de/papers/C47.pdf},
Volume = 186,
Year = 2015,
}
@inproceedings{C46,
Address = {Berlin, Germany},
Author = {Christoph Benzm{\"u}ller and Woltzenlogel Paleo,
Bruno},
Booktitle = {Reasoning Web 2015},
Doi = {10.1007/978-3-319-21768-0_2},
Editor = {Adrian Paschke and Wolfgang Faber},
Keywords = {own, Automated Reasoning, Interactive Proof,
Ontology Reasoning, LEO Prover, Higher Order Logic,
Computational Metaphysics},
Note = {(Invited paper)},
Number = 9203,
Pages = {32-74},
Publisher = {Springer},
Series = {LNCS},
Title = {Higher-Order Modal Logics: Automation and
Applications},
url = {https://www.researchgate.net/publication/281677232},
Year = 2015,
}
@inproceedings{C45,
Author = {Max Wisniewski and Alexander Steen and Christoph
Benzm{\"{u}}ller},
Booktitle = {Intelligent Computer Mathematics - International
Conference, {CICM} 2015, Washington, DC, USA, July
13-17, 2015, Proceedings},
Doi = {10.1007/978-3-319-20615-8_22},
Editor = {Manfred Kerber and Jacques Carette and Cezary
Kaliszyk and Florian Rabe and Volker Sorge},
Keywords = {own, Automated Reasoning, LEO Prover, Higher Order
Logic, Agents},
Pages = {325--330},
Publisher = {Springer},
Series = {LNCS},
Title = {LeoPARD - {A} Generic Platform for the
Implementation of Higher-Order Reasoners},
url = {http://christoph-benzmueller.de/papers/C45.pdf},
Volume = 9150,
Year = 2015,
}
@misc{C45arxiv,
doi = {10.48550/ARXIV.1505.01629},
OPTurl = {https://arxiv.org/abs/1505.01629},
author = {Wisniewski, Max and Steen, Alexander and
Benzm{\"u}ller, Christoph},
title = {LeoPARD --- A Generic Platform for the
Implementation of Higher-Order Reasoners},
publisher = {arXiv},
note = {Preprint},
year = 2015,
copyright = {arXiv.org perpetual, non-exclusive license}
}
@inproceedings{C44,
Author = {Christoph Benzm{\"{u}}ller and Woltzenlogel Paleo,
Bruno},
Booktitle = {Computer Science - Theory and Applications - 10th
International Computer Science Symposium in Russia,
{CSR} 2015, Listvyanka, Russia, July 13-17, 2015,
Proceedings},
Doi = {10.1007/978-3-319-20297-6_25},
Editor = {Lev D. Beklemishev and Daniil V. Musatov},
Keywords = {own, Automated Reasoning, Interactive Proof,
Ontology Reasoning, LEO Prover, Higher Order Logic,
Computational Metaphysics},
Pages = {398--411},
Publisher = {Springer},
Series = {LNCS},
Title = {Interacting with Modal Logics in the {Coq} Proof
Assistant},
url = {https://www.researchgate.net/publication/273201458},
Volume = 9139,
Year = 2015,
}
@misc{C41,
Author = {Christoph Benzm{\"u}ller and Woltzenlogel Paleo,
Bruno},
Keywords = {own, Automated Reasoning, Interactive Proof,
Ontology Reasoning, LEO Prover, Higher Order Logic,
Computational Metaphysics},
Note = {(Non-reviewed, superseded by CSR-2015 paper)},
Title = {Modal Logic in Coq and Scott's Version of
{G\"odel's} Proof of {God}'s Existence (Rough
Diamond Proof Pearl)},
Year = 2014
}
@inproceedings{C43,
Author = {Christoph Benzm{\"u}ller},
Booktitle = {Handbook of the 1st World Congress on Logic and
Religion, Jo\~ao Pessoa, Brazil},
Editor = {Ricardo Souza Silvestre and Jean-Yves B\'eziau},
Keywords = {own, Automated Reasoning, Interactive Proof,
Ontology Reasoning, LEO Prover, Higher Order Logic,
Computational Metaphysics},
Note = {(Invited abstract)},
Pages = 13,
Title = {{G\"{o}del's} Ontological Argument Revisited --
Findings from a Computer-supported Analysis
(invited)},
Url =
{http://christoph-benzmueller.de/papers/2015-handbook-logic-and-religion.pdf},
Year = 2015,
}
@inproceedings{C42,
Author = {Christoph Benzm{\"u}ller and Leon Weber and Bruno
Woltzenlogel Paleo},
Booktitle = {Handbook of the 1st World Congress on Logic and
Religion, Joao Pessoa, Brazil},
Editor = {Ricardo Souza Silvestre and Jean-Yves B\'eziau},
Keywords = {own, Automated Reasoning, Interactive Proof,
Ontology Reasoning, LEO Prover, Higher Order Logic,
Computational Metaphysics},
Note = {(superseded by 2016 paper in Logica Universalis)},
Pages = {53-54},
Title = {Computer-Assisted Analysis of the
{Anderson-H\'{a}jek} Ontological Controversy},
Url =
{http://christoph-benzmueller.de/papers/2015-handbook-logic-and-religion.pdf},
Year = 2015,
}
@inproceedings{W55,
Address = {Sinaia, Romania},
Author = {Christoph Benzm{\"u}ller and Woltzenlogel Paleo,
Bruno},
Booktitle = {Recent Trends in Algebraic Development Techniques:
22nd International Workshop, WADT 2014, Sinaia,
Romania, September 4-7, 2014, Revised Selected
Papers},
Doi = {10.1007/978-3-319-28114-8_1},
Editor = {Codescu, Mihai and Diaconescu, Razvan and Tutu,
Ionut},
Isbn = {978-3-319-28114-8},
Keywords = {own, Higher Order Logic, Semantic Embedding, Modal
Logics, Automated Reasoning, Computational
Metaphysics},
Note = {(Invited paper)},
Number = 9563,
Pages = {3-6},
Publisher = {Springer},
Series = {LNCS},
Title = {On Logic Embeddings and {G\"odel's} {God}},
url = {https://www.researchgate.net/publication/300112614},
Year = 2015,
}
@proceedings{E14,
Comment = {event-website},
Editor = {Christoph Benzm{\"u}ller and Jens Otten},
issn = {2398-7340},
Pages = {1-86},
Publisher = {EasyChair},
Series = {EPiC Series in Computing},
Title = {ARQNL 2014. Automated Reasoning in Quantified
Non-Classical Logics},
Url =
{https://easychair.org/publications/volume/ARQNL_2014/},
Volume = 33,
Year = 2015,
}
@proceedings{E13,
Doi = {10.4204/EPTCS.167},
Editor = {Benzm{\"u}ller, Christoph and Woltzenlogel Paleo,
Bruno},
Issn = {2075-2180},
Pages = {1-94},
Series = {Electronic Proceedings in Theoretical Computer
Science (EPTCS)},
Title = {Proceedings of the 11th International Workshop on
User Interfaces for Theorem Provers (UITP 2014),
Vienna, Austria},
Url =
{http://eptcs.web.cse.unsw.edu.au/content.cgi?UITP2014},
Volume = 167,
Year = 2014,
}
@inproceedings{W54,
Author = {Christoph Benzm{\"u}ller},
Booktitle = {ARQNL 2014. Automated Reasoning in Quantified
Non-Classical Logics},
Editor = {Christoph Benzm{\"u}ller and Jens Otten},
issn = {2398-7340},
Keywords = {own, LEO Prover, Automated Reasoning, Proof
Transformation, Higher Order Logic},
Pages = {37-41},
Publisher = {EasyChair},
Series = {EPiC Series in Computing},
Title = {{HOL} Provers for First-order Modal Logics ---
Experiments},
Url = {https://easychair.org/publications/paper/sdnL},
Volume = 33,
Year = 2015,
Doi = {10.29007/przw},
}
@inproceedings{W53,
Author = {Max Wisniewski and Alexander Steen and Christoph
Benzm{\"u}ller},
Booktitle = {Joint Automated Reasoning Workshop and
Deduktionstreffen},
Editor = {Alexander Bolotov and Manfred Kerber},
Keywords = {own, LEO Prover, Automated Reasoning, Proof
Transformation, Higher OrderLogic},
Pages = 38,
Title = {The {Leo-III} Project},
url = {http://christoph-benzmueller.de/papers/W53.pdf},
Year = 2014,
}
@incollection{B14,
Address = {London, UK},
Author = {Christoph Benzm{\"u}ller},
Booktitle = {All about Proofs, Proof for All},
Comment = {publisher},
Editor = {David Delahaye and Woltzenlogel Paleo, Bruno},
Isbn = {978-1-84890-166-7},
Keywords = {own, Automated Reasoning, Higher Order Logic},
Pages = {171-214},
Publisher = {College Publications},
Series = {Mathematical Logic and Foundations},
Title = {Higher-Order Automated Theorem Provers},
url = {http://christoph-benzmueller.de/papers/B14.pdf},
Year = 2015,
}
@misc{R55,
doi = {10.48550/ARXIV.1303.3761},
OPTurl = {https://arxiv.org/abs/1303.3761},
author = {Benzm{\"u}ller, Christoph and Sultana, Nik},
title = {Update report: LEO-II version 1.5},
publisher = {arXiv},
note = {Preprint},
year = 2013,
copyright = {arXiv.org perpetual, non-exclusive license}
}
@inproceedings{C40,
Author = {Christoph Benzm{\"u}ller and Woltzenlogel Paleo,
Bruno},
OPTNote = {(Acceptance rate $\leq 28\%$)},
Booktitle = {ECAI 2014},
Comment = {slides},
Doi = {10.3233/978-1-61499-419-0-93},
Editor = {Torsten Schaub and Gerhard Friedrich and Barry
O'Sullivan},
Keywords = {own, Automated Reasoning, Interactive Proof,
Ontology Reasoning, LEO Prover, Higher Order Logic,
Computational Metaphysics, DFG-2501-Selected},
Pages = {93 -- 98},
Publisher = {IOS Press},
Series = {Frontiers in Artificial Intelligence and
Applications},
Title = {Automating {G\"{o}del's} Ontological Proof of
{God}'s Existence with Higher-order Automated
Theorem Provers},
url = {https://www.researchgate.net/publication/265050231},
Volume = 263,
Year = 2014,
}
@incollection{B13,
Author = {Christoph Benzm{\"u}ller and Dale Miller},
Booktitle = {Handbook of the History of Logic, Volume 9 ---
Computational Logic},
Doi = {10.1016/B978-0-444-51624-4.50005-8},
Editor = {Gabbay, Dov M. and Siekmann, J\"org H. and Woods,
John},
Isbn = {978-0-444-51624-4},
Keywords = {own, Automated Reasoning, Higher Order Logic,
History of Logic, DFG-2501-Selected},
Pages = {215-254},
Publisher = {North Holland, Elsevier},
Title = {Automation of Higher-Order Logic},
url = {http://christoph-benzmueller.de/papers/B5.pdf},
Year = 2014,
}
@inproceedings{C39,
Author = {Christoph Benzm{\"u}ller and Woltzenlogel Paleo,
Bruno},
Booktitle = {Handbook of the World Congress on the Square of
Opposition IV},
Editor = {Jean-Yves Beziau and Katarzyna Gan-Krzywoszynska},
Keywords = {own, Automated Reasoning, Interactive Proof,
Ontology Reasoning, LEO Prover, Higher Order Logic,
Computational Metaphysics},
Note = {(superseded by ECAI-2014 paper)},
Pages = {22-23},
Title = {{G\"odel's} Proof of {God's} Existence},
Url =
{http://www.stoqatpul.org/lat/materials/hand_square2014.pdf},
Year = 2014,
}
@article{J28,
Author = {Christoph Benzm{\"u}ller and Woltzenlogel Paleo,
Bruno},
Journal = {Archive of Formal Proofs (data publication)},
Keywords = {own, Automated Reasoning, Interactive Proof,
Ontology Reasoning, LEO Prover, Higher Order Logic,
Computational Metaphysics},
Title = {{G{\"o}del's God in Isabelle/HOL}},
Url = {http://afp.sourceforge.net/entries/GoedelGod.shtml},
Year = 2013,
Pages = {1--5},
}
@inproceedings{W51,
Author = {Christoph Benzm{\"u}ller},
Booktitle = {Proceedings of the International Workshop on
Algebraic Logic in Computer Science},
Comment = {event-website},
Editor = {Clint van Alten, Petr Cintula, Carles Noguera},
Title = {Cut-free Calculi for Challenge Logics in a Lazy Way},
url = {http://christoph-benzmueller.de/papers/W51.pdf},
Year = 2013,
}
@inproceedings{W50,
Author = {Christoph Benzm{\"u}ller and Woltzenlogel Paleo,
Bruno},
Booktitle = {Proceedings of the 10th International Workshop on
the Implementation of Logics},
Comment = {event-website},
Editor = {Schulz, S. and Sutcliffe, G. and Konev, B.},
Note = {(Invited paper)},
Title = {{G\"odel's} {God} on the Computer},
url = {http://christoph-benzmueller.de/papers/W50.pdf},
Year = 2013,
Keywords = {own, Automated Reasoning, Interactive Proof,
Ontology Reasoning, LEO Prover, Higher Order Logic,
Computational Metaphysics},
}
@inproceedings{C38,
Address = {Stellenbosch, South Africa},
Author = {Christoph Benzm{\"u}ller and Thomas Raths},
Booktitle = {Proceedings of the 19th International Conference on
Logic for Programming, Artificial Intelligence and
Reasoning (LPAR)},
Doi = {10.1007/978-3-642-45221-5_9},
Editor = {Kenneth L. McMillan and Aart Middeldorp and Andrei
Voronkov},
Isbn = {978-3-642-45220-8},
Keywords = {own, Higher Order Logic, Semantic Embedding, Modal
Logics, Automated Reasoning},
Pages = {127-136},
Publisher = {Springer},
Series = {LNCS},
Title = {{HOL} based First-order Modal Logic Provers},
url = {http://christoph-benzmueller.de/papers/C38.pdf},
Volume = 8312,
Year = 2013,
}
@techreport{R54,
Author = {Christoph Benzm{\"u}ller},
Keywords = {own, Automated Reasoning},
Title = {{CADE 2015 in Berlin: A Proposal}},
Institution = {Freie Universität Berlin},
Year = 2013
}
@inproceedings{W49,
Address = {Corunna, Spain},
Author = {Christoph Benzm{\"u}ller and Marco Ziener},
Booktitle = {The 5th International Workshop on Acquisition,
Representation and Reasoning with Contextualized
Knowledge (ARCOE-LogIC 2013)},
Editor = {Michael Fink and Martin Homola and Alessandra Mileo
and Ivan Jose Varzinczak},
Keywords = {own, Automated Reasoning, Ontology Reasoning, LEO
Prover, Higher Order Logic},
Title = {Automated Consistency Checking of Expressive
Ontologies --- Beware of the Wrong Interpretation of
Success!},
url = {http://christoph-benzmueller.de/papers/W49.pdf},
Year = 2013,
}
@inproceedings{C37,
Address = {Beijing, China},
Author = {Christoph Benzm{\"u}ller},
Booktitle = {23rd International Joint Conference on Artificial
Intelligence (IJCAI-13)},
Comment = {poster},
Editor = {Francesca Rossi},
Publisher = {AAAI Press},
Isbn = {978-1-57735-633-2},
Keywords = {own, Higher Order Logic, LEO Prover, Semantic
Embedding, Conditional Logics, Combinations of
Logics},
Pages = {746-753},
Title = {Automating Quantified Conditional Logics in {HOL}},
url = {http://christoph-benzmueller.de/papers/C37.pdf},
Year = 2013,
}
@inproceedings{W52,
Author = {Christoph Benzm{\"u}ller and Nik Sultana},
Booktitle = {PxTP 2013},
Editor = {Jasmin Christian Blanchette and Josef Urban},
issn = {2398-7340},
Keywords = {own, LEO Prover, Automated Reasoning, Proof
Transformation, Higher Order Logic},
Pages = {2-10},
Publisher = {EasyChair},
Series = {EPiC Series in Computing},
Title = {{LEO-II} Version 1.5},
OPTurl =
{http://www.easychair.org/publications/?page=1802176591},
Volume = 14,
Year = 2013,
Doi = {10.29007/lbxw},
}
@incollection{B1,
Author = {J{\"o}rg Siekmann and Christoph Benzm{\"u}ller and
Armin Fiedler and Andreas Meier and Immanuel Normann
and Martin Pollet},
Booktitle = {Thirty Five Years of Automating Mathematics},
Doi = {10.1007/978-94-017-0253-9_11},
Editor = {Fairouz Kamareddine},
Isbn = {978-1-402-01656-1},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Automated Reasoning, Proof Planning, System
Integration},
Pages = {271-314},
Publisher = {Kluwer Academic Publishers},
Series = {Applied Logic series (28)},
Title = {Proof Development in {OMEGA}: The Irrationality of
Square Root of 2},
url = {http://christoph-benzmueller.de/papers/B1.pdf},
Year = 2003,
}
@incollection{B9,
Author = {Serge Autexier and Christoph Benzm{\"u}ller and
Dominik Dietrich and J\"org Siekmann},
Booktitle = {Resource-Adaptive Cognitive Processes},
Doi = {10.1007/978-3-540-89408-7_17},
Editor = {Matthew W. Crocker and J\"org Siekmann},
Isbn = {978-3-540-89407-0},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Automated Reasoning, Proof Planning, System
Integration, Agents},
Note = {(Final project report, DFG SFB 378)},
Pages = {389-423},
Publisher = {Springer},
Series = {Cognitive Technologies},
Title = {{OMEGA}: Resource-Adaptive Processes in an Automated
Reasoning Systems},
url = {http://christoph-benzmueller.de/papers/B10.pdf},
Year = 2010,
}
@incollection{B10,
Author = {Christoph Benzm{\"u}ller and Marvin Schiller and
J\"org Siekmann},
Booktitle = {Resource-Adaptive Cognitive Processes},
Doi = {10.1007/978-3-540-89408-7_13},
Editor = {Matthew W. Crocker and J\"org Siekmann},
Isbn = {978-3-540-89407-0},
Keywords = {own, Proof Presentation, DIALOG, Natural Language
Dialog, Proof Assistants, Machine Learning, Tutoring
Systems},
Note = {(Final project report, DFG SFB 378)},
Pages = {291-311},
Publisher = {Springer},
Series = {Cognitive Technologies},
Title = {Resource-Bounded Modelling and Analysis of
Human-Level Interactive Proofs},
url = {http://christoph-benzmueller.de/papers/B11.pdf},
Year = 2010,
}
@incollection{B11,
Author = {Christoph Benzm{\"u}ller},
Booktitle = {Verification, Induction, Termination Analysis -
Festschrift for Christoph Walther on the Occasion of
His 60th Birthday},
Doi = {10.1007/978-3-642-17172-7_7},
Editor = {Simon Siegler and Nathan Wasser},
Keywords = {own, Modal Logics, Semantic Embedding, Higher Order
Logic, Automated Reasoning, LEO Prover},
Note = {(Superseded by PxTP-2015 paper)},
Pages = {117-128},
Publisher = {Springer},
Series = {LNCS},
Title = {Verifying the Modal Logic Cube is an Easy Task (for
Higher-Order Automated Reasoners)},
url = {http://christoph-benzmueller.de/papers/B12.pdf},
Volume = 6463,
Year = 2010,
}
@incollection{B12,
Author = {Christoph Benzm{\"u}ller and Adam Pease},
Booktitle = {Ontology: A Practical Guide},
Editor = {Adam Pease},
Isbn = {978-1-889455-10-5},
Keywords = {own, Ontology Reasoning, Automated Reasoning, Higher
Order Logic},
Note = {(This chapter has some essential overlap with the
2012 journal paper with A. Pease titled Higher-Order
Aspects and Context in SUMO)},
Pages = {171-214},
Address = {Angwin, CA, USA},
Publisher = {Articulate Software Press},
Title = {Knowledge Engineering Tools},
Url = {http://www.ontologyportal.org/Book.html},
Year = 2011,
}
@incollection{B2,
Abstract = {Accessing knowledge of a single knowledge source
with different client applications often requires
the help of mediator systems as middleware
components. In the domain of theorem proving large
efforts have been made to formalize knowledge for
mathematics and verification issues, and to
structure it in databases. But these databases are
either specialized for a single client, or if the
knowledge is stored in a general database, the
services this database can provide are usually
limited and hard to adjust for a particular theorem
prover. Only recently there have been initiatives to
flexibly connect existing theorem proving systems
into networked environments that contain large
knowledge bases. An intermediate layer containing
both, search and proving functionality can be used
to mediate between the two. In this paper we
motivate the need and discuss the requirements for
mediators between mathematical knowledge bases and
theorem proving systems. We also present an attempt
at a concurrent mediator between a knowledge base
and a proof planning system.},
Author = {Christoph Benzm{\"u}ller and Andreas Meier and
Volker Sorge},
Booktitle = {Mechanizing Mathematical Reasoning: Essays in Honor
of {J{\"o}rg Siekmann} on the Occasion of His 60th
Birthday},
Doi = {10.1007/978-3-540-32254-2_17},
Editor = {Dieter Hutter and Werner Stephan},
Isbn = {978-3-540-25051-7},
Keywords = {own, Proof Assistants, OMEGA, Mathematical Knowledge
Management, System Integration, Interactive Proof},
Pages = {277-296},
Publisher = {Springer},
Series = {LNCS},
Title = {Bridging Theorem Proving and Mathematical Knowledge
Retrieval},
url = {http://christoph-benzmueller.de/papers/B2.pdf},
Volume = 2605,
Year = 2004,
}
@incollection{B3,
Author = {Christoph Benzm{\"u}ller and Armin Fiedler and
Andreas Meier and Martin Pollet and J{\"o}rg
Siekmann},
Booktitle = {The Seventeen Provers of the World},
Doi = {10.1007/11542384_17},
Editor = {Freek Wiedijk},
Isbn = {978-3-540-30704-4},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Automated Reasoning, Proof Planning, System
Integration},
Number = 3600,
Pages = {127-141},
Publisher = {Springer},
Series = {LNCS},
Title = {OMEGA},
url = {http://christoph-benzmueller.de/papers/B3.pdf},
Year = 2006,
}
@incollection{B8,
Author = {Claus-Peter Wirth and J{\"o}rg Siekmann and
Christoph Benzm{\"u}ller and Serge Autexier},
Booktitle = {Handbook of the History of Logic, Volume 5 -- Logic
from Russell to Church},
Doi = {10.1016/S1874-5857(09)70009-3},
Editor = {Dov Gabbay and John Woods},
Issn = {1874-5857},
Keywords = {own, Jacques Herbrand, History of Logic},
Publisher = {Elsevier},
Title = {Jacques {Herbrand}: Life, Logic, and Automated
Deduction},
Year = 2009,
}
@incollection{B4,
Author = {Christoph Benzm{\"u}ller and Chad Brown},
Booktitle = {From Insight to Proof -- Festschrift in Honour of
Andrzej Trybulec},
Editor = {Roman Matuszewski and Anna Zalewska},
Isbn = {978-83-7431-128-1},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Higher Order Logic},
Pages = {299-388},
Publisher = {The University of Bialystok, Polen},
Series = {Studies in Logic, Grammar, and Rhetoric},
Title = {The curious inference of {B}oolos in {MIZAR} and
{OMEGA}},
url = {http://christoph-benzmueller.de/papers/B6.pdf},
Volume = {10(23)},
Year = 2007,
}
@incollection{B5,
Author = {Christoph Benzm{\"u}ller and Helmut Horacek and
Ivana Kruijff-Korbayova and Manfred Pinkal and
J{\"o}rg Siekmann and Magdalena Wolska},
Booktitle = {Cognitive Systems},
Doi = {10.1007/978-3-540-70934-3_1},
Editor = {Ruqian Lu and J{\"o}rg Siekmann and Carsten Ullrich},
Isbn = {978-3-540-70933-6},
Keywords = {own, DIALOG, Proof Presentation, Natural Language
Dialog, Proof Assistants, Tutoring Systems},
Pages = {1-14},
Publisher = {Springer},
Series = {LNCS},
Title = {Natural Language Dialog with a Tutor System for
Mathematical Proofs},
url = {http://christoph-benzmueller.de/papers/B7.pdf},
Volume = 4429,
Year = 2007,
}
@incollection{B6,
Author = {Christoph Benzm{\"u}ller and Chad Brown and Michael
Kohlhase},
Booktitle = {Reasoning in Simple Type Theory --- Festschrift in
Honor of Peter B.~Andrews on His 70th Birthday},
Editor = {Christoph Benzm{\"u}ller and Chad Brown and J{\"o}rg
Siekmann and Richard Statman},
Isbn = {978-1-904987-70-3},
Keywords = {own, Higher Order Logic},
Pages = {84-100},
Publisher = {College Publications},
Series = {Studies in Logic, Mathematical Logic and
Foundations},
Title = {Cut Elimination with Xi-Functionality},
url = {http://christoph-benzmueller.de/papers/B8.pdf},
Year = 2008,
}
@incollection{B7,
Author = {Christoph Benzm{\"u}ller and Paulson, Lawrence C.},
Booktitle = {Reasoning in Simple Type Theory --- Festschrift in
Honor of {Peter B. Andrews} on His 70th Birthday},
Editor = {Christoph Benzm{\"u}ller and Chad Brown and J{\"o}rg
Siekmann and Richard Statman},
Isbn = {978-1-904987-70-3},
Keywords = {own, Higher Order Logic, LEO Prover, Semantic
Embedding, Modal Logics},
Note = {(Superseded by 2013 paper in Logica Universalis)},
Pages = {386-406},
Publisher = {College Publications},
Series = {Studies in Logic, Mathematical Logic and
Foundations},
Title = {Exploring Properties of Normal Multimodal Logics in
Simple Type Theory with {LEO-II}},
url = {http://christoph-benzmueller.de/papers/B9.pdf},
Year = 2008,
}
@inproceedings{C1,
Abstract = {{Omega} is a mixed-initiative system with the
ultimate purpose of supporting theorem proving in
main-stream mathematics and mathematics
education. The current system consists of a proof
planner and an integrated collection of tools for
formulating problems, proving subproblems, and proof
presentation.},
Author = {Christoph Benzm{\"u}ller and Lassaad Cheikhrouhou
and Detlef Fehrer and Armin Fiedler and Xiaorong
Huang and Manfred Kerber and Michael Kohlhase and
Karsten Konrad and Erica Melis and Andreas Meier and
Wolf Schaarschmidt and J{\"o}rg Siekmann and Volker
Sorge},
Booktitle = {Automated Deduction - CADE-14, 14th International
Conference on Automated Deduction, Townsville, North
Queensland, Australia, July 13-17, 1997,
Proceedings},
Doi = {10.1007/3-540-63104-6_23},
Editor = {William McCune},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Automated Reasoning, Proof Planning, System
Integration},
Number = 1249,
Pages = {252-255},
Publisher = {Springer},
Series = {LNCS},
Title = {{OMEGA}: Towards a mathematical assistant},
url = {http://christoph-benzmueller.de/papers/C1.pdf},
Year = 1997,
}
@inproceedings{C10,
Abstract = {This paper discusses an agent based approach to
automated and interactive reasoning. It combines
ideas from two subfields of AI (theorem
proving/proof planning and multi-agent systems) and
makes use of state of the art distribution
techniques to decentralise and spread its reasoning
agents over the internet. The approach particularly
supports cooperative proofs between reasoning agents
which are strong in different applications areas,
e.g., higher-order and first-order theorem provers
and computer algebra systems.},
Author = {Christoph Benzm{\"u}ller and Mateja Jamnik and
Manfred Kerber and Volker Sorge},
Booktitle = {KI 2001: Advances in Artificial Intelligence, Joint
German/Austrian Conference on AI, Vienna, Austria,
September 19-21, 2001, Proceedings},
Comment = {slides},
Doi = {10.1007/3-540-45422-5_29},
Editor = {Franz Baader and Gerhard Brewka and Thomas Eiter},
Keywords = {own, Proof Assistants, OMEGA, LEO Prover, Automated
Reasoning, System Integration, Agents},
Number = 2174,
Pages = {409-424},
Publisher = {Springer},
Series = {LNCS},
Title = {Experiments with an Agent-oriented Reasoning system},
url = {http://christoph-benzmueller.de/papers/C10.pdf},
Year = 2001,
}
@inproceedings{C11,
Address = {Copenhagen, Denmark},
Author = {J{\"o}rg Siekmann and Christoph Benzm{\"u}ller and
Vladimir Brezhnev and Lassaad Cheikhrouhou and Armin
Fiedler and Andreas Franke and Helmut Horacek and
Michael Kohlhase and Andreas Meier and Erica Melis
and Markus Moschner and Immanuel Normann and Martin
Pollet and Volker Sorge and Carsten Ullrich and
Claus-Peter Wirth and J{\"u}rgen Zimmer},
Booktitle = {Proceedings of the 18th International Conference on
Automated Deduction (CADE-18)},
Comment = {slides},
Doi = {10.1007/3-540-45620-1_12},
Editor = {Andrei Voronkov},
Isbn = 3540439315,
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Automated Reasoning, Proof Planning, System
Integration},
Number = 2392,
Pages = {144-149},
Publisher = {Springer},
Series = {LNCS},
Title = {Proof Development with {OMEGA}},
url = {http://christoph-benzmueller.de/papers/C11.pdf},
Year = 2002,
}
@inproceedings{C12,
Abstract = {Freek Wiedijk proposed the well-known theorem about
the irrationality of sqrt{2} as a case study and
used this theorem for a comparison of fifteen
(interactive) theorem proving systems, which were
asked to present their solution. This represents an
important shift of emphasis in the field of
automated deduction away from the somehow artificial
problems of the past as represented, for example, in
the test set of the TPTP library back to real
mathematical challenges. In this paper we present an
overview of the OMEGA system as far as it is
relevant for the purpose of this paper and show the
development of a proof for this theorem.},
Author = {J\"org Siekmann and Christoph Benzm{\"u}ller and
Armin Fiedler and Andreas Meier and Martin Pollet},
Booktitle = {Logic for Programming, Artificial Intelligence, and
Reasoning, 9th International Conference, LPAR 2002},
Comment = {slides},
Editor = {Matthias Baaz and Andrei Voronkov},
Isbn = 3540000100,
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Automated Reasoning, Proof Planning, System
Integration},
Number = 2514,
Pages = {367-387},
Publisher = {Springer},
Series = {LNCS},
Title = {Proof Development with {OMEGA}: Sqrt(2) is
irrational},
url = {http://christoph-benzmueller.de/papers/C12.pdf},
Year = 2002,
}
@inproceedings{C13,
Address = {Acapulco, Mexico},
Author = {Quoc Bao Vo and Christoph Benzm{\"u}ller and Serge
Autexier},
Booktitle = {Proceedings of the International Joint Conference on
Artificial Intelligence (IJCAI)},
Comment = {poster},
Editor = {G. Gottlob and T. Walsh},
Keywords = {own, Proof Assistants, OMEGA, Proof Planning, Deep
Inference},
Note = {ISBN 0-127-05661-0},
Title = {Assertion Application in Theorem Proving and Proof
Planning},
url = {http://christoph-benzmueller.de/papers/C13.pdf},
Year = 2003,
}
@inproceedings{C14,
Address = {Lisbon, Portugal},
Author = {Magdalena Wolska and Bao Quoc Vo and Dimitra
Tsovaltzi and Ivana Kruijff-Korbayova and Elena
Karagjosova and Helmut Horacek and Malte Gabsdil and
Armin Fiedler and Christoph Benzm{\"u}ller},
Booktitle = {Proceedings of International Conference on Language
Resources and Evaluation (LREC 2004)},
Keywords = {own, DIALOG, Proof Presentation, Natural Language
Dialog, Tutoring Systems},
Publisher = {ELDA},
Title = {An annotated corpus of tutorial dialogs on
mathematical theorem proving},
url = {http://christoph-benzmueller.de/papers/C14.pdf},
Year = 2004,
}
@inproceedings{C15,
Address = {Ulm, Germany},
Author = {J{\"o}rg Siekmann and Christoph Benzm{\"u}ller},
Booktitle = {KI 2004: Advances in Artificial Intelligence, 27th
Annual German Conference on AI, KI 2004, Ulm,
Germany, September 20-24, 2004, Proceedings},
Doi = {10.1007/978-3-540-30221-6_2},
Editor = {Susanne Biundo and Thom W. Fr{\"u}hwirth and
G{\"u}nther Palm},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Automated Reasoning, Proof Planning, System
Integration},
Number = 3228,
Pages = {3-28},
Series = {LNCS},
Title = {{OMEGA}: Computer Supported Mathematics},
url = {http://christoph-benzmueller.de/papers/C15.pdf},
Year = 2004,
}
@inproceedings{C16,
Author = {Christoph Benzm{\"u}ller and Volker Sorge and Mateja
Jamnik and Manfred Kerber},
Booktitle = {Logic for Programming, Artificial Intelligence, and
Reasoning, 11th International Conference, LPAR 2004,
Montevideo, Uruguay, March 14-18, 2005, Proceedings},
Comment = {slides},
Doi = {10.1007/978-3-540-32275-7_27},
Editor = {Franz Baader and Andrei Voronkov},
Keywords = {own, Higher Order Logic, Automated Reasoning, LEO
Prover, System Integration},
Number = 3452,
Pages = {415-431},
Publisher = {Springer},
Series = {LNCS},
Title = {Can a Higher-Order and a First-Order Theorem Prover
Cooperate?},
url = {http://christoph-benzmueller.de/papers/C16.pdf},
Year = 2005,
}
@inproceedings{C17,
Author = {Christoph Benzm{\"u}ller and Chad Brown},
Booktitle = {Theorem Proving in Higher Order Logics, 18th
International Conference, TPHOLs 2005, Oxford, UK,
August 22-25, 2005, Proceedings},
Doi = {10.1007/11541868_5},
Editor = {Joe Hurd and Thomas F. Melham},
Keywords = {own, Higher Order Logic, Automated Reasoning, Henkin
Semantics},
Number = 3603,
Pages = {66-81},
Publisher = {Springer},
Series = {LNCS},
Title = {A Structured Set of Higher-Order Problems},
url = {http://christoph-benzmueller.de/papers/C17.pdf},
Year = 2005,
}
@inproceedings{C18,
Author = {Christoph Benzm{\"u}ller and Bao Quoc Vo},
Booktitle = {Proceedings, The Twentieth National Conference on
Artificial Intelligence and the Seventeenth
Innovative Applications of Artificial Intelligence
Conference, July 9-13, 2005, Pittsburgh,
Pennsylvania, USA},
Comment = {slides},
Editor = {Manuela Veloso and Subbarao Kambhampati},
Keywords = {own, DIALOG, Proof Presentation, Natural Language
Dialog, Proof Assistants, Tutoring Systems},
Pages = {516-522},
Publisher = {AAAI Press / The MIT Press},
Title = {Mathematical Domain Reasoning Tasks in Natural
Language Tutorial Dialog on Proofs},
url = {http://christoph-benzmueller.de/papers/C18.pdf},
Year = 2005,
}
@inproceedings{C19,
Author = {Serge Autexier and Christoph Benzm{\"u}ller and
Dominik Dietrich and Andreas Meier and Claus-Peter
Wirth},
Booktitle = {Mathematical Knowledge Management, 4th International
Conference, MKM 2005, Bremen, Germany, July 15-17,
2005, Revised Selected Papers},
Doi = {10.1007/11618027_9},
Editor = {Michael Kohlhase},
Keywords = {own, DIALOG, Proof Presentation, Proof Assistants,
OMEGA},
Pages = {126-142},
Publisher = {Springer},
Series = {LNCS},
Title = {A Generic Modular Data Structure for Proof Attempts
Alternating on Ideas and Granularity},
url = {http://christoph-benzmueller.de/papers/C19.pdf},
Volume = 3863,
Year = 2006,
}
@inproceedings{C2,
Abstract = {In this paper we present an extensional higher-order
resolution calculus that is complete relative to
Henkin model semantics. The treatment of the
extensionality principles -- necessary for the
completeness result -- by specialized
(goal-directed) inference rules is of practical
applicability, as an implentation of the calculus in
the LEO-System shows. Furthermore, we prove the
long-standing conjecture, that it is sufficient to
restrict the order of primitive substitutions to the
order of input formulae.},
Author = {Christoph Benzm{\"u}ller and Michael Kohlhase},
Booktitle = {Automated Deduction - CADE-15, 15th International
Conference on Automated Deduction, Lindau, Germany,
July 5-10, 1998, Proceedings},
Doi = {10.1007/BFb0054248},
Editor = {Claude Kirchner and H{\'e}l{\`e}ne Kirchner},
Keywords = {own, LEO Prover, Higher Order Logic, Automated
Reasoning, Henkin Semantics},
Number = 1421,
Pages = {56-71},
Publisher = {Springer},
Series = {LNAI},
Title = {Extensional Higher-Order Resolution},
url = {http://christoph-benzmueller.de/papers/C2.pdf},
Year = 1998,
}
@inproceedings{C20,
Address = {Genova, Italy},
Author = {Christoph Benzm{\"u}ller and Helmut Horacek and
Henri Lesourd and Ivana Kruijff-Korbayova and Marvin
Schiller and Magdalena Wolska},
Booktitle = {Proceedings of International Conference on Language
Resources and Evaluation (LREC 2006)},
Keywords = {own, DIALOG, Proof Presentation, Natural Language
Dialog, Tutoring Systems},
Publisher = {ELDA},
Title = {A corpus of tutorial dialogs on theorem proving; the
influence of the presentation of the study-material},
url = {http://christoph-benzmueller.de/papers/C20.pdf},
Year = 2006,
}
@inproceedings{C22,
Author = {Mark Buckley and Christoph Benzm{\"u}ller},
Booktitle = {Perspectives of Systems Informatics, 6th
International Andrei Ershov Memorial Conference, PSI
2006, Novosibirsk, Russia, June 27-30, 2006. Revised
Papers},
Doi = {10.1007/978-3-540-70881-0_14},
Editor = {Irina Virbitskaite and Andrei Voronkov},
Isbn = {978-3-540-70880-3},
Keywords = {own, DIALOG, Proof Presentation, Natural Language
Dialog, Proof Assistants, Agents, System
Integration},
Pages = {135-147},
Publisher = {Springer},
Series = {LNCS},
Title = {An Agent-based Architecture for Dialogue Systems},
url = {http://christoph-benzmueller.de/papers/C21.pdf},
Volume = 4378,
Year = 2007,
}
@inproceedings{C23,
Author = {Christoph Benzm{\"u}ller and Helmut Horacek and
Henri Lesourd and Ivana Kruijff-Korbayova and Marvin
Schiller and Magdalena Wolska},
Booktitle = {KI 2006: Advances in Artificial Intelligence, 29th
Annual German Conference on AI, KI 2006, Bremen,
Germany, June 14-17, 2006, Proceedings},
Doi = {10.1007/978-3-540-69912-5_13},
Editor = {Freksa, Christian and Kohlhase, Michael and Schill,
Kerstin},
Keywords = {own, DIALOG, Proof Presentation, Natural Language
Dialog, Tutoring Systems},
Pages = {159-173},
Publisher = {Springer},
Series = {LNCS},
Title = {{DiaWOz-II} - A Tool for Wizard-of-Oz Experiments in
Mathematics},
url = {http://christoph-benzmueller.de/papers/C22.pdf},
Volume = 4314,
Year = 2007,
}
@inproceedings{C21,
Author = {Christoph Benzm{\"u}ller and Chad Brown and Michael
Kohlhase},
Booktitle = {Automated Reasoning, Third International Joint
Conference, IJCAR 2006, Seattle, WA, USA, August
17-20, 2006, Proceedings},
Comment = {slides},
Doi = {10.1007/11814771_20},
Editor = {Ulrich Furbach and Natarajan Shankar},
Keywords = {own, Higher Order Logic, Henkin Semantics,
Cut-Elimination},
Pages = {220-234},
Publisher = {Springer},
Series = {LNCS},
Title = {Cut-Simulation in Impredicate Logics},
url = {http://christoph-benzmueller.de/papers/C23.pdf},
Volume = 4130,
Year = 2006,
}
@inproceedings{C24,
Author = {Christoph Benzm{\"u}ller and Dominik Dietrich and
Marvin Schiller and Serge Autexier},
Booktitle = {KI 2007: Advances in Artificial Intelligence, 30th
Annual German Conference on AI, KI 2007,
Osnabr{\"u}ck, Germany, September 10-13, 2007,
Proceedings},
Doi = {10.1007/978-3-540-74565-5_34},
Editor = {Joachim Hertzberg and Michael Beetz and Roman
Englert},
Keywords = {own, Proof Assistants, OMEGA, Tutoring Systems, Deep
Inference},
Pages = {435-439},
Publisher = {Springer},
Title = {Deep Inference for Automated Proof Tutoring?},
url = {http://christoph-benzmueller.de/papers/C24.pdf},
Volume = 4667,
Year = 2007,
}
@inproceedings{C25,
Author = {Christoph Benzm{\"u}ller and Florian Rabe and Geoff
Sutcliffe},
Booktitle = {Automated Reasoning, 4th International Joint
Conference, IJCAR 2008, Sydney, Australia, August
12-15, 2008, Proceedings},
Doi = {10.1007/978-3-540-71070-7_41},
Editor = {Alessandro Armando and Peter Baumgartner and Gilles
Dowek},
Keywords = {own, Higher Order Logic, Henkin Semantics, Automated
Reasoning},
Pages = {491-506},
Publisher = {Springer},
Series = {LNCS},
Title = {{THF0} -- The Core of the {TPTP} Language for
Classical Higher-Order Logic},
url = {http://christoph-benzmueller.de/papers/C25.pdf},
Volume = 5195,
Year = 2008,
}
@inproceedings{C26,
Author = {Christoph Benzm{\"u}ller and Frank Theiss and
Paulson, Lawrence C. and Arnaud Fietzke},
Booktitle = {Automated Reasoning, 4th International Joint
Conference, IJCAR 2008, Sydney, Australia, August
12-15, 2008, Proceedings},
Comment = {slides},
Doi = {10.1007/978-3-540-71070-7_14},
Editor = {Alessandro Armando and Peter Baumgartner and Gilles
Dowek},
Keywords = {own, LEO Prover, Higher Order Logic, Automated
Reasoning, Henkin Semantics},
Pages = {162-170},
Publisher = {Springer},
Series = {LNCS},
Title = {{LEO-II} - A Cooperative Automatic Theorem Prover
for Higher-Order Logic (System Description)},
url = {http://christoph-benzmueller.de/papers/C26.pdf},
Volume = 5195,
Year = 2008,
}
@inproceedings{C27,
Author = {Christoph Benzm{\"u}ller},
Booktitle = {Emerging Challenges for Security, Privacy and Trust,
24th IFIP TC 11 International Information Security
Conference, SEC 2009, Pafos, Cyprus, May 18-20,
2009. Proceedings},
Comment = {slides},
Doi = {10.1007/978-3-642-01244-0_34},
Editor = {Dimitris Gritzalis and Javier L{\'o}pez},
Isbn = {978-3-642-01243-3},
Keywords = {own, LEO Prover, Higher Order Logic, Automated
Reasoning, Henkin Semantics, Security Logics},
Pages = {387-398},
Publisher = {Springer},
Series = {IFIP},
Title = {Automating Access Control Logic in Simple Type
Theory with {LEO-II}},
url = {http://christoph-benzmueller.de/papers/C27.pdf},
Volume = 297,
Year = 2009,
}
@inproceedings{C28,
Author = {Marvin Schiller and Christoph Benzm{\"u}ller},
Booktitle = {CSEDU 2009 - Proceedings of the First International
Conference on Computer Supported Education, Lisboa,
Portugal, March 23-26, 2009 - Volume 1},
Doi = {10.5220/0002159603500354},
Editor = {Jos{\'e} A. Moinhos Cordeiro and Boris Shishkov and
Alexander Verbraeck and Markus Helfert},
Isbn = {978-989-8111-82-1},
Keywords = {own, Proof Presentation, DIALOG, Natural Language
Dialog, Proof Assistants, Machine Learning, Tutoring
Systems},
Pages = {350-354},
Publisher = {SciTePress Digital Library},
Title = {Proof Granularity as an Empirical Problem?},
url = {http://christoph-benzmueller.de/papers/C28.pdf},
Year = 2009,
}
@inproceedings{C29,
Author = {Geoff Sutcliffe and Christoph Benzm{\"u}ller and
Chad Brown and Frank Theiss},
Booktitle = {Automated Deduction - CADE-22, 22nd International
Conference on Automated Deduction, Montreal, Canada,
August 2-7, 2009. Proceedings},
Doi = {10.1007/978-3-642-02959-2_8},
Editor = {Renate Schmidt},
Isbn = {978-3-642-02958-5},
Keywords = {own, Higher Order Logic, Automated Reasoning},
Pages = {116-130},
Publisher = {Springer},
Series = {LNCS},
Title = {Progress in the Development of Automated Theorem
Proving for Higher-order Logic},
url = {http://christoph-benzmueller.de/papers/C29.pdf},
Volume = 5663,
Year = 2009,
}
@inproceedings{C3,
Abstract = {In this paper we discuss the Higher-Order Theorem
Prover LEO, which is based on the Extensional
Higher-Order Resolution Calculus EXTRES.},
Author = {Christoph Benzm{\"u}ller and Michael Kohlhase},
Booktitle = {Automated Deduction - CADE-15, 15th International
Conference on Automated Deduction, Lindau, Germany,
July 5-10, 1998, Proceedings},
Comment = {slides},
Doi = {10.1007/BFb0054256},
Editor = {Claude Kirchner and H{\'e}l{\`e}ne Kirchner},
Keywords = {own, LEO Prover, Higher Order Logic, Automated
Reasoning, Henkin Semantics},
Number = 1421,
Pages = {139-143},
Publisher = {Springer},
Series = {LNCS},
Title = {{LEO} -- A Higher-Order Theorem Prover},
url = {http://christoph-benzmueller.de/papers/C3.pdf},
Year = 1998,
}
@inproceedings{C30,
Author = {Marvin Schiller and Christoph Benzm{\"u}ller},
Booktitle = {Artificial Intelligence in Education: Building
Learning Systems that Care: From Knowledge
Representation to Affective Modelling, Proceedings
of the 14th International Conference on Artificial
Intelligence in Education, AIED 2009, July 6-10,
2009, Brighton, UK},
Isbn = {978-1-60750-028-5},
Keywords = {own, Proof Presentation, DIALOG, Natural Language
Dialog, Proof Assistants, Machine Learning, Tutoring
Systems},
Pages = {599-601},
Publisher = {IOS Press},
Series = {Frontiers in Artificial Intelligence and
Applications},
Title = {Granularity-Adaptive Proof Presentation},
url = {http://christoph-benzmueller.de/papers/C30.pdf},
Volume = 200,
Year = 2009,
}
@inproceedings{C31,
Address = {Paderborn, Germany},
Author = {Marvin Schiller and Christoph Benzm{\"u}ller},
Booktitle = {KI 2009: Advances in Artificial Intelligence, 32nd
Annual German Conference on AI, Paderborn, Germany,
September 15-18, 2009. Proceedings},
Doi = {10.1007/978-3-642-04617-9_37},
Editor = {B{\"a}rbel Mertsching and Marcus Hund and Muhammad
Zaheer Aziz},
Isbn = {978-3-642-04616-2},
Keywords = {own, Proof Presentation, DIALOG, Natural Language
Dialog, Proof Assistants, Machine Learning, Tutoring
Systems},
Pages = {289-297},
Publisher = {Springer},
Series = {LNAI},
Title = {Presenting Proofs with Adapted Granularity},
url = {http://christoph-benzmueller.de/papers/C31.pdf},
Volume = 5803,
Year = 2009,
}
@inproceedings{C32,
Address = {Lisbon, Portugal},
Author = {Christoph Benzm{\"u}ller},
Booktitle = {Contest paper at the World Congress and School on
Universal Logic III (UNILOG)},
Comment = {slides},
Keywords = {own, Higher Order Logic, LEO Prover, Modal Logics,
Combinations of Logics, Semantic Embedding},
Note = {The conference had no published proceedings for the
contest papers; the paper is available as
arXiv:1004.5500v1},
Title = {Simple Type Theory as Framework for Combining
Logics},
OPTurl = {http://arxiv.org/abs/1004.5500},
doi = {10.48550/ARXIV.1004.5500},
Year = 2010,
}
@inproceedings{C33,
Address = {Guangzhou (Canton), China},
Author = {Christoph Benzm{\"u}ller and Valerio Genovese},
Booktitle = {The International Conference on Non-classical Modal
and Predicate Logics (NCMPL)},
Comment = {[slides], [movie]},
Keywords = {own, Higher Order Logic, Semantic Embedding,
Conditional Logics, Automated Reasoning},
Note = {(The conference had no published proceedings; the
paper is available as arXiv:1204.5920v1; superseded
by IJCAI-2013 paper)},
Title = {Quantified Conditional Logics are Fragments of
{HOL}},
OPTurl = {http://arxiv.org/abs/1204.5920},
doi = {10.48550/ARXIV.1204.5920},
Year = 2011,
}
@inproceedings{C34,
Address = {Montpellier, France},
Author = {Christoph Benzm{\"u}ller and Jens Otten and Thomas
Raths},
Booktitle = {ECAI 2012},
Comment = {slides},
Doi = {10.3233/978-1-61499-098-7-163},
Editor = {Luc De Raedt and Christian Bessiere and Didier
Dubois and Patrick Doherty and Paolo Frasconi and
Fredrik Heintz and Peter Lucas},
Isbn = {978-1-61499-097-0},
Keywords = {own, Higher Order Logic, Semantic Embedding, Modal
Logics, Automated Reasoning},
Pages = {163-168},
Publisher = {IOS Press},
Series = {Frontiers in Artificial Intelligence and
Applications},
Title = {Implementing and Evaluating Provers for First-order
Modal Logics},
url = {http://christoph-benzmueller.de/papers/C34.pdf},
Volume = 242,
Year = 2012,
}
@inproceedings{C35,
Address = {Barcelona, Spain},
Author = {Christoph Benzm{\"u}ller},
Booktitle = {Proc. of the 5th International Conference on Agents
and Artificial Intelligence (ICAART)},
Comment = {slides},
Doi = {10.5220/0004324803460351},
Editor = {Joaquim Filipe and Ana Fred},
Keywords = {own, Higher Order Logic, Semantic Embedding, Modal
Logics, Combinations of Logics},
Pages = {346-351},
Publisher = {SCITEPRESS -- Science and Technology Publications,
Lda},
Title = {A Top-down Approach to Combining Logics},
url = {http://christoph-benzmueller.de/papers/C35.pdf},
Volume = 1,
Year = 2013,
}
@inproceedings{C36,
Address = {Rio de Janeiro, Brazil},
Author = {Christoph Benzm{\"u}ller},
Booktitle = {Handbook of the 4th World Congress and School on
Universal Logic},
Comment = {slides},
Editor = {J.Y. Beziau and A. Buchsbaum and A. Costa-Leite and
A. Altair},
Isbn = {978-85-400-0682-9},
Keywords = {own, Higher Order Logic, LEO Prover, Semantic
Embedding, Modal Logics, Combinations of Logics},
Note = {(Superseded by ICAART-2013 paper)},
Pages = {232-233},
Title = {{HOL} based Universal Reasoning},
url = {http://christoph-benzmueller.de/papers/C36.pdf},
Year = 2013,
}
@inproceedings{C4,
Abstract = {The acceptance and usability of current interactive
theorem proving environments is, among other things,
strongly influenced by the availability of an
intelligent default suggestion mechanism for
commands. Such mechanisms support the user by
decreasing the necessary interactions during the
proof construction. Although many systems offer such
facilities, they are often limited in their
functionality. In this paper we present a new
agent-based mechanism that independently observes
the proof state, steadily computes suggestions on
how to further construct the proof, and communicates
these suggestions to the user via a graphical user
interface. We furthermore introduce a focus
technique in order to restrict the search space when
deriving default suggestions. Although the agents we
discuss in this paper are rather simple from a
computational viewpoint, we indicate how the
presented approach can be extended in order to
increase its deductive power.},
Author = {Christoph Benzm{\"u}ller and Volker Sorge},
Booktitle = {Artificial Intelligence: Methodology, Systems, and
Applications, 8th International Conference, AIMSA
'98, Sozopol, Bulgaria, September 21-13, 1998,
Proceedings},
Doi = {10.1007/BFb0057438},
Editor = {Fausto Giunchiglia},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
System Integration, Agents},
Number = 1480,
Pages = {102-114},
Publisher = {Springer},
Series = {LNCS},
Title = {A Blackboard Architecture for Guiding Interactive
Proofs},
url = {http://christoph-benzmueller.de/papers/C4.pdf},
Year = 1998,
}
@inproceedings{C5,
Abstract = {This paper presents two approaches to primitive
equality treatment in higher-order (HO) automated
theorem proving: a calculus $\EXTPARA$ adapting
traditional first-order (FO)
paramodulation~\cite{RoWo69} , and a calculus
$\EXTRUE$ adapting FO
RUE-Resolution~\cite{Digricoli79} to HO logic (based
on Church's simply typed
$\lambda$-calculus). $\EXTPARA$ and $\EXTRUE$ extend
the extensional HO resolution approach
$\EXTRES$~\cite{BenKoh:ehor98}. In order to reach
Henkin completeness without the need for additional
extensionality axioms both calculi employ new,
positive extensionality rules analogously to the
respective negative ones provided by $\EXTRES$ that
operate on unification constraints. As the
extensionality rules have an intrinsic and
unavoidable difference-reducing character the HO
paramodulation approach looses its pure
term-rewriting character. On the other hand examples
demonstrate that the extensionality rules harmonise
rather well with the difference-reducing HO
RUE-resolution idea.},
Author = {Christoph Benzm{\"u}ller},
Booktitle = {Automated Deduction - CADE-16, 16th International
Conference on Automated Deduction, Trento, Italy,
July 7-10, 1999, Proceedings},
Comment = {slides},
Doi = {10.1007/3-540-48660-7_39},
Editor = {Harald Ganzinger},
Number = 1632,
Pages = {399-413},
Publisher = {Springer},
Series = {LNCS},
Title = {Extensional Higher-Order Paramodulation and
{RUE}-Resolution},
url = {http://christoph-benzmueller.de/papers/C5.pdf},
Year = 1999,
}
@inproceedings{C6,
Abstract = {We introduce a resource adaptive agent mechanism
which supports the user in interactive theorem
proving. The mechanism, an extension
of~\cite{BeSo98b}, uses a two layered architecture
of agent societies to suggest appropriate commands
together with possible command argument
instantiations. Experiments with this approach show
that its effectiveness can be further improved by
introducing a resource concept. In this paper we
provide an abstract view on the overall mechanism,
motivate the necessity of an appropriate resource
concept and discuss its realization within the agent
architecture.},
Author = {Christoph Benzm{\"u}ller and Volker Sorge},
Booktitle = {Progress in Artificial Intelligence, 9th Portuguese
Conference on Artificial Intelligence, EPIA '99,
{\'E}vora, Portugal, September 21-24, 1999,
Proceedings},
Comment = {slides},
Doi = {10.1007/3-540-48159-1_15},
Editor = {Pedro Borahona and Jose J.~Alferes},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
System Integration, Agents, LEO Prover},
Number = 1695,
Pages = {208-221},
Publisher = {Springer},
Series = {LNCS},
Title = {Critical Agents Supporting Interactive Theorem
Proving},
url = {http://christoph-benzmueller.de/papers/C6.pdf},
Year = 1999,
}
@inproceedings{C7,
Author = {Christoph Benzm{\"u}ller and Mateja Jamnik and
Manfred Kerber and Volker Sorge},
Booktitle = {Symbolic Computation and Automated Reasoning},
Editor = {Manfred Kerber and Michael Kohlhase},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Automated Reasoning, System Integration, Agents, LEO
Prover},
Pages = {245-246},
Publisher = {A.K.Peters},
Title = {Resource Guided Concurrent Deduction},
url = {http://christoph-benzmueller.de/papers/C7.pdf},
Year = 2000,
}
@inproceedings{C9,
Abstract = {We present the O-ANTS theorem prover that is built
on top of an agent-based command suggestion
mechanism. The theorem prover inherits beneficial
properties from the underlying suggestion mechanism
such as run-time extendibility and resource
adaptability. Moreover, it supports the distributed
integration of external reasoning systems. We also
discuss how the implementation and modeling of a
calculus in our agent-based approach can be
investigated wrt. the inheritance of properties such
as completeness and soundness.},
Author = {Christoph Benzm{\"u}ller and Volker Sorge},
Booktitle = {Symbolic Computation and Automated Reasoning},
Comment = {slides},
Editor = {Manfred Kerber and Michael Kohlhase},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Automated Reasoning, System Integration, Agents, LEO
Prover},
Pages = {81-97},
Publisher = {A.K.Peters},
Title = {{OANTS} -- Combining Interactive and Automated
Theorem Proving},
url = {http://christoph-benzmueller.de/papers/C8.pdf},
Year = 2001,
}
@inproceedings{C8,
Abstract = {In this paper we propose how proof planning systems
can be extended by an automated learning
capability. The idea is that a proof planner would
be capable of learning new proof methods from well
chosen examples of proofs which use a similar
reasoning strategy to prove related theorems, and
this strategy could be characterised as a proof
method. We propose a representation framework for
methods, and a machine learning technique which can
learn methods using this representation
framework. The technique can be applied (amongst
other) to learn whether and when to call external
systems such as theorem provers or computer algebra
systems. This is work in progress, and we hope to
gain useful feedback from the CALCULEMUS community.},
Author = {Mateja Jamnik and Manfred Kerber and Christoph
Benzm{\"u}ller},
Booktitle = {Symbolic Computation and Automated Reasoning},
Editor = {Manfred Kerber and Michael Kohlhase},
Keywords = {own, CALCULEMUS, Symb. Computation and
Symb. Reasoning, Proof Planning, Machine Learning},
Pages = {142-159},
Publisher = {A.K.Peters},
Title = {Towards Learning New Methods in Proof Planning},
url = {http://christoph-benzmueller.de/papers/C9.pdf},
Year = 2000,
}
@proceedings{E1,
Abstract = {This report contains the descriptions of student
posters accepted for presentation at the Calculemus
Autumn School 2002 in Pisa.},
Editor = {J{\"u}rgen Zimmer and Christoph Benzm{\"u}ller},
Keywords = {own, CALCULEMUS, Symb. Computation and
Symb. Reasoning},
Note = {(115 pages)},
Number = {SR-02-06},
Pages = {1-116},
Publisher = {SEKI Publications (ISSN 1437-4447)},
Title = {{CALCULEMUS Autumn School 2002: Student Poster
Abstracts}},
url = {http://christoph-benzmueller.de/papers/E1.pdf},
Year = 2002,
doi = {10.22028/D291-42127},
}
@proceedings{E9,
Editor = {Benzm{\"u}ller, Christoph and Fischer, Bernd and
Sutcliffe, Geoff},
Issn = {ISSN 1613-0073},
Publisher = {CEUR-WS.org},
Series = {CEUR Workshop Proceedings},
Title = {Proceedings of the 6th International Workshop on the
Implementation of Logics},
Url = {http://ceur-ws.org/Vol-212/},
Volume = 212,
Year = 2006,
}
@book{E11,
Isbn = {978-1-904987-70-3},
Editor = {Christoph Benzm{\"u}ller and Chad Brown and J{\"o}rg
Siekmann and Richard Statman},
Pages = {1--460},
Publisher = {College Publications},
Series = {Studies in Logic, Mathematical Logic and
Foundations},
Title = {Reasoning in Simple Type Theory -- Festschrift in
Honor of {Peter B.~Andrews} on His 70th Birthday},
Url =
{http://www.collegepublications.co.uk/logic/mlf/?00010},
Year = 2008,
}
@proceedings{E12,
Editor = {Serge Autexier and Christoph Benzm{\"u}ller},
Pages = {1-106},
Publisher = {Elsevier},
Series = {Electronic Notes in Theoretical Computer Science},
Title = {Proceedings of the 8th International Workshop on
User Interfaces for Theorem Provers (UITP 2008),
Montr\'{e}al, Canada},
Url =
{http://www.sciencedirect.com/science/journal/15710661/226/},
Volume = 226,
Year = 2009,
}
@proceedings{E2,
Abstract = {This are the notes (Part I) of the courses presented
at the Calculemus Autumn School 2002 in Pisa.},
Editor = {Christoph Benzm{\"u}ller and Regine Endsuleit},
Keywords = {own, CALCULEMUS, Symb. Computation and
Symb. Reasoning},
Note = {(168 pages)},
Number = {SR-02-07},
Pages = {1-168},
Publisher = {SEKI Publications (ISSN 1437-4447)},
Title = {{CALCULEMUS Autumn School 2002: Course Notes (Part
I)}},
Type = {SEKI Report},
url = {http://christoph-benzmueller.de/papers/E2.pdf},
Year = 2002,
doi = {10.22028/D291-42126},
}
@proceedings{E3,
Abstract = {This are the notes (Part II) of the courses
presented at the Calculemus Autumn School 2002 in
Pisa.},
Editor = {Christoph Benzm{\"u}ller and Regine Endsuleit},
Keywords = {own, CALCULEMUS, Symb. Computation and
Symb. Reasoning},
Note = {(130 pages)},
Number = {SR-02-08},
Pages = {1-130},
Publisher = {SEKI Publications (ISSN 1437-4447)},
Title = {{CALCULEMUS Autumn School 2002: Course Notes (Part
II)}},
Type = {SEKI Report},
url = {http://christoph-benzmueller.de/papers/E3.pdf},
Year = 2002,
}
@proceedings{E4,
Abstract = {This are the notes (Part III) of the courses
presented at the Calculemus Autumn School 2002 in
Pisa.},
Editor = {Christoph Benzm{\"u}ller and Regine Endsuleit},
Keywords = {own, CALCULEMUS, Symb. Computation and
Symb. Reasoning},
Note = {121 pages},
Number = {SR-02-09},
Publisher = {SEKI Publications (ISSN 1437-4447)},
Title = {{CALCULEMUS Autumn School 2002: Course Notes (Part
III)}},
Type = {SEKI Report},
url = {http://christoph-benzmueller.de/papers/E4.pdf},
Year = 2002,
}
@proceedings{E5,
Editor = {Christoph Benzm{\"u}ller},
Keywords = {own, CALCULEMUS, Symb. Computation and
Symb. Reasoning},
Note = {135 pages},
Publisher = {SEKI Publications (ISSN 1437-4447)},
Title = {Systems for Integrated Computation and Deduction --
Interim Report of the {CALCULEMUS} {IHP} Network},
OPTurl =
{http://christoph-benzmueller.de/papers/MTR-report-long.pdf},
Year = 2003,
doi = {10.22028/D291-40445},
}
@proceedings{E6,
Editor = {Benzm{\"u}ller, Christoph and Windsteiger, Wolfgang},
Keywords = {own, CALCULEMUS, Symb. Computation and
Symb. Reasoning},
Note = {Proceedings of the first ``Workshop on
Computer-Supported Mathematical Theory Development''
held in the frame of IJCAR 2004 in Cork, Ireland,
July 5, 2004. ISBN 3-902276-04-5.},
Number = {04-14},
Organization = {RISC Institute, University of Linz},
Series = {RISC Report Series},
Title = {{Computer-Supported Mathematical Theory
Development}},
url = {http://christoph-benzmueller.de/papers/E6.pdf},
Year = 2004,
}
@proceedings{E8,
editor = {Christoph Benzm{\"u}ller},
Keywords = {own, CALCULEMUS, Symb. Computation and
Symb. Reasoning, Proof Assistants, History of Logic},
Publisher = {Journal of Applied Logic, Elsevier},
Title = {Special Issue on Assistance Systems for Mathematics},
Url = {https://www.sciencedirect.com/journal/journal-of-applied-logic/vol/4/issue/4},
Year = 2006,
}
@proceedings{E7,
Address = {Wexford Hotel, Montego Bay, Jamaica},
Booktitle = {Proceedings of the LPAR-05 Workshop: Empirically
Successfull Automated Reasoning in Higher-Order
Logic (ESHOL)},
Editor = {Christoph Benzm{\"u}ller and John Harrison and
Carsten Sch{\"u}rmann},
Keywords = {own, Higher Order Logic, Automated Reasoning},
Note = {arXiv:cs/0601042},
Title = {Proceedings of the LPAR-05 Workshop: Empirically
Successfull Automated Reasoning in Higher-Order
Logic (ESHOL)},
Url = {http://arxiv.org/abs/cs/0601042},
Year = 2005,
}
@proceedings{E10,
Booktitle = {User Interfaces for Theorem Provers, Proceedings of
UITP'06},
Editor = {Serge Autexier and Christoph Benzm{\"u}ller},
Issn = {1571-0661},
Keywords = {own, User Interface},
Number = 2,
Pages = {1-2},
Publisher = {Elsevier},
Series = {Electronic Notes in Theoretical Computer Science},
Title = {User Interfaces for Theorem Provers, Proceedings of
UITP'06},
Url =
{http://www.sciencedirect.com/science/journal/15710661/174/2},
Volume = 174,
Year = 2007,
}
@article{J1,
Abstract = {This paper reports on the integration of the
higher-order theorem proving environment TPS
[Andrews96] into the mathematical assistant OMEGA
[Omega97]. TPS can be called from OMEGA either as a
black box or as an interactive system. In black box
mode, the user has control over the parameters which
control proof search in TPS; in interactive mode,
all features of the TPS-system are available to the
user. If the subproblem which is passed to TPS
contains concepts defined in OMEGA's database of
mathematical theories, these definitions are not
instantiated but are also passed to TPS. Using a
special theory which contains proof tactics that
model the ND-calculus variant of TPS within OMEGA,
any complete or partial proof generated in TPS can
be translated one to one into an OMEGA proof
plan. Proof transformation is realised by proof plan
expansion in OMEGA's 3-dimensional proof data
structure, and remains transparent to the user.},
Author = {Christoph Benzm{\"u}ller and Matt Bishop and Volker
Sorge},
Doi = {10.3217/jucs-005-03-0188},
Journal = {Journal of Universal Computer Science},
Keywords = {own, Proof Assistants, OMEGA, Proof Transformation,
System Integration, Higher Order Logic},
Number = 3,
Pages = {188-207},
Title = {Integrating {TPS} and {OMEGA}},
url = {http://christoph-benzmueller.de/papers/J1.pdf},
Volume = 5,
Year = 1999,
}
@techreport{J10,
Author = {Serge Autexier and Christoph Benzm{\"u}ller and
Armin Fiedler and Henri Lesourd},
Journal = {Electronic Notes in Theoretical Computer Science},
Keywords = {own, DIALOG, Proof Presentation, User Interface,
Proof Assistants},
Note = {This paper was formally accepted for the UITP'05
post-proceedings in ENTCS; this volume did not
appear though.},
Institution = {Saarland University},
Title = {Integrating Proof Assistants as Reasoning and
Verification Tools into a Scientific WYSIWYG Editor},
url = {http://christoph-benzmueller.de/papers/J10.pdf},
Year = 2005,
}
@techreport{J11,
Author = {Mark Buckley and Christoph Benzm{\"u}ller},
Journal = {Electronic Notes in Theoretical Computer Science},
Keywords = {own, Natural Language Dialog, Agents, System
Integration},
Note = {This paper was formally accepted for the UITP'05
post-proceedings in ENTCS; this volume did not
appear though.},
Title = {System Description: A Dialog Manager supporting
Tutorial Natural Language Dialogue on Proofs},
Institution = {Saarland University},
url = {http://christoph-benzmueller.de/papers/J11.pdf},
Year = 2005,
}
@article{J12,
Author = {J{\"o}rg Siekmann and Christoph Benzm{\"u}ller and
Serge Autexier},
Doi = {10.1016/j.jal.2005.10.008},
Journal = {Journal of Applied Logic},
Publisher = {Elsevier},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Automated Reasoning, Proof Planning, System
Integration, Agents, ERIH PLUS},
Number = 4,
Pages = {533-559},
Title = {Computer Supported Mathematics with {OMEGA}},
url = {http://christoph-benzmueller.de/papers/J12.pdf},
Volume = 4,
Year = 2006,
}
@article{J13,
Author = {Christoph Benzm{\"u}ller},
Doi = {10.1016/j.jal.2005.10.001},
Journal = {Journal of Applied Logic},
Publisher = {Elsevier},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Automated Reasoning, System Integration,
Symb. Computation and Symb. Reasoning, ERIH PLUS},
Note = {(non-reviewed)},
Number = 4,
Pages = {359-365},
Title = {Editorial: Towards Computer Aided Mathematics},
url = {http://christoph-benzmueller.de/papers/J13.pdf},
Volume = 4,
Year = 2006,
}
@article{J14,
Author = {Marc Wagner and Serge Autexier and Christoph
Benzm{\"u}ller},
Doi = {10.1016/j.entcs.2006.09.024},
Issn = {1571-0661},
Journal = {Electronic Notes in Theoretical Computer Science},
Keywords = {own, Proof Assistants, Proof Presentation, OMEGA,
Interactive Proof, System Integration, Mathematical
Knowledge Management, User Interface},
Number = 2,
Pages = {87-107},
Title = {PLATO: A Mediator between Text-Editors and Proof
Assistance Systems},
url = {http://christoph-benzmueller.de/papers/J14.pdf},
Volume = 174,
Year = 2007,
}
@article{J15,
Author = {Serge Autexier and Christoph Benzm{\"u}ller},
Doi = {10.1016/j.entcs.2006.09.017},
Issn = {1571-0661},
Journal = {Electronic Notes in Theoretical Computer Science},
Keywords = {own, User Interface, Proof Assistants},
Number = 2,
Pages = {1-2},
Title = {Preface: Proceedings of the 7th Workshop on User
Interfaces for Theorem Provers ({UITP} 2006)},
url = {http://christoph-benzmueller.de/papers/J15.pdf},
Volume = 174,
Year = 2007,
}
@article{J16,
Author = {Christoph Benzm{\"u}ller and Volker Sorge and Mateja
Jamnik and Manfred Kerber},
Doi = {10.1016/j.jal.2007.06.003},
Journal = {Journal of Applied Logic},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Automated Reasoning, Agents, Higher Order Logic, LEO
Prover, System Integration, ERIH PLUS},
Number = 3,
Pages = {318-342},
Title = {Combined Reasoning by Automated Cooperation},
url = {http://christoph-benzmueller.de/papers/J16.pdf},
Volume = 6,
Year = 2008,
}
@article{J17,
Author = {Serge Autexier and Christoph Benzm{\"u}ller and
Dominik Dietrich and Marc Wagner},
Doi = {10.1007/s11786-008-0054-6},
Journal = {Mathematics in Computer Science},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Mathematical Knowledge Management, Proof Planning,
System Integration},
Number = 2,
Pages = {253-277},
Title = {Organisation, Transformation, and Propagation of
Mathematical Knowledge in {Omega}},
url = {http://christoph-benzmueller.de/papers/J17.pdf},
Volume = 2,
Year = 2008,
}
@article{J19,
Author = {Christoph Benzm{\"u}ller and Chad Brown and Michael
Kohlhase},
Doi = {10.2168/LMCS-5(1:6)2009},
Journal = {Logical Methods in Computer Science},
Keywords = {own, Higher Order Logic, Henkin Semantics,
Cut-Elimination},
Number = {1:6},
Pages = {1-21},
Title = {Cut-Simulation and Impredicativity},
url = {http://christoph-benzmueller.de/papers/J18.pdf},
Volume = 5,
Year = 2009,
}
@article{J18,
Author = {Marvin Schiller and Dominik Dietrich and Christoph
Benzm{\"u}ller},
Issn = {1589-7389},
Journal = {Teaching Mathematics and Computer Science},
Keywords = {own, Proof Presentation, DIALOG, Natural Language
Dialog, Proof Assistants, Machine Learning, Tutoring
Systems},
Number = 2,
Pages = {325-343},
Title = {Proof Step Analysis for Proof Tutoring -- A Learning
Approach to Granularity},
url = {http://christoph-benzmueller.de/papers/J19.pdf},
doi = {10.5485/TMCS.2008.0183},
Volume = 6,
Year = 2008,
doi = {10.5485/TMCS.2008.0183},
}
@article{J2,
Author = {J{\"o}rg Siekmann and Stephan Hess and Christoph
Benzm{\"u}ller and Lassaad Cheikhrouhou and Armin
Fiedler and Helmut Horacek and Michael Kohlhase and
Karsten Konrad and Andreas Meier and Erica Melis and
Martin Pollet and Volker Sorge},
Doi = {10.1007/s001650050053},
Journal = {Formal Aspects of Computing},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Proof Presentation, User Interface},
Number = 3,
Pages = {326-342},
Title = {{LOUI}: Lovely {OMEGA} User Interface},
url = {http://christoph-benzmueller.de/papers/J2.pdf},
Volume = 11,
Year = 1999,
}
@article{J20,
Author = {Serge Autexier and Christoph Benzm{\"u}ller},
Doi = {10.1016/j.entcs.2008.12.093},
Issn = {1571-0661},
Journal = {Electronic Notes in Theoretical Computer Science},
Keywords = {own, User Interface, Proof Presentation},
Number = 1,
Pages = {1-2},
Title = {Preface: Proceedings of the 8th Workshop on User
Interfaces for Theorem Provers ({UITP} 2008)},
url = {http://christoph-benzmueller.de/papers/J20.pdf},
Volume = 226,
Year = 2009,
}
@article{J21,
Author = {Christoph Benzm{\"u}ller and Paulson, Lawrence C.},
Doi = {10.1093/jigpal/jzp080},
Journal = {The Logic Journal of the IGPL},
Keywords = {own, Higher Order Logic, LEO Prover, Semantic
Embedding, Modal Logics, Combinations of Logics,
Henkin Semantics, ERIH PLUS},
Number = 6,
Pages = {881-892},
Title = {Multimodal and Intuitionistic Logics in Simple Type
Theory},
url = {http://christoph-benzmueller.de/papers/J21.pdf},
Volume = 18,
Year = 2010,
}
@article{J22,
Author = {Geoff Sutcliffe and Christoph Benzm{\"u}ller},
Issn = {1972-5787},
Journal = {Journal of Formalized Reasoning},
Keywords = {own, Higher Order Logic, Automated Reasoning, Henkin
Semantics},
Number = 1,
Pages = {1-27},
Title = {Automated Reasoning in Higher-Order Logic using the
{TPTP THF} Infrastructure},
url = {https://www.researchgate.net/publication/49595291},
OPTurl = {https://jfr.unibo.it/article/view/1710},
Volume = 3,
Year = 2010,
doi = {10.6092/issn.1972-5787/1710},
}
@article{J26,
Author = {Christoph Benzm{\"u}ller and Paulson, Lawrence C.},
Doi = {10.1007/s11787-012-0052-y},
Journal = {Logica Universalis (Special Issue on Multimodal
Logics)},
Keywords = {own, Higher Order Logic, Semantic Embedding, Modal
Logics, Henkin Semantics},
Number = 1,
Pages = {7-20},
Title = {Quantified Multimodal Logics in Simple Type Theory},
url = {https://www.researchgate.net/publication/221677897},
Volume = 7,
Year = 2013,
}
@article{J27,
Author = {Adam Pease and Christoph Benzm{\"u}ller},
Doi = {10.3233/AIC-120549},
Journal = {AI Communications (Special Issue on Intelligent
Engineering Techniques for Knowledge Bases)},
Keywords = {own, Ontology Reasoning, System Integration,
Automated Reasoning},
Number = 1,
Pages = {79-97},
Title = {Sigma: An Integrated Development Environment for
Formal Ontology},
url = {http://christoph-benzmueller.de/papers/J24.pdf},
Volume = 26,
Year = 2013,
}
@article{J23,
Author = {Christoph Benzm{\"u}ller},
Comment = {slides},
Doi = {10.1007/s10472-011-9249-7},
Journal = {Annals of Mathematics and Artificial Intelligence
(Special issue Computational Logics in Multi-agent
Systems (CLIMA XI))},
Keywords = {own, Higher Order Logic, Semantic Embedding, Modal
Logics, Henkin Semantics, Automated Reasoning},
Number = {1-2},
Pages = {103-128},
Title = {Combining and Automating Classical and Non-Classical
Logics in Classical Higher-Order Logic},
url = {http://christoph-benzmueller.de/papers/J25.pdf},
Volume = 62,
Year = 2011,
}
@article{J24,
Author = {Christoph Benzm{\"u}ller and Dov Gabbay and Valerio
Genovese and Daniele Rispoli},
Doi = {10.1007/s10472-012-9320-z},
Journal = {Annals of Mathematics and Artificial Intelligence},
Keywords = {own, Higher Order Logic, Semantic Embedding,
Conditional Logics, Automated Reasoning},
Number = {1-4},
Pages = {257-271},
Title = {Embedding and Automating Conditional Logics in
Classical Higher-Order Logic},
url = {http://christoph-benzmueller.de/papers/J26.pdf},
Volume = 66,
Year = 2012,
}
@article{J25,
Author = {Christoph Benzm{\"u}ller and Adam Pease},
Doi = {10.1016/j.websem.2011.11.008},
Journal = {Journal of Web Semantics (Special Issue on Reasoning
with context in the Semantic Web)},
Keywords = {own, Ontology Reasoning, Automated Reasoning, Higher
Order Logic, Modal Logics},
Pages = {104-117},
Title = {Higher-order Aspects and Context in {SUMO}},
url = {https://www.researchgate.net/publication/221677796},
Volume = {12-13},
Year = 2012,
}
@article{J3,
Author = {J{\"o}rg Siekmann and Helmut Horacek and Michael
Kohlhase and Christoph Benzm{\"u}ller and Lassaad
Cheikhrouhou and Detlef Fehrer and Armin Fiedler and
Stephan Hess and Karsten Konrad and Andreas Meier
and Erica Melis and Volker Sorge},
Issn = {1373-5411},
Journal = {International Journal of Computing Anticipatory
Systems (CASYS)},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Proof Presentation, User Interface},
Pages = {101-110},
Title = {An Interactive Proof Development Environment $+$ Anticipation = A Mathematical Assistant?},
url = {http://christoph-benzmueller.de/papers/J3.pdf},
Volume = 3,
Year = 1999,
}
@article{J4,
Abstract = {In this contribution we propose an agent
architecture for theorem proving which we intend to
investigate in depth in the future. The work
reported in this paper is in an early state, and by
no means finished. We present and discuss our
proposal in order to get feedback from the
Calculemus community.},
Author = {Christoph Benzm{\"u}ller and Mateja Jamnik and
Manfred Kerber and Volker Sorge},
Doi = {10.1016/S1571-0661(05)82522-8},
Journal = {Electronic Notes in Theoretical Computer Science,
Elsevier},
Keywords = {own, Agents, Proof Assistants, OMEGA, Automated
Reasoning, System Integration},
Number = 3,
Pages = {21-33},
Title = {Agent based Mathematical Reasoning},
url = {http://christoph-benzmueller.de/papers/J4.pdf},
Volume = 23,
Year = 1999,
}
@article{J5,
Abstract = {We investigate several approaches to resolution
based automated theorem proving in classical
higher-order logic (based on Church's simply typed
lambda calculus) and discuss their requirements with
respect to Henkin completeness and full
extensionality. In particular we focus on Andrews'
higher-order resolution [Andrews71], Huet's
constrained resolution [Huet72], higher-order
$E$-resolution, and extensional higher-order
resolution [BenzmuellerKohlhase98]. With the help of
examples we illustrate the parallels and differences
of the extensionality treatment of these approaches
and demonstrate that extensional higher-order
resolution is the sole approach that can completely
avoid additional extensionality axioms.},
Author = {Christoph Benzm{\"u}ller},
Doi = {10.1023/A:1020840027781},
Issn = {0039-7857},
Journal = {Synthese},
Keywords = {own, LEO Prover, Automated Reasoning, Higher Order
Logic, Henkin Semantics, ERIH PLUS, History of
Logic},
Number = {1-2},
Pages = {203-235},
Title = {Comparing Approaches to Resolution based
Higher-Order Theorem Proving},
url = {http://christoph-benzmueller.de/papers/J5.pdf},
Volume = 133,
Year = 2002,
}
@article{J7,
Author = {Christoph Benzm{\"u}ller and Chad Brown and Michael
Kohlhase},
Doi = {10.2178/jsl/1102022211},
Journal = {Journal of Symbolic Logic},
Keywords = {own, Higher Order Logic, Henkin Semantics,
Cut-Elimination, ERIH PLUS},
Number = 4,
Pages = {1027-1088},
Title = {Higher-Order Semantics and Extensionality},
url = {https://www.researchgate.net/publication/38338872},
Volume = 69,
Year = 2004,
}
@article{J6,
Author = {Mateja Jamnik and Manfred Kerber and Martin Pollet
and Christoph Benzm{\"u}ller},
Doi = {10.1093/jigpal/11.6.647},
Journal = {The Logic Journal of the IGPL},
Keywords = {own, Agents, Proof Assistants, Proof Planning,
System Integration, Machine Learning, ERIH PLUS},
Number = 6,
Pages = {647-674},
Title = {Automatic Learning of Proof Methods in Proof
Planning},
url = {http://christoph-benzmueller.de/papers/J7.pdf},
Volume = 11,
Year = 2003,
}
@article{J8,
Author = {Serge Autexier and Christoph Benzm{\"u}ller and
Armin Fiedler and Helmut Horacek and Bao Quoc Vo},
Doi = {10.1016/j.entcs.2003.12.026},
Journal = {Electronic Notes in Theoretical Computer Science},
Keywords = {own, Proof Assistants, Proof Planning, System
Integration, Proof Presentation, Proof
Transformation},
Pages = {5-23},
Title = {Assertion-level Proof Representation with
Under-Specification},
url = {http://christoph-benzmueller.de/papers/J8.pdf},
Volume = 93,
Year = 2004,
}
@article{J9,
Author = {Malte H\"ubner and Serge Autexier and Christoph
Benzm{\"u}ller and Andreas Meier},
Doi = {10.1016/j.entcs.2004.02.021},
Journal = {Electronic Notes in Theoretical Computer Science},
Keywords = {own, Agents, Proof Assistants, Proof Planning,
System Integration},
Number = {C},
Pages = {161-181},
Title = {Interactive Theorem Proving with Tasks},
url = {http://christoph-benzmueller.de/papers/J9.pdf},
Volume = 103,
Year = 2004,
}
@techreport{R1,
Author = {Serge Autexier and Christoph Benzm{\"u}ller and
Ramses A. Heckler},
Institution = {Saarland University, SEKI Publications (ISSN
1437-4447)},
Number = {WP 92/36},
Title = {{Das Fallbeispiel `UNIX' --- Dokumentation einer
UNIX-Filesystem-Spezifikation mit OWEB}},
url = {http://christoph-benzmueller.de/papers/R1.pdf},
Year = 1992,
}
@techreport{R10,
Author = {Christoph Benzm{\"u}ller and Mateja Jamnik and
Manfred Kerber and Volker Sorge},
Institution = {Saarland University, SEKI Publications (ISSN
1437-4447)},
Number = {SR-99-07},
Pages = {1-27},
Title = {Towards Concurrent Resource Guided Deduction},
Type = {SEKI Report},
url = {http://christoph-benzmueller.de/papers/R10.pdf},
Year = 1999,
}
@techreport{R11,
Author = {Christoph Benzm{\"u}ller},
Institution = {Saarland University, SEKI Publications (ISSN
1437-4447)},
Keywords = {own, Higher Order Logic, Henkin Semantics, LEO
Prover, Automated Reasoning},
Number = {SR-99-08},
Pages = {1-139},
Title = {Equality and Extensionality in Higher-Order Theorem
Proving},
Type = {SEKI Report},
url = {http://christoph-benzmueller.de/papers/R11.pdf},
Year = 1999,
}
@techreport{R12,
Author = {Christoph Benzm{\"u}ller and Volker Sorge and John
Byrnes},
Note = {Draft, AG Siekmann, Saarland University},
Pages = {1-5},
Title = {{OANTS} for Interactive {ATP}},
Institution = {Saarland University},
url = {http://christoph-benzmueller.de/papers/R12.pdf},
Year = 1999,
}
@techreport{R13,
Author = {Mateja Jamnik and Manfred Kerber and Christoph
Benzm{\"u}ller},
Institution = {University of Birmingham, School of Computer
Science},
Number = {CSRP-00-09},
Pages = {1-16},
Title = {Towards Learning new Methods in Proof Planning},
url = {http://christoph-benzmueller.de/papers/R13.pdf},
Year = 2000,
}
@techreport{R14,
Author = {Mateja Jamnik and Manfred Kerber and Christoph
Benzm{\"u}ller},
Institution = {University of Birmingham, School of Computer
Science},
Number = {CSRP-01-08},
Pages = {1-15},
Title = {Learning Method Outlines in Proof Planning},
url = {http://christoph-benzmueller.de/papers/R14.pdf},
Year = 2001,
}
@techreport{R17,
Author = {Christoph Benzm{\"u}ller and Armin Fiedler and
Andreas Meier and Martin Pollet},
Institution = {Saarland University, SEKI Publications (ISSN
1437-4447)},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Mathematical Knowledge Management, Proof Planning,
System Integration},
Number = {SR-02-03},
Pages = {1-103},
Title = {Irrationality of square root of 2 -- A case study in
{OMEGA}},
Type = {SEKI Report},
url = {http://christoph-benzmueller.de/papers/R15.pdf},
Year = 2002,
doi = {10.22028/D291-42121},
}
@techreport{R18,
Author = {Mateja Jamnik and Manfred Kerber and Martin Pollet
and Christoph Benzm{\"u}ller},
File = {/2002/CSRP-02-05.ps.gz},
Institution = {University of Birmingham, School of Computer
Science},
Number = {CSRP-02-05},
Pages = {1-34},
Title = {Automatic Learning of Proof Methods in Proof
Planning},
url = {http://christoph-benzmueller.de/papers/R16.pdf},
Year = 2002,
}
@techreport{R19,
Abstract = {We show that a prominent counterexample for the
completeness of first order RUE-resolution does not
apply to the higher order RUE-resolution approach
EXTRUE.},
Author = {Christoph Benzm{\"u}ller},
Institution = {Saarland University, SEKI Publications (ISSN
1437-4447)},
Note = {arXiv:0901.3608},
Number = {SR-02-05},
Pages = {1-5},
Title = {A remark on higher order {RUE}-resolution with
{EXTRUE}},
Type = {SEKI Report},
OPTurl = {http://arxiv.org/abs/0901.3608},
doi = {10.48550/ARXIV.0901.3608},
Year = 2002,
}
@techreport{R20,
Abstract = {In this paper we re-examine the semantics of
classical higher order logic with the purpose of
clarifying the role of extensionality. To reach this
goal, we distinguish nine classes of higher order
models with respect to various combinations of
Boolean extensionality and three forms of functional
extensionality. Furthermore, we develop a
methodology of abstract consistency methods (by
providing the necessary model existence theorems)
needed to analyze completeness of (machine-oriented)
higher order calculi with respect to these model
classes.},
Author = {Christoph Benzm{\"u}ller and Chad Brown and Michael
Kohlhase},
Institution = {Carnegie Mellon University, Pittsburgh, PA},
Keywords = {own, Higher Order Logic, Henkin Semantics, LEO
Prover, Automated Reasoning},
Number = {CMU-01-03},
Pages = {1-74},
Title = {Higher Order Semantics and Extensionality},
url = {http://christoph-benzmueller.de/papers/R18.pdf},
Year = 2003,
}
@techreport{R21,
Abstract = {In this report we present a variety of model
existence theorems for classical higher-order
logics. The extend the well-known abstract
consistency methods to higher-order logics and
pinpoint the contribution of extensionality. The
results reported here weaken the saturation
precondition needed in earlier model existence
theorems, making them appliccable to cut-free
higher-order logics.},
Author = {Christoph Benzm{\"u}ller and Chad Brown and Michael
Kohlhase},
Institution = {Saarland University, Saarbr{\"u}cken, Germany and
Carnegie Mellon University, Pittsburgh, USA},
Keywords = {own, Higher Order Logic, Henkin Semantics, LEO
Prover, Automated Reasoning, Cut-Elimination,R37},
Title = {Semantic Techniques for Cut-Elimination in Higher
Order Logic.},
url = {http://christoph-benzmueller.de/papers/R19.pdf},
Year = 2003,
}
@techreport{R2,
Annote = {KORSO, Heck III, siehe Ben93},
Author = {Christoph Benzm{\"u}ller},
Institution = {Saarland University, SEKI Publications (ISSN
1437-4447)},
Number = {A/06/93},
Pages = {1-59},
Title = {{HDMS--A und OBSCURE in KORSO--- Die Funktionale
Essenz von HDMS--A aus Sicht der algorithmischen
Spezifikationsmethode --- TEIL 3: Spezifikation der
atomaren Funktionen}},
url = {http://christoph-benzmueller.de/papers/R2.pdf},
Year = 1993,
doi = {10.22028/D291-25819},
}
@techreport{R22,
Abstract = {In this paper we address assertion retrieval and
application in theorem proving systems or proof
planning systems for classical first-order
logic. Due to Huang the notion of assertion
comprises mathematical knowledge from a mathematical
knowledge base KB such as definitions, theorems, and
axioms. the prover during proof construction. We
propose a distributed mediator module between KB and
a theorem proving system S which is independent of
the particular proof representation format of S and
which applies generalized resolution in order to
analyze the logical consequences of arbitrary
assertions for a proof context at hand. Our approach
is applicable without any extension also to the
assumptions that are dynamically created during a
proof search process. It therefore realizes a
crucial first step towards full automation of
assertion level reasoning. We discuss the benefits
and connection of our approach to proof planning and
motivate an application in a project aiming at a
tutorial dialogue system for mathematics.},
Author = {Bao Quoc Vo and Christoph Benzm{\"u}ller and Serge
Autexier},
Institution = {Saarland University, SEKI Publications (ISSN
1437-4447)},
Number = {SR-03-01},
Publisher = {SEKI Publications (ISSN 1437-4447)},
Title = {An Approach to Assertion Application via Generalized
Resolution},
Type = {SEKI Report},
url = {http://christoph-benzmueller.de/papers/R20.pdf},
Year = 2003,
doi = {10.22028/D291-40439},
}
@techreport{R23,
Abstract = {Research on automated and interactive theorem
proving aims at the mechanization of logical
reasoning. Aside from the development of logic
calculi it became rapidly apparent that the
organization of proof search on top of the calculi
is an essential task in the design of powerful
theorem proving systems. Different paradigms of how
to organize proof search have emerged in that area
of research, the most prominent representatives are
generally described by the buzzwords: automated
theorem proving, tactical theorem proving and proof
planning. Despite their paradigmatic differences,
all approaches share a common goal: to find a proof
for a given conjecture. In this paper we start with
a rational reconstruction of proof search paradigms
in the area of proof planning and tactical theorem
proving. Guided by similarities between software
engineering and proof construction we develop a
uniform view that accommodates the various proof
search methodologies and eases their
comparison. Based on this view, we propose a unified
framework that enables the combination of different
methodologies for proof construction to take
advantage of their individual virtues within
specific phases of a proof construction.},
Author = {Serge Autexier and Christoph Benzm{\"u}ller and
Dieter Hutter},
Institution = {Saarland University, SEKI Publications (ISSN
1437-4447)},
Number = {SR-03-02},
Publisher = {SEKI Publications (ISSN 1437-4447)},
Title = {Towards a Framework to Integrate Proof Search
Paradigms},
Type = {SEKI Report},
url = {http://christoph-benzmueller.de/papers/R21.pdf},
Year = 2003,
doi = {10.22028/D291-40440},
}
@book{R24,
Editor = {Christoph Benzm{\"u}ller and Corinna Hahn},
Keywords = {own, CALCULEMUS, Symb. Computation and
Symb. Reasoning},
Note = {EU Report, Saarland University, Saarbr{\"u}cken,
Germany},
Publisher = {Saarland University, Germany},
Title = {The CALCULEMUS Midterm Report},
url = {http://christoph-benzmueller.de/papers/R22.pdf},
Year = 2003,
}
@techreport{R25,
Author = {Christoph Benzm{\"u}ller},
Note = {Project proposal in the DFG Aktionsplan Informatik},
Pages = {1-43},
Title = {ALONZO: Deduktionsagenten h{\"o}herer Ordnung
f{\"u}r Mathematische Assistenzsysteme},
url = {http://christoph-benzmueller.de/papers/R23.pdf},
Year = 2003,
}
@book{R26,
Author = {Christoph Benzm{\"u}ller and Dieter Hutter},
Keywords = {own, CALCULEMUS, Symb. Computation and
Symb. Reasoning},
Note = {Project proposal for a Marie Curie Research Training
Network within the EU 6th framework; 73 pages},
Pages = {1-73},
Publisher = {Saarland University, Germany},
Title = {{CALCULEMUS-II}: Computer-supported Mathematical
Knowledge Evolution},
url = {http://christoph-benzmueller.de/papers/R24.pdf},
Year = 2003,
}
@techreport{R15,
Author = {Manfred Pinkal and J{\"o}rg Siekmann and Christoph
Benzm{\"u}ller},
Keywords = {own, DIALOG, Proof Presentation, Natural Language
Dialog, Proof Assistants, Tutoring Systems},
Note = {Project proposal in the Collaborative Research
Centre SFB 378 on Resource-adaptive Cognitive
Processes},
Pages = {1-34},
Title = {DIALOG: Tutorieller Dialog mit einem Mathematik
Assistenzsystem},
url = {http://christoph-benzmueller.de/papers/R25.pdf},
Year = 2001,
}
@techreport{R16,
Author = {J{\"o}rg Siekmann and Christoph Benzm{\"u}ller and
Erica Melis},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Mathematical Knowledge Management, Proof Planning,
System Integration},
Note = {Project proposal in the Collaborative Research
Centre SFB 378 on Resource-adaptive Cognitive
Processes},
Pages = {1-30},
Title = {{OMEGA: Ressourcenadaptive Beweisplanung}},
url = {http://christoph-benzmueller.de/papers/R25.pdf},
Year = 2001,
}
@techreport{R27,
Author = {Christoph Benzm{\"u}ller},
Note = {EURYI project proposal},
Pages = {1-37},
Title = {ALONZO: Higher-Order Reasoning Agents for
Mathematics},
url = {http://christoph-benzmueller.de/papers/R23.pdf},
Year = 2004,
}
@techreport{R28,
Author = {Manfred Pinkal and J{\"o}rg Siekmann and Christoph
Benzm{\"u}ller},
Keywords = {own, DIALOG, Proof Presentation, Natural Language
Dialog, Proof Assistants, Tutoring Systems},
Note = {Project report in the Collaborative Research Centre
SFB 378 on Resource-adaptive Cognitive Processes},
Pages = {1-24},
Title = {DIALOG: Tutorial Dialog with an Assistance System
for Mathematics},
url = {http://christoph-benzmueller.de/papers/R28.pdf},
Year = 2004,
}
@techreport{R29,
Author = {J{\"o}rg Siekmann and Christoph Benzm{\"u}ller and
Erica Melis},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Mathematical Knowledge Management, Proof Planning,
System Integration},
Note = {Project report in the Collaborative Research Centre
SFB 378 on Resource-adaptive Cognitive Processes},
Pages = {1-22},
Title = {{OMEGA: Resource-adaptive Proof Planning}},
url = {http://christoph-benzmueller.de/papers/R29.pdf},
Year = 2004,
}
@techreport{R3,
Author = {Christoph Benzm{\"u}ller},
Note = {Draft, AG Siekmann, Saarland University},
Pages = {1-26},
Title = {Proposal for my {PhD}-Study},
url = {http://christoph-benzmueller.de/papers/R3.pdf},
Year = 1995,
}
@techreport{R30,
Author = {Manfred Pinkal and J{\"o}rg Siekmann and Christoph
Benzm{\"u}ller and Ivana Kruijff-Korbayova},
Keywords = {own, DIALOG, Proof Presentation, Natural Language
Dialog, Proof Assistants, Tutoring Systems},
Note = {Project proposal in the Collaborative Research
Centre SFB 378 on Resource-adaptive Cognitive
Processes},
Pages = {1-31},
Title = {DIALOG: Natural Language-based Interaction with a
Mathematics Assistance System},
url = {http://christoph-benzmueller.de/papers/R30.pdf},
Year = 2004,
}
@techreport{R31,
Author = {J{\"o}rg Siekmann and Christoph Benzm{\"u}ller and
Serge Autexier},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Mathematical Knowledge Management, Proof Planning,
System Integration},
Note = {Project proposal in the Collaborative Research
Centre SFB 378 on Resource-adaptive Cognitive
Processes},
Pages = {1-26},
Title = {{OMEGA}: Agent-oriented Proof Planning},
url = {http://christoph-benzmueller.de/papers/R31.pdf},
Year = 2004,
}
@techreport{R32,
Author = {Christoph Benzm{\"u}ller},
Note = {DFG research grant proposal},
Pages = {1-29},
Title = {ALONZO: Higher-Order Reasoning Agents and Semantical
Mediation of Mathematical Knowledge},
url = {http://christoph-benzmueller.de/papers/R32.pdf},
Year = 2004,
}
@techreport{R33,
Author = {Serge Autexier and Christoph Benzm{\"u}ller and
Michael Kohlhase and J\"org Siekmann},
Note = {DFG research grant proposal},
Pages = {1-22},
Title = {VERMATH: Distributed Mathematical Problem Solving},
url = {http://christoph-benzmueller.de/papers/R33.pdf},
Year = 2004,
}
@techreport{R34,
Author = {Christoph Benzm{\"u}ller and Michael Kohlhase and
J{\"o}rg Siekmann},
Note = {DFG research grant report},
Pages = {1-14},
Title = {Abschlussbericht Projekt HOTEL},
url = {http://christoph-benzmueller.de/papers/R34.pdf},
Year = 2004,
}
@techreport{R35,
Author = {Mark Buckley and Christoph Benzm{\"u}ller},
Institution = {Saarland University, SEKI Publications (ISSN
1437-4447)},
Keywords = {own, DIALOG, Proof Presentation, Natural Language
Dialog, Proof Assistants, Agents, System
Integration},
Number = {SR-04-01},
Publisher = {SEKI Publications (ISSN 1437-4447)},
Title = {A Dialogue Manager for the DIALOG Demonstrator},
Type = {SEKI Report},
url = {http://christoph-benzmueller.de/papers/R35.pdf},
Year = 2004,
doi = {10.22028/D291-41449},
}
@book{R36,
Author = {Christoph Benzm{\"u}ller and Corinna Hahn},
Keywords = {own, CALCULEMUS, Symb. Computation and
Symb. Reasoning},
Note = {Final report of the Marie Curie Research Training
Network CALCULEMUS within the EU 5th framework},
Pages = {1-57},
Publisher = {Saarland University, Germany},
Title = {The CALCULEMUS Final Report},
url = {http://christoph-benzmueller.de/papers/R36.pdf},
Year = 2004,
}
@techreport{R37,
Author = {Christoph Benzm{\"u}ller and Chad Brown and Michael
Kohlhase},
Institution = {Saarland University, Saarbr{\"u}cken, Germany},
Number = {SR-2004-07},
Publisher = {SEKI Publications (ISSN 1437-4447)},
Title = {Semantic Techniques for Cut-Elimination in
Higher-Order Logics},
Type = {SEKI Report},
url = {http://christoph-benzmueller.de/papers/R37.pdf},
Year = 2004,
}
@techreport{R38,
Address = {Malaga, Spain},
Author = {Christoph Benzm{\"u}ller and Chad Brown},
Note = {Course Notes from the 18th European Summer School in
Logic, Language and Information (ESSLLI'06)},
Pages = {1-50},
Title = {Semantics of Higher-Order Logic},
url = {http://christoph-benzmueller.de/papers/R38.pdf},
Year = 2006,
}
@techreport{R39,
Author = {Christoph Benzm{\"u}ller and Chad Brown and Michael
Kohlhase},
Institution = {Saarland University, Saarbr{\"u}cken, Germany},
Number = {SR-2006-01},
Publisher = {SEKI Publications (ISSN 1437-4447)},
Title = {Cut-Simulation in Impredicative Logics (extended
version)},
Type = {SEKI Report},
url = {http://christoph-benzmueller.de/papers/R39.pdf},
Year = 2006,
}
@techreport{R4,
Author = {Christoph Benzm{\"u}ller},
Institution = {Department of Mathematical Sciences, Carnegie Mellon
University, Pittsburgh, USA},
Number = {97-198},
Pages = {1-28},
Title = {A Calculus and a System Architecture for Extensional
Higher-Order Resolution},
Type = {Research Report},
url = {http://christoph-benzmueller.de/papers/R4.pdf},
Year = 1997,
doi = {10.1184/R1/6476477.v1},
}
@techreport{R40,
Author = {J{\"o}rg Siekmann and Serge Autexier and Christoph
Benzm{\"u}ller},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Mathematical Knowledge Management, Proof Planning,
System Integration},
Note = {Project report in the Collaborative Research Centre
SFB 378 on Resource-adaptive Cognitive Processes},
Pages = {1-19},
Title = {{OMEGA}: Agent-oriented Proof Planning},
url = {http://christoph-benzmueller.de/papers/R40.pdf},
Year = 2008,
}
@techreport{R41,
Author = {Manfred Pinkal and J{\"o}rg Siekmann and Christoph
Benzm{\"u}ller and Ivana Kruijff-Korbayova},
Keywords = {own, DIALOG, Proof Presentation, Natural Language
Dialog, Proof Assistants, Machine Learning, Tutoring
Systems},
Note = {Project report in the Collaborative Research Centre
SFB 378 on Resource-adaptive Cognitive Processes},
Pages = {1-20},
Title = {DIALOG: Natural Language-based Interaction with a
Mathematics Assistance System},
url = {http://christoph-benzmueller.de/papers/R41.pdf},
Year = 2008,
}
@techreport{R42,
Abstract = {Garg and Abadi recently proved that prominent access
control logics can be translated in a sound and
complete way into modal logic S4. We have previously
outlined how normal multimodal logics, including
monomodal logics K and S4, can be embedded in simple
type theory and we have demonstrated that the
higher-order theorem prover LEO-II can automate
reasoning in and about them. In this paper we
combine these results and describe a sound embedding
of different access control logics in simple type
theory. Employing this framework we show that the
off the shelf theorem prover LEO-II can be applied
to automate reasoning in prominent access control
logics. },
Author = {Christoph Benzm{\"u}ller},
Institution = {Universit{\"a}t des Saarlandes},
Address = {Saarbr{\"u}cken, Germany},
Keywords = {own, LEO Prover, Higher Order Logic, Automated
Reasoning, Henkin Semantics, Security Logics},
Note = {arXiv:0901.3574},
Number = {SR-2008-01},
Publisher = {SEKI Publications (ISSN 1437-4447)},
Title = {Automating Access Control Logics in Simple Type
Theory with {LEO-II}},
Type = {SEKI Report},
OPTurl = {http://arxiv.org/abs/0901.3574},
Doi = {10.48550/arXiv.0901.3574},
Year = 2008,
}
@book{R43,
Abstract = {We give some lectures on the work on formal logic of
Jacques Herbrand, and sketch his life and his
influence on automated theorem proving. The intended
audience ranges from students interested in logic
over historians to logicians. Besides the well-known
correction of Herbrand's False Lemma by Goedel and
Dreben, we also present the hardly known unpublished
correction of Heijenoort and its consequences on
Herbrand's Modus Ponens Elimination. Besides
Herbrand's Fundamental Theorem and its relation to
the Loewenheim-Skolem-Theorem, we carefully
investigate Herbrand's notion of intuitionism in
connection with his notion of falsehood in an
infinite domain. We sketch Herbrand's two proofs of
the consistency of arithmetic and his notion of a
recursive function, and last but not least, present
the correct original text of his unification
algorithm with a new translation.},
Author = {Wirth, Claus-Peter and Siekmann, J{\"o}rg and
Benzm{\"u}ller, Christoph and Autexier, Serge},
Keywords = {own, Jacques Herbrand, History of Logic},
Note = {arXiv:0902.4682},
Publisher = {SEKI Publications (ISSN 1437-4447)},
Title = {Lectures on {Jacques Herbrand} as a Logician},
OPTurl = {http://arxiv.org/abs/0902.4682},
doi = {10.48550/ARXIV.0902.4682},
Year = 2009,
}
@techreport{R44,
Abstract = {When mathematicians present proofs they usually
adapt their explanations to their didactic goals and
to the (assumed) knowledge of their
addressees. Modern automated theorem provers, in
contrast, present proofs usually at a fixed level of
detail (also called granularity). Often these
presentations are neither intended nor suitable for
human use. A challenge therefore is to develop user-
and goal-adaptive proof presentation techniques that
obey common mathematical practice. We present a
flexible and adaptive approach to proof presentation
that exploits machine learning techniques to extract
a model of the specific granularity of proof
examples and employs this model for the automated
generation of further proofs at an adapted level of
granularity.},
Institution = {Saarland University},
Address = {{DFKI Bremen GmbH, Safe and Secure Cognitive
Systems, Cartesium, Enrique Schmidt Str.\,5,
D--28359 Bremen, Germany}},
Author = {Schiller, Marvin and Benzm{\"u}ller, Christoph},
Keywords = {own, Proof Presentation, DIALOG, Natural Language
Dialog, Proof Assistants, Machine Learning, Tutoring
Systems},
Note = {arXiv:0903.0314},
Publisher = {{SEKI Publications (ISSN 1437-4447)}},
Series = {{SEKI Working-Paper SWP--2009--01}},
Title = {Granularity-Adaptive Proof Presentation},
OPTurl = {http://arxiv.org/abs/0903.0314},
doi = {10.48550/ARXIV.0903.0314},
Year = 2009,
}
@techreport{R45,
Abstract = {We present a straightforward embedding of quantified
multimodal logic in simple type theory and prove its
soundness and completeness. Modal operators are
replaced by quantification over a type of possible
worlds. We present simple experiments, using
existing higher-order theorem provers, to
demonstrate that the embedding allows automated
proofs of statements in these logics, as well as
meta properties of them.},
Address = {{DFKI Bremen GmbH, Safe and Secure Cognitive
Systems, Cartesium, Enrique Schmidt Str.\,5,
D--28359 Bremen, Germany}},
Author = {Benzm{\"u}ller, Christoph and Paulson, Lawrence C.},
Note = {arXiv:0905.2435},
Institution = {Saarland University},
Publisher = {{SEKI Publications (ISSN 1437-4447)}},
Series = {{SEKI Report SR-2009-02 (ISSN 1437-4447)}},
Title = {Quantified Multimodal Logics in Simple Type Theory},
OPTurl = {http://arxiv.org/abs/0905.2435},
doi = {10.48550/arXiv.0905.2435},
Year = 2009,
}
@techreport{R46,
Address = {{DFKI Bremen GmbH, Safe and Secure Cognitive
Systems, Cartesium, Enrique Schmidt Str.\,5,
D--28359 Bremen, Germany}},
Author = {Benzm{\"u}ller, Christoph},
Note = {arXiv:0905.4369},
Institution = {Saarland University},
Publisher = {{SEKI Publications (ISSN 1437-4447)}},
Series = {{SEKI Working-Paper SWP-2009-02}},
Title = {Automating Quantified Multimodal Logics in Simple
Type Theory -- A Case Study},
OPTurl = {http://arxiv.org/abs/0905.4369},
doi = {10.48550/ARXIV.0905.4369},
Year = 2009,
}
@techreport{R47,
Author = {Benzm{\"u}ller, Christoph},
Howpublished = {International University in Germany, Bruchsal},
Keywords = {own, LEO Prover, Higher Order Logic, Automated
Reasoning, Henkin Semantics, Ontology Reasoning},
Title = {{Kooperatives höherstufiges-erststufiges automatisches Beweisen zum Schließen in Ontologien}},
url = {http://christoph-benzmueller.de/papers/R47.pdf},
Year = 2009,
}
@techreport{R48,
Author = {Benzm{\"u}ller, Christoph},
Keywords = {own, LEO Prover, Higher Order Logic, Automated
Reasoning},
Institution = {AAR Newsletter No. 84},
Title = {A Note on {LEO-II} and the Basic Fragment of Simple
Type Theory},
Url = {http://www.AARInc.org/Newsletters/084-2009-07.html},
Year = 2009,
}
@techreport{R49,
Author = {Benzm{\"u}ller, Christoph and Sutcliffe, Geoff},
Institution = {Saarland University},
Title = {The {THFTPTP} Project --- An Infrastructure for
Typed Higher-order Form Automated Theorem Proving
Marie Curie International Incoming Fellowship Grant
Agreement PIIF-GA-2008-219982 Project Report ---
Implications},
url = {http://christoph-benzmueller.de/papers/R49.pdf},
Year = 2009,
}
@techreport{R5,
Author = {Christoph Benzm{\"u}ller and Michael Kohlhase},
Institution = {Saarland University, SEKI Publications (ISSN
1437-4447)},
Number = {SR-97-09},
Pages = {1-34},
Publisher = {{SEKI Publications (ISSN 1437-4447)}},
Title = {Model Existence for Higher-Order Logic},
Type = {SEKI Report},
url = {http://christoph-benzmueller.de/papers/R5.pdf},
Year = 1997,
doi = {10.22028/D291-41622},
}
@techreport{R50,
Author = {Benzm{\"u}ller, Christoph and Sutcliffe, Geoff},
Institution = {Saarland University},
Publisher = {Saarland University},
Title = {The {THFTPTP} Project --- An Infrastructure for
Typed Higher-order Form Automated Theorem Proving
Marie Curie International Incoming Fellowship Grant
Agreement PIIF-GA-2008-219982 Project Report ---
Scientific},
url = {http://christoph-benzmueller.de/papers/R50.pdf},
Year = 2009,
}
@techreport{R51,
Author = {Benzm{\"u}ller, Christoph and Wirth, Claus-Peter},
Howpublished = {DFG research project proposal},
Keywords = {own, LEO Prover, Higher Order Logic, Automated
Reasoning},
Title = {{Effective Higher-Order Automated Theorem Proving
with integrated Descente Infinie and Presburger
Arithmetic LEO-III}},
url = {http://christoph-benzmueller.de/papers/R51.pdf},
Year = 2009,
}
@misc{R53,
doi = {10.48550/ARXIV.1207.6685},
OPTurl = {https://arxiv.org/abs/1207.6685},
author = {Benzm{\"u}ller, Christoph and Raths, Thomas},
title = {FMLtoHOL (version 1.0): Automating First-order Modal
Logics with LEO-II and Friends},
publisher = {arXiv},
note = {Preprint},
year = 2012,
copyright = {arXiv.org perpetual, non-exclusive license}
}
@misc{R52,
doi = {10.48550/ARXIV.1106.3685},
OPTurl = {https://arxiv.org/abs/1106.3685},
author = {Benzm{\"u}ller, Christoph and Gabbay, Dov and
Genovese, Valerio and Rispoli, Daniele},
title = {Embedding and Automating Conditional Logics in
Classical Higher-Order Logic},
publisher = {arXiv},
note = {Preprint},
year = 2011,
copyright = {arXiv.org perpetual, non-exclusive license}
}
@techreport{R6,
Author = {Christoph Benzm{\"u}ller and Michael Kohlhase},
Institution = {Saarland University, SEKI Publications (ISSN
1437-4447)},
Number = {SR-97-10},
Pages = {1-12},
Publisher = {{SEKI Publications (ISSN 1437-4447)}},
Title = {Henkin Completeness of Higher-Order Resolution},
Type = {SEKI Report},
url = {http://christoph-benzmueller.de/papers/R6.pdf},
Year = 1997,
urn = {urn:nbn:de:hbz:386-kluedo-3813},
}
@techreport{R7,
Author = {Christoph Benzm{\"u}ller},
Institution = {Saarland University, SEKI Publications (ISSN
1437-4447)},
Number = {SR-98-07},
Pages = {1-55},
Publisher = {{SEKI Publications (ISSN 1437-4447)}},
Title = {An Adaptation of Paramodulation and RUE-Resolution
to Higher-Order Logic},
Type = {SEKI Report},
url = {http://christoph-benzmueller.de/papers/R7.pdf},
Year = 1998,
}
@techreport{R8,
Author = {Christoph Benzm{\"u}ller},
Note = {Draft, AG Siekmann, Saarland University},
Pages = {1-17},
Title = {{F}orschungsinteressen am {G}raduiertenkolleg
{K}ognitionswissenschaft},
url = {http://christoph-benzmueller.de/papers/R8.pdf},
Year = 1999,
}
@techreport{R9,
Author = {Christoph Benzm{\"u}ller and Volker Sorge},
Institution = {Saarland University, SEKI Publications (ISSN
1437-4447)},
Number = {SR-99-02},
Pages = {1-13},
Publisher = {{SEKI Publications (ISSN 1437-4447)}},
Title = {Resource Adaptive Agents in Interactive Theorem
Proving},
Type = {SEKI Report},
OPTurl = {http://arxiv.org/abs/0901.3585},
doi = {10.48550/ARXIV.0901.3585},
Year = 1999,
}
@mastersthesis{T1,
Keywords = {thesis},
Author = {Christoph Benzm{\"u}ller},
Pages = {1-194},
School = {Department of Computer Science, Saarland University,
Germany},
Title = {{Eine Fallstudie zur Spezifikation von
Systemanforderungen in der Spezifikationssprache
OBSCURE}},
url = {http://christoph-benzmueller.de/papers/T1.pdf},
Year = 1994,
}
@phdthesis{T2,
Author = {Christoph Benzm{\"u}ller},
Keywords = {own, thesis, Higher Order Logic, Henkin Semantics,
LEO Prover, Automated Reasoning},
Pages = {1-174},
School = {Naturwissenschaftlich-Technische Fakult{\"a}t I,
Saarland University, Saarbr{\"u}cken, Germany},
Title = {Equality and Extensionality in Higher-Order Theorem
Proving},
doi = {10.22028/D291-25680},
url = {http://christoph-benzmueller.de/papers/T2.pdf},
Year = 1999,
}
@book{T3,
Author = {Christoph Benzm{\"u}ller},
Keywords = {own, thesis, Higher Order Logic, Henkin Semantics,
LEO Prover, Automated Reasoning},
Pages = {1-357},
Publisher = {Saarland University, Germany},
Title = {Cumulative Habilitation Script},
url = {http://christoph-benzmueller.de/papers/T3.pdf},
Year = 2006,
}
@inproceedings{W1,
Abstract = {Most interactive proof development environments are
insufficient to handle the complexity of the
information to be conveyed to the user and to
support his orientation in large-scale proofs. In
this paper we present a distributed client-server
extension of the OMEGA proof development system,
focusing on the LOUI (Lovely OMEGA User Interface)
client. This graphical user interface provides
advanced communication facilities through an
adaptable proof tree visualization and through
various selective proof object display methods. Some
of LOUI's main features are the graphical display of
co-references in proof graphs, a selective term
browser, and support for dynamically adding
knowledge to partial proofs -- all based upon and
implemented in a client-server architecture.},
Address = {Eindhoven, Netherlands},
Author = {J{\"o}rg Siekmann and Stephan Hess and Christoph
Benzm{\"u}ller and Lassaad Cheikhrouhou and Detlef
Fehrer and Armin Fiedler and Helmut Horacek and
Michael Kohlhase and Karsten Konrad and Andreas
Meier and Erica Melis and Volker Sorge},
Booktitle = {Proceedings of the International Workshop "User
Interfaces for Theorem Provers 1998 (UITP'98)},
Pages = {130-138},
Title = {A Distributed Graphical User Interface for the
Interactive Proof System},
url = {http://christoph-benzmueller.de/papers/W1.pdf},
Year = 1998,
}
@inproceedings{W10,
Author = {Christoph Benzm{\"u}ller},
Booktitle = {Extended abstract for invited plenary talk at
AISB'01 Convention `Agents and Cognition},
Comment = {slides},
Keywords = {own, Agents, Proof Assistants, Automated Reasoning},
Pages = {57-58},
Publisher = {University of York},
Title = {An Agent Based Approach to Reasoning},
url = {http://christoph-benzmueller.de/papers/W10.pdf},
Year = 2001,
}
@inproceedings{W11,
Abstract = {This paper discusses experiments with an agent
oriented approach to automated and interactive
reasoning. The approach combines ideas from two
subfields of AI (theorem proving/proof planning and
multi-agent systems) and makes use of state of the
art distribution techniques to decentralise and
spread its reasoning agents over the internet. It
particularly supports cooperative proofs between
reasoning systems which are strong in different
application areas, e.g., higher-order and
first-order theorem provers and computer algebra
systems.},
Address = {Siena, Italy},
Author = {Christoph Benzm{\"u}ller and Mateja Jamnik and
Manfred Kerber and Volker Sorge},
Booktitle = {Proceedings of the Calculemus Workshop 2001},
Pages = {48-63},
Title = {An Agent-oriented Approach to Reasoning},
url = {http://christoph-benzmueller.de/papers/W11.pdf},
Year = 2001,
}
@inproceedings{W12,
Address = {Siena, Italy},
Author = {Christoph Benzm{\"u}ller and Andreas Meier and Erica
Melis and Martin Pollet and Volker Sorge},
Booktitle = {Proceedings of the IJCAR 2001 Workshop: Future
Directions in Automated Reasoning},
Pages = {25-37},
Title = {Proof Planning: A Fresh Start?},
url = {http://christoph-benzmueller.de/papers/W12.pdf},
Year = 2001,
}
@inproceedings{W13,
Abstract = {We re-investigate a proof example presented by
George Boolos which perspicuously illustrates
G\"odel's argument for the potentially drastic
increase of proof-lengths in formal systems when
carrying through the argument at too low a
level. More concretely, restricting the order of the
logic in which the proof is carried through to the
order of the logic in which the problem is
formulated in the first place can result in
unmanageable long proofs, although there are short
proofs in a logic of higher order. Our motivation in
this paper is of practical nature and its aim is to
sketch the implications of this example to current
technology in automated theorem proving, to point to
related questions about the foundational character
of type theory (without explicit comprehension
axioms) for mathematics, and to work out some
challenging aspects with regard to the automation of
this proof -- which, as we belief, nicely
illustrates the discrepancy between the creativity
and intuition required in mathematics and the
limitations of state of the art theorem provers.},
Address = {Siena, Italy},
Author = {Christoph Benzm{\"u}ller and Manfred Kerber},
Booktitle = {Proceedings of the IJCAR 2001 Workshop: Future
Directions in Automated Reasoning},
Pages = {13-24},
Title = {A Lost Proof},
url = {http://christoph-benzmueller.de/papers/W13.pdf},
Year = 2001,
}
@inproceedings{W14,
Address = {RISC Linz, Schloss Hagenberg},
Author = {Christoph Benzm{\"u}ller and Andreas Meier and
Volker Sorge},
Booktitle = {First International Workshop on Mathematical
Knowledge Management},
Comment = {slides},
Pages = {1-7},
Title = {Distributed Assertion Retrieval},
url = {http://christoph-benzmueller.de/papers/W14.pdf},
Year = 2001,
}
@inproceedings{W15,
Address = {London, England},
Author = {Christoph Benzm{\"u}ller and Volker Sorge},
Booktitle = {Proceedings of the 9th Workshop on Automated
Reasoning: Bridging the Gap between Theory and
Practice},
Pages = {1-3},
Title = {Agent-based Theorem Proving},
url = {http://christoph-benzmueller.de/papers/W15.pdf},
Year = 2002,
}
@inproceedings{W16,
Abstract = {This paper describes work aimed at integrating
OMEGA's agent-based suggestion mechanism OANTS and
the new theorem proving framework developed by
Autexier [Autexier01].},
Address = {Marseilles, France},
Author = {Malte H{\"u}bner and Serge Autexier and Christoph
Benzm{\"u}ller},
Booktitle = {Additonal Proceedings of 10th Symposium on the
Integration of Symbolic Computation and Mechanized
Reasoning (CALCULEMUS 2002)},
Comment = {slides},
Pages = {11-20},
Title = {Agent-based Proof Search with Indexed Formulas},
url = {http://christoph-benzmueller.de/papers/W16.pdf},
Year = 2002,
}
@inproceedings{W17,
Abstract = {Verification of hybrid systems is a challenging
task. Unlike many other verification methods the
approach proposed in [nonnengart99] avoids
approximations and operates directly on the original
system specifications. This approach, however,
requires the solution of non-trivial mathematical
subtasks. We propose to model those kinds of
subtasks that are suitable for being tackled with
reasoning specialists as mathematical service
requests to a network of service systems like the
MathWeb Software Bus. So far we have identified the
following candidates of mathematical service
requests: the solution of differential equations,
subsumption and consistency of sets of
constraints. A further candidate can be the
elimination of second order set variables with
higher order theorem provers.},
Address = {Marseilles, France},
Author = {Christoph Benzm{\"u}ller and Corrado Giromini and
Andreas Nonnengart},
Booktitle = {Additonal Proceedings of 10th Symposium on the
Integration of Symbolic Computation and Mechanized
Reasoning (CALCULEMUS 2002)},
Pages = {1-10},
Title = {Symbolic Verification of Hybrid Systems supported by
Mathematical Services},
url = {http://christoph-benzmueller.de/papers/W17.pdf},
Year = 2002,
}
@inproceedings{W18,
Abstract = {Verification of non-linear hybrid systems is a
challenging task. Unlike many other verification
methods the deduction-based verification approach we
investigate in this paper avoids approximations and
operates directly on the original non-linear system
specifications. This approach, however, requires the
solution of non-trivial mathematical subtasks. We
propose to model existing reasoning systems, such as
computer algebra systems and constraint solvers, as
mathematical services and to provide them in a
network of mathematical tools in a way that they can
reasonably support subtasks as they may occur in
formal methods applications. The motivation is to
make it simpler to implement and test verification
approaches by out-sourcing complex but precisely
identifiable mathematical subtasks for which
specialised reasoners do already exists.},
Address = {Kopenhagen, Denmark},
Author = {Christoph Benzm{\"u}ller and Corrado Giromini and
Andreas Nonnengart and J{\"u}rgen Zimmer},
Booktitle = {Proceedings of the Verification Workshop - VERIFY'02
in connection with FLOC 2002},
Pages = {29-39},
Title = {Reasoning Services in the MathWeb-SB for Symbolic
Verification of Hybrid Systems},
url = {http://christoph-benzmueller.de/papers/W18.pdf},
Year = 2002,
}
@inproceedings{W20,
Address = {Liverpool, England},
Author = {Bao Quoc Vo and Christoph Benzm{\"u}ller and Serge
Autexier},
Booktitle = {Proceedings of the 10th Workshop on Automated
Reasoning: Bridging the Gap between Theory and
Practice},
Title = {Assertion Application in Theorem Proving and Proof
Planning},
url = {http://christoph-benzmueller.de/papers/W19.pdf},
Year = 2003,
}
@inproceedings{W2,
Abstract = {We report on the integration of TPS as an external
reasoning component into the mathematical assistant
system OMEGA. Thereby TPS can be used both as an
automatic theorem prover for higher order logic as
well as interactively employed from within the OMEGA
environment. TPS proofs can be directly incorporated
into OMEGA on a tactic level enabling their
visualization and verbalization. Using an example we
show how \tps\/ proofs can be inserted into OMEGA's
knowledge base by expanding them to calculus level
using both OMEGA's tactic mechanism and the first
order theorem prover OTTER. Furthermore we
demonstrate how the facts from OMEGA's knowledge
base can be used to build a TPS library.},
Address = {Canberra, Australia},
Author = {Christoph Benzm{\"u}ller and Volker Sorge},
Booktitle = {Theorem Proving in Higher Order Logics: Emerging
Trends},
Editor = {Jim Grundy and Malcolm Newey},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Proof Transformation, System Integration},
Pages = {1-18},
Series = {Technical Report 98-08, Department of Computer
Science and Computer Science Lab, The Australian
National University},
Title = {Integrating {TPS} with {OMEGA}},
url = {http://christoph-benzmueller.de/papers/W2.pdf},
Year = 1998,
}
@inproceedings{W21,
Address = {Acapulco, Mexico},
Author = {Christoph Benzm{\"u}ller and Armin Fiedler and Malte
Gabsdil and Helmut Horacek and Ivana
Kruijff-Korbayova and Manfred Pinkal and J{\"o}rg
Siekmann and Dimitra Tsovaltzi and Bao Quoc Vo and
Magdalena Wolska},
Booktitle = {Proceedings of IJCAI-03 Workshop on Knowledge
Representation and Automated Reasoning for
E-Learning Systems},
Comment = {slides},
Keywords = {own, DIALOG, Proof Presentation, Natural Language
Dialog, Proof Assistants, Tutoring Systems},
Pages = {12-22},
Title = {Tutorial Dialogs on Mathematical Proofs},
url = {http://christoph-benzmueller.de/papers/W20.pdf},
Year = 2003,
}
@inproceedings{W22,
Address = {Rome, Italy},
Author = {Christoph Benzm{\"u}ller},
Booktitle = {Proceedings of the 11th Symposium on the Integration
of Symbolic Computation and Mechanized Reasoning
(CALCULEMUS 2003)},
Comment = {slides},
Keywords = {own, CALCULEMUS, Symb. Computation and
Symb. Reasoning},
Pages = {1-16},
Publisher = {MMIII ARACNE EDITRICE S.R.L. (ISBN 88-7999-545-6)},
Title = {The {CALCULEMUS} research training network: A short
overview},
url = {http://christoph-benzmueller.de/papers/W21.pdf},
Year = 2003,
}
@inproceedings{W23,
Address = {Miami, USA},
Author = {Christoph Benzm{\"u}ller},
Booktitle = {Proceedings of the First QPQ Workshop on Deductive
Software Components at CADE-19},
Comment = {slides},
Keywords = {own, CALCULEMUS, Symb. Computation and
Symb. Reasoning},
Pages = {13-27},
Title = {The {CALCULEMUS} research training network: A short
overview},
url = {http://christoph-benzmueller.de/papers/W22.pdf},
Year = 2003,
}
@inproceedings{W24,
Address = {Sydney, Australia},
Author = {Christoph Benzm{\"u}ller and Armin Fiedler and Malte
Gabsdil and Helmut Horacek and Ivana
Kruijff-Korbayova and Manfred Pinkal and J\"org
Siekmann and Dimitra Tsovaltzi and Bao Quoc Vo and
Magdalena Wolska},
Booktitle = {Proceedings of AI in Education (AIED 2003) Workshop
on Advanced Technologies for Mathematics Education},
Keywords = {own, DIALOG, Proof Presentation, Natural Language
Dialog, Proof Assistants, Tutoring Systems},
Title = {A Wizard of Oz Experiment for Tutorial Dialogues in
Mathematics},
url = {http://christoph-benzmueller.de/papers/W23.pdf},
Year = 2003,
}
@inproceedings{W25,
Address = {Rome, Italy},
Author = {Malte H\"ubner and Christoph Benzm{\"u}ller and
Serge Autexier and Andreas Meier},
Booktitle = {Proceedings of the Workshop User Interfaces for
Theorem Provers (UITP 2003)},
Note = {Also available as: Technical Report No. 189,
Institut f\"ur Informatik,
Albert-Ludwig-Universit\"at, Freiburg},
Pages = {81-100},
Publisher = {ARACNE EDITRICE S.R.L. (ISBN 88-7999-545-6)},
Title = {Interactive Proof Construction at the Task Level},
url = {http://christoph-benzmueller.de/papers/W24.pdf},
Year = 2003,
}
@inproceedings{W26,
Address = {Wallerfangen, Germany},
Author = {Christoph Benzm{\"u}ller and Armin Fiedler and Malte
Gabsdil and Helmut Horacek and Ivana
Kruijff-Korbayova and Dimitra Tsovaltzi and Bao Quoc
Vo and Magdalena Wolska},
Booktitle = {Proceedings of the 7th Workshop on the semantics and
pragmatics of dialogue (DiaBruck)},
Keywords = {own, DIALOG, Proof Presentation, Natural Language
Dialog, Tutoring Systems},
Title = {Language Phenomena in Tutorial Dialogs on
Mathematical Proofs},
url = {http://christoph-benzmueller.de/papers/W25.pdf},
Year = 2003,
}
@inproceedings{W27,
Address = {Hamburg, Germany},
Author = {Christoph Benzm{\"u}ller and Armin Fiedler and Malte
Gabsdil and Helmut Horacek and Ivana
Kruijff-Korbayova and Dimitra Tsovaltzi and Bao Quoc
Vo and Magdalena Wolska},
Booktitle = {Proceedings of the Workshop on Expressive Media and
Intelligent Tools for Learning, German Conference on
AI (KI 2003)},
Title = {Towards a Principled Approach to Tutoring
Mathematical Proofs},
url = {http://christoph-benzmueller.de/papers/W26.pdf},
Year = 2003,
}
@inproceedings{W28,
Address = {Heriot-Watt University, Edinburgh, Scotland},
Author = {Serge Autexier and Christoph Benzm{\"u}ller},
Booktitle = {Mathematical Knowledge Management Symposium},
Comment = {slides},
Keywords = {own, Proof Assistants, OMEGA, Interactive Proof,
Mathematical Knowledge Management, Proof Planning,
System Integration},
Title = {{OMEGA} --- From Proof Planning towards Mathematical
Knowledge Management},
url = {http://christoph-benzmueller.de/papers/W27.pdf},
Year = 2003,
}
@inproceedings{W19,
Address = {London, England},
Author = {Mateja Jamnik and Manfred Kerber and Martin Pollet
and Christoph Benzm{\"u}ller},
Booktitle = {Proceedings of the 9th Workshop on Automated
Reasoning: Bridging the Gap between Theory and
Practice},
Pages = {1-2},
Title = {Automatic Learning of Proof Methods in Proof
Planning},
url = {https://arw.csc.liv.ac.uk/year/2002/papers/jamnik.ps},
Year = 2002,
}
@inproceedings{W29,
Address = {Edinburgh, Scotland},
Author = {Mark Buckley and Christoph Benzm{\"u}ller},
Booktitle = {Proceedings of the ETAPS Satellite Workshop on User
Interfaces for Theorem Provers (UITP)},
Keywords = {own, DIALOG, Proof Presentation, Natural Language
Dialog, Proof Assistants, Tutoring Systems, Agents,
System Integration},
Pages = {40-67},
Title = {System Description: A Dialog Manager supporting
Tutorial Natural Language Dialogue on Proofs},
url = {http://christoph-benzmueller.de/papers/W29.pdf},
Year = 2005,
}
@inproceedings{W3,
Author = {Christoph Benzm{\"u}ller and Volker Sorge},
Booktitle = {Proceedings of the 6th Workshop on Automated
Reasoning},
Note = {(Mildly reviewed)},
Pages = {19-20},
Publisher = {Edinburgh College of Art \& Divison of Informatics,
University of Edinburgh},
Title = {Towards Fine-Grained Proof Planning with Critical
Agents},
url = {http://christoph-benzmueller.de/papers/W3.pdf},
Year = 1999,
}
@inproceedings{W30,
Address = {Edinburgh, Scotland},
Author = {Mark Buckley and Christoph Benzm{\"u}ller},
Booktitle = {Proceedings of the ETAPS Satellite Workshop on User Interfaces for Theorem Provers (UITP)},
Pages = {16-39},
Title = {Integrating Proof Assistants as Reasoning and
Verification Tools into a Scientific WYSIWIG Editor},
url = {http://christoph-benzmueller.de/papers/W30.pdf},
Year = 2005,
}
@inproceedings{W31,
Address = {Wexford Hotel, Montego Bay, Jamaica},
Author = {Christoph Benzm{\"u}ller},
Booktitle = {Proceedings of the LPAR-05 Workshop: Empirically
Successfull Automated Reasoning in Higher-Order
Logic (ESHOL)},
Keywords = {own, LEO Prover, Higher Order Logic, Automated
Reasoning, Henkin Semantics},
Note = {arXiv:cs/0601042},
Pages = {25-44},
Title = {System Description: {LEO} -- A Resolution based
Higher-Order Theorem Prover},
OPTurl = {http://arxiv.org/abs/cs/0601042},
doi = {10.48550/ARXIV.CS/0601042},
Year = 2005,
}
@inproceedings{W32,
Address = {Wexford Hotel, Montego Bay, Jamaica},
Author = {Christoph Benzm{\"u}ller and Volker Sorge and Mateja
Jamnik and Manfred Kerber},
Booktitle = {Proceedings of the LPAR-05 Workshop: Empirically
Successfull Automated Reasoning in Higher-Order
Logic {(ESHOL)}},
Note = {arXiv:cs/0601042},
Pages = {45-58},
Title = {Combining Proofs of Higher-Order and First-Order
Automated Theorem Provers},
OPTUrl = {http://arxiv.org/abs/cs/0601042},
Doi = {10.48550/arXiv.cs/0601042},
Year = 2005,
}
@inproceedings{W33,
Address = {Bremen, Germany},
Author = {Marvin Schiller and Christoph Benzm{\"u}ller},
Booktitle = {Poster papers at KI 2006: Advances in Artificial
Intelligence: 29th Annual German Conference on AI},
Keywords = {own, Proof Presentation, DIALOG, Natural Language
Dialog, Proof Assistants, Machine Learning, Tutoring
Systems},
Title = {Granularity Judgments in Proof Tutoring},
url = {http://christoph-benzmueller.de/papers/W33.pdf},
Year = 2006,
}
@inproceedings{W34,
Address = {Pnom Penh, Cambodia},
Author = {Marvin Schiller and Christoph Benzm{\"u}ller and Ann
van de Veire},
Booktitle = {Short papers at LPAR 2006: 13th International
Conference on Logic for Programming Artificial
Intelligence and Reasoning},
Comment = {slides},
Keywords = {own, Proof Presentation, DIALOG, Natural Language
Dialog, Proof Assistants, Machine Learning, Tutoring
Systems},
Title = {Judging Granularity for Automated Mathematics
Teaching},
url = {http://christoph-benzmueller.de/papers/W34.pdf},
Year = 2006,
}
@inproceedings{W35,
Address = {Pnom Penh, Cambodia},
Author = {Frank Theiss and Christoph Benzm{\"u}ller},
Booktitle = {IWIL-6 workshop at LPAR 2006: The 6th International
Workshop on the Implementation of Logics},
Comment = {slides},
Keywords = {own, LEO Prover, Higher Order Logic, Automated
Reasoning},
Title = {Term Indexing for the {LEO-II} Prover},
url = {http://christoph-benzmueller.de/papers/W35.pdf},
Year = 2006,
}
@inproceedings{W36,
Author = {Christoph Benzm{\"u}ller and Paulson, Lawrence
C. and Frank Theiss and Arnaud Fietzke},
Booktitle = {Proceedings of the Fourteenth Workshop on Automated
Reasoning, Bridging the Gap between Theory and
Practice},
Keywords = {own, LEO Prover, Higher Order Logic, Automated
Reasoning},
Note = {(Mildly reviewed)},
Publisher = {Imperial College, London, England},
Title = {The {LEO-II} Project},
url = {http://christoph-benzmueller.de/papers/W36.pdf},
Year = 2007,
}
@inproceedings{W37,
Author = {Christoph Benzm{\"u}ller and Paulson, Lawrence
C. and Frank Theiss and Arnaud Fietzke},
Booktitle = {TPHOLs 2007 Emerging Trends Proceedings},
Comment = {slides},
Keywords = {own, LEO Prover, Higher Order Logic, Automated
Reasoning},
Pages = {33-48},
Publisher = {Internal Report 364/07 at Department of Computer
Science},
Address = {University of Kaiserslautern, Germany},
Title = {Progress Report on {LEO-II} -- An Automatic Theorem
Prover for Higher-Order Logic},
url = {http://christoph-benzmueller.de/papers/W37.pdf},
Year = 2007,
}
@inproceedings{W38,
Address = {Jacobs University Bremen, Germany},
Author = {Marvin Schiller and Dominik Dietrich and Christoph
Benzm{\"u}ller},
Booktitle = {JEM Workshop on identifying and supporting
(scientific) communities in education and research},
Keywords = {own, Proof Presentation, DIALOG, Natural Language
Dialog, Proof Assistants, Machine Learning, Tutoring
Systems},
Note = {(Mildly reviewed)},
Title = {Towards Computer-Assisted Proof Tutoring},
url = {http://christoph-benzmueller.de/papers/W38.pdf},
Year = 2007,
}
@inproceedings{W39,
Author = {Christoph Benzm{\"u}ller and Florian Rabe and
Carsten Sch{\"u}rmann and Geoff Sutcliffe},
Booktitle = {Proceedings of the First International Workshop on
Practical Aspects of Automated Reasoning, Sydney,
Australia, August 10-11, 2008},
Editor = {Boris Konev and Renate A. Schmidt and Stephan
Schulz},
Note = {(Invited non-reviewed paper)},
Publisher = {CEUR-WS.org},
Series = {CEUR Workshop Proceedings},
Title = {Evaluation of Systems for Higher-order Logic
{(ESHOL)}},
url = {http://christoph-benzmueller.de/papers/W39.pdf},
Volume = 373,
Year = 2008,
}
@inproceedings{W4,
Abstract = {In this contribution we propose an agent
architecture for theorem proving which we intend to
investigate in depth in the future. The work
reported in this paper is in an early state, and by
no means finished. We present and discuss our
proposal in order to get feedback from the
Calculemus community.},
Address = {Trento, Italy},
Author = {Christoph Benzm{\"u}ller and Mateja Jamnik and
Manfred Kerber and Volker Sorge},
Booktitle = {Proceedings of the Calculemus Workshop: Systems for
Integrated Computation and Deduction},
Comment = {slides},
Pages = {1-12},
Title = {Agent Based Mathematical Reasoning},
url = {http://christoph-benzmueller.de/papers/W4.pdf},
Year = 1999,
}
@inproceedings{W45,
Author = {Christoph Benzm{\"u}ller and Adam Pease},
Booktitle = {PAAR-2010 -- Workshop on Practical Aspects of
Automated Reasoning},
Comment = {slides},
Editor = {Renate A. Schmidt and Stephan Schulz and Boris
Konev},
issn = {2398-7340},
Pages = {22-32},
Publisher = {EasyChair},
Series = {EPiC Series in Computing},
Title = {Progress in Automating Higher-Order Ontology
Reasoning},
OPTUrl =
{http://www.easychair.org/publications/?page=999569486},
Volume = 9,
Year = 2012,
Doi = {10.29007/dtnz},
}
@inproceedings{W40,
Address = {Lisbon, Portugal},
Author = {Christoph Benzm{\"u}ller},
Booktitle = {Computational Logic in Multi-Agent Systems, 11th
International Workshop, CLIMA XI, Lisbon, Portugal,
August 16-17, 2010. Proceedings},
Doi = {10.1007/978-3-642-14977-1_6},
Editor = {J{\"u}rgen Dix and Joao Leite and Guido Governatori
and Woitek Jamroga},
Pages = {33-48},
Publisher = {Springer},
Series = {Lecture Notes in Artifical Intelligence},
Title = {Combining Logics in Simple Type Theory},
url = {http://christoph-benzmueller.de/papers/W41.pdf},
Volume = 6245,
Year = 2010,
}
@inproceedings{W41,
Address = {Lisbon, Portugal},
Author = {Adam Pease and Christoph Benzm{\"u}ller},
Booktitle = {The ECAI 2010 Workshop on Intelligent Engineering
Techniques for Knowledge Bases (IKBET'2010)},
Comment = {slides},
Note = {(Superseded by 2013 paper in AI Communications)},
Title = {{Sigma}: An Integrated Development Environment for
Logical Theory Development},
url = {http://christoph-benzmueller.de/papers/W42.pdf},
Year = 2010,
}
@inproceedings{W42,
Address = {August 16-17, Lisbon, Portugal},
Author = {Adam Pease and Christoph Benzm{\"u}ller},
Booktitle = {The ECAI-10 Workshop on Automated Reasoning about
Context and Ontology Evolution (ARCOE-10)},
Comment = {slides},
Editor = {A.~Bundy and J.~Lehmann and G.~Qi and
I.~J.~Varzinczak},
Title = {Ontology Archaeology: Mining a Decade of Effort on
the Suggested Upper Merged Ontology},
url = {http://christoph-benzmueller.de/papers/W43.pdf},
Year = 2010,
}
@inproceedings{W43,
Address = {August 16-17, Lisbon, Portugal},
Author = {Christoph Benzm{\"u}ller and Adam Pease},
Booktitle = {The ECAI-10 Workshop on Automated Reasoning about
Context and Ontology Evolution (ARCOE-10)},
Comment = {slides},
Editor = {A.~Bundy and J.~Lehmann and G.~Qi and
I.~J.~Varzinczak},
Keywords = {own, Ontology Reasoning, Automated Reasoning, Higher
Order Logic},
Note = {(Superseded by 2012 paper in Journal of Web
Semantics)},
Title = {Reasoning with Embedded Formulas and Modalities in
{SUMO}},
url = {http://christoph-benzmueller.de/papers/W44.pdf},
Year = 2010,
}
@inproceedings{W44,
Address = {Paris, France},
Author = {Marvin Schiller and Christoph Benzm{\"u}ller},
Booktitle = {Workshop on Mathematically Intelligent Proof Search
(MIPS 2010, affiliated with CICM 2010)},
Keywords = {own, Proof Presentation, DIALOG, Natural Language
Dialog, Proof Assistants, Machine Learning, Tutoring
Systems},
Title = {Human-Oriented Proof Techniques are Relevant for
Proof Tutoring},
url = {http://christoph-benzmueller.de/papers/W45.pdf},
Year = 2010,
}
@inproceedings{W46,
Author = {Christoph Benzm{\"u}ller and Marvin Schiller},
Booktitle = {EMSQMS 2010 -- Workshop on Evaluation Methods for
Solvers and Quality Metrics for Solutions},
Editor = {Aaron Stump and Geoff Sutcliffe and Cesare Tinelli},
issn = {2398-7340},
Keywords = {own, Proof Presentation, DIALOG, Natural Language
Dialog, Proof Assistants, Machine Learning, Tutoring
Systems},
Pages = {39-40},
Publisher = {EasyChair},
Series = {EPiC Series in Computing},
Title = {Adaptive Assertion-Level Proofs},
OPTurl =
{http://www.easychair.org/publications/?page=1718758449},
Volume = 6,
Year = 2012,
Doi = {10.29007/gvgn},
}
@inproceedings{W47,
Address = {Merida, Venezuela},
Author = {Nik Sultana and Christoph Benzm{\"u}ller},
Booktitle = {IWIL 2012},
Editor = {Konstantin Korovin and Stephan Schulz and Eugenia
Ternovska},
issn = {2398-7340},
Keywords = {own, LEO Prover, Higher Order Logic, Automated
Reasoning, Henkin Semantics, System Integration},
Pages = {33-52},
Publisher = {EasyChair},
Series = {EPiC Series in Computing},
Title = {Understanding {LEO-II's} Proofs},
OPTurl =
{http://www.easychair.org/publications/?page=572811915},
Volume = 22,
Year = 2013,
Doi = {10.29007/x9c9},
}
@inproceedings{W48,
Author = {Christoph Benzm{\"u}ller and Jens Otten and Thomas
Raths},
Booktitle = {PAAR-2012},
Editor = {Pascal Fontaine and Renate A. Schmidt and Stephan
Schulz},
issn = {2398-7340},
Keywords = {own, Higher Order Logic, Automated Reasoning,
Semantic Embedding, Modal Logics},
Pages = {12-18},
Publisher = {EasyChair},
Series = {EPiC Series in Computing},
Title = {Implementing Different Proof Calculi for First-order
Modal Logics},
OPTurl =
{http://www.easychair.org/publications/?page=1303066787},
Volume = 21,
Year = 2013,
Doi = {10.29007/mclw},
}
@inproceedings{W5,
Abstract = {Today's interactive mathematics textbooks use a
collection of predefined documents, typically
organized as a network of html pages. This makes a
reuse and a sound re-combination of the encoded
knowledge impossible and inhibits a radical adaption
of course presentation and content to the user's
needs. In order to avoid these drawbacks we have
designed a web-based framework for dynamically
producing interactive documents for learning
mathematics called ID. The system design relies on
the separation of knowledge representation from
system functionalities. Salient features of our
system are the individual generation of interactive
documents based on general domain knowledge,
user-specific preferences and the user's knowledge
as well as the integration of external problem
solving systems. The paper describes the distributed
web-based architecture of our system and the
principles of its components.},
Address = {Montreal},
Author = {J{\"o}rg Siekmann and Christoph Benzm{\"u}ller and
Armin Fiedler and Andreas Franke and George Goguadze
and Helmut Horacek and Michael Kohlhase and Paul
Libbrecht and Andreas Meier and Erica Melis and
Martin Pollet and Volker Sorge and Carsten Ullrich
and J{\"u}rgen Zimmer},
Booktitle = {Proceedings of the Fifth International Conference on
Intelligent Tutoring Systems---Workshop W2: Adaptive
and Intelligent Web-Based Education Systems},
Editor = {P. Brusilovski},
Pages = {54-61},
Title = {Adaptive Course Generation and Presentation},
url = {http://christoph-benzmueller.de/papers/W5.pdf},
Year = 2000,
}
@inproceedings{W7,
Author = {Mateja Jamnik and Manfred Kerber and Christoph
Benzm{\"u}ller},
Booktitle = {Proceedings of the CADE-17 Workshop: Automated
Deduction in the Context of Mathematics},
Pages = {1-12},
Title = {Towards Learning New Methods in Proof Planning},
url = {http://christoph-benzmueller.de/papers/W6.pdf},
Year = 2001,
}
@inproceedings{W6,
Address = {Birmingham, England},
Author = {Christoph Benzm{\"u}ller and Mateja Jamnik and
Manfred Kerber and Volker Sorge},
Booktitle = {Proceedings of the AISB'2000 Symposium `How to
design a functioning mind'},
Note = {(Mildly reviewed)},
Pages = {137-138},
Title = {Resource Guided Concurrent Deduction},
url = {http://christoph-benzmueller.de/papers/W7.pdf},
Year = 2000,
}
@inproceedings{W8,
Abstract = {In this paper we propose how proof planning systems
can be extended by an automated learning
capability. The idea is that a proof planner would
be capable of learning new proof methods from well
chosen examples of proofs which use a similar
reasoning strategy to prove related theorems, and
this strategy could be characterised as a proof
method. We propose a representation framework for
methods, and a machine learning technique which can
learn methods using this representation
framework. This is work in progress, and we hope to
gain useful feedback from the workshop community.},
Author = {Mateja Jamnik and Manfred Kerber and Christoph
Benzm{\"u}ller},
Booktitle = {Proceedings of the Eighth Workshop on Automated
Reasoning, Bridging the Gap between Theory and
Practice},
Note = {(Mildly reviewed)},
Pages = {5-6},
Publisher = {University of York},
Title = {Learning proof methods in proof planning},
url = {http://christoph-benzmueller.de/papers/W8.pdf},
Year = 2001,
}
@inproceedings{W9,
Author = {Christoph Benzm{\"u}ller and Andreas Meier and
Martin Pollet and Volker Sorge},
Booktitle = {Proceedings of the Eighth Workshop on Automated
Reasoning, Bridging the Gap between Theory and
Practice},
Note = {(Mildly reviewed)},
Pages = {1-2},
Publisher = {University of York},
Title = {Proof transformation and expansion with a
parameterisable inference machine.},
url = {http://christoph-benzmueller.de/papers/W9.pdf},
Year = 2001,
}