Back
  1. Home
  2. Profile of Christoph BENZMÜLLER (Unilu)
Profil

BENZMÜLLER Christoph

Main Referenced Co-authors
STEEN, Alexander  (26)
PARENT, Xavier  (16)
Wisniewski, Max (12)
Fuenmayor, David (11)
FARJAMI, Ali  (10)
Main Referenced Keywords
Higher Order Logic (28); Automated Reasoning (25); own (12); LEO Prover (9); Computational Metaphysics (8);
Main Referenced Disciplines
Computer science (60)
Philosophy & ethics (21)
Religion & theology (6)
Arts & humanities: Multidisciplinary, general & others (2)
Mathematics (2)

Publications (total 70)

The most downloaded
990 downloads
Benzmüller, C. (2018). Universal (Meta-)Logical Reasoning: Recent Successes. Science of Computer Programming. doi:10.1016/j.scico.2018.10.008 https://hdl.handle.net/10993/37443

The most cited

44 citations (Scopus®)

Steen, A., & Benzmüller, C. (2018). The Higher-Order Prover Leo-III. In Automated Reasoning 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings (pp. 108-116). Springer, Cham. doi:10.1007/978-3-319-94205-6_8 https://hdl.handle.net/10993/37461

Steen, A., & Benzmüller, C. (27 March 2021). Extensional Higher-Order Paramodulation in Leo-III. Journal of Automated Reasoning, 65, 775-807. doi:10.1007/s10817-021-09588-x
Peer Reviewed verified by ORBi

Benzmüller, C., Farjami, A., Fuenmajor, D., Meder, P. J. Y., Parent, X., Steen, A., van der Torre, L., & Zahoransky, V. (December 2020). LogiKEy Workbench: Deontic Logics, Logic Combinations and Expressive Ethical and Legal Reasoning (Isabelle/HOL Dataset). Data in Brief, 33. doi:10.1016/j.dib.2020.106409
Peer Reviewed verified by ORBi

Steen, A., & Benzmüller, C. (2020). The Higher-Order Prover Leo-III (Highlight paper). In Proceedings of the 24th European Conference on Artificial Intelligence (pp. 2937-2938). IOS Press. doi:10.3233/FAIA200462
Peer reviewed

Steen, A., & Benzmüller, C. (2020). On Reductions of Hintikka Sets for Higher-Order Logic. ORBilu-University of Luxembourg. https://orbilu.uni.lu/handle/10993/43235.

Benzmüller, C., & Steen, A. (November 2019). Consistent Rational Argumentation in Politics (CRAP) [Poster presentation]. Forum Experiment!, Hannover, Germany.

Fuenmayor, D., & Benzmüller, C. (2019). A Computational-Hermeneutic Approach for Conceptual Explicitation. In A. Nepomuceno, L. Magnani, F. Salguero, C. Bares, ... M. Fontaine (Eds.), Model-Based Reasoning in Science and Technology -- Inferential Models for Logic, Language, Cognition and Computation (pp. 441-469). Cham, Switzerland: Springer. doi:10.1007/978-3-030-32722-4_25
Peer reviewed

Fuenmayor, D., & Benzmüller, C. (2019). Harnessing Higher-Order (Meta-)Logic to Represent and Reason with Complex Ethical Theories. In A. Nayak & A. Sharma (Eds.), PRICAI 2019: Trends in Artificial Intelligence (pp. 418-432). Cham, Switzerland: Springer International Publishing. doi:10.1007/978-3-030-29908-8_34
Peer reviewed

Kirchner, D., Benzmüller, C., & Zalta, E. N. (23 August 2019). Computer Science and Metaphysics: A Cross-Fertilization. Open Philosophy, 2 (1), 230–251. doi:10.1515/opphil-2019-0015
Peer reviewed

Kirchner, D., Benzmüller, C., & Zalta, E. N. (2019). Mechanizing Principia Logico-Metaphysica in Functional Type Theory. Review of Symbolic Logic, 1-13. doi:10.1017/S1755020319000297
Peer reviewed

Benzmüller, C., Parent, X., & Ricca, F. (24 June 2019). Report on the Second International Joint Conference on Rules and Reasoning. AI Magazine, 40 (2), 73-74. doi:10.1609/aimag.v40i2.2888
Peer reviewed

Benzmüller, C. (June 2019). Universal (Meta-)Logical Reasoning: The Wise Men Puzzle (Isabelle/HOL Dataset). Data in Brief, 24 (103823), 1--5. doi:10.1016/j.dib.2019.103823
Peer reviewed

Benzmüller, C., Parent, X., & Steen, A. (Eds.). (2019). Selected Student Contributions and Workshop Papers of LuxLogAI 2018. EasyChair.

Benzmüller, C., & Andrews, P. (2019). Church's Type Theory. Stanford Encyclopedia of Philosophy, 1--62.
Peer reviewed

Benzmüller, C. (2019). Computational Metaphysics: New Insights on Gödel's Ontological Argument and Modal Collapse. In S. Kovac & K. Swietorzecka, Formal Methods and Science in Philosophy III, Informal Proceedings.

Steen, A., & Benzmüller, C. (2019). The Higher-Order Prover Leo-III (Extended Abstract). In C. Benzmüller & H. Stuckenschmidt (Eds.), {KI} 2019: Advances in Artificial Intelligence - 42nd German Conference on AI, Kassel, Germany, September 23-26, 2019, Proceedings (pp. 333-337). Springer. doi:10.1007/978-3-030-30179-8_30
Peer reviewed

Steen, A., & Benzmüller, C. (2019). Extensional Higher-Order Paramodulation in Leo-III. ORBilu-University of Luxembourg. https://orbilu.uni.lu/handle/10993/40691.

Benzmüller, C., & Stuckenschmidt, H. (Eds.). (2019). KI 2019: Advances in Artificial Intelligence -- 42nd German Conference on AI, Kassel, Germany, September 23-26, 2019, Proceedings. Springer, Cham, Cham. doi:10.1007/978-3-030-30179-8

Benzmüller, C., & Scott, D. (2019). Automating Free Logic in HOL, with an Experimental Application in Category Theory. Journal of Automated Reasoning. doi:10.1007/s10817-018-09507-7
Peer Reviewed verified by ORBi

Fuenmayor, D., & Benzmüller, C. (2019). Automated Reasoning with Complex Ethical Theories--A Case Study Towards Responsible AI. In 16th International Congress on Logic, Methodology and Philosophy of Science and Technology (CLMPST 2019) --- Bridging across Academic Cultures, Book of Abstracts.
Peer reviewed

Benzmüller, C., Farjami, A., & Parent, X. (2019). Åqvist's Dyadic Deontic Logic E in HOL. IfCoLog Journal of Logics and Their Applications, 6 (5), 733--755.
Peer reviewed

Benzmüller, C., Farjami, A., Meder, P. J. Y., & Parent, X. (2019). I/O Logic in HOL. IfCoLog Journal of Logics and Their Applications, 6 (5), 715--732.
Peer reviewed

Benzmüller, C. (2018). Universal (Meta-)Logical Reasoning: Recent Successes. Science of Computer Programming. doi:10.1016/j.scico.2018.10.008
Peer Reviewed verified by ORBi

Farjami, A., Meder, P. J. Y., Parent, X., & Benzmüller, C. (17 September 2018). I/O Logic in HOL [Paper presentation]. MIREL 2018 workshop on MIning and REasoning with Legal texts, Luxembourg.

Benzmüller, C., Farjami, A., & Parent, X. (17 September 2018). Aqvist's Dyadic Deontic Logic E in HOL [Paper presentation]. MIREL 2018 workshop on MIning and REasoning with Legal texts, Luxembourg.

Benzmüller, C., & Otten, J. (Eds.). (25 June 2018). ARQNL 2018 Automated Reasoning in Quantified Non-Classical Logics. CEUR Workshop Proceedings, 2095, 100.
Peer Reviewed verified by ORBi

Benzmüller, C., Farjami, A., & Parent, X. (16 June 2018). A Faithful Semantic Embedding of the Dyadic Deontic Logic E in HOL [Poster presentation]. 6th World Congress and School on Universal Logic, Vichy, France.

Benzmüller, C., Farjami, A., & Parent, X. (2018). A Dyadic Deontic Logic in HOL. In J. Broersen, C. Condoravdi, S. Nair, ... G. Pigozzi (Eds.), Deontic Logic and Normative Systems --- 14th International Conference, DEON 2018, Utrecht, The Netherlands, 3-6 July, 2018 (pp. 33-50). College Publications.
Peer reviewed

Benzmüller, C., Farjami, A., & Parent, X. (04 May 2018). Implementation of Dyadic Deontic Logic E in Isabelle/HOL [Paper presentation]. 10th edition of PhDs in Logic, Prague, Czechia.

Benzmüller, C., Farjami, A., & Parent, X. (2018). Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL.

Steen, A., & Benzmüller, C. (2018). System Demonstration: The Higher-Order Prover Leo-III. CEUR Workshop Proceedings, 2095.
Peer Reviewed verified by ORBi

Kirchner, D., Benzmüller, C., & Zalta, E. N. (2018). Mechanizing Principia Logico-Metaphysica in Functional Type Theory (Extended Abstract). In 3rd Conference on Artificial Intelligence and Theorem Proving (AITP 2018), Book of Abstracts.
Peer reviewed

Fuenmayor, D., & Benzmüller, C. (2018). A Case Study On Computational Hermeneutics: E. J. Lowe's Modal Ontological Argument. IfCoLog Journal of Logics and Their Applications, 5 (7), 1567-1603.
Peer reviewed

Fuenmayor, D., & Benzmüller, C. (2018). Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL. Archive of Formal Proofs.
Peer reviewed

Benzmüller, C., & Scott, D. S. (2018). Axiom Systems for Category Theory in Free Logic. Archive of Formal Proofs.
Peer reviewed

Benzmüller, C., & Scott, D. S. (2018). Some Reflections on a Computer-aided Theory Exploration Study in Category Theory (Extended Abstract). In 3rd Conference on Artificial Intelligence and Theorem Proving (AITP 2018), Book of Abstracts.
Peer reviewed

Benzmüller, C., Ricca, F., Parent, X., & Roman, D. (Eds.). (2018). Rules and Reasoning, Second International Joint Conference, RuleML+RR 2018, Luxembourg, Luxembourg, September 18-21, 2018, Proceedings. Springer. doi:10.1007/978-3-319-99906-7

Steen, A., & Benzmüller, C. (2018). The Higher-Order Prover Leo-III. In Automated Reasoning 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings (pp. 108-116). Springer, Cham. doi:10.1007/978-3-319-94205-6_8
Peer reviewed

Benzmüller, C., & Fuenmayor, D. (2018). Can Computers Help to Sharpen our Understanding of Ontological Arguments? In Mathematics and Reality, Proceedings of the 11th All India Students' Conference on Science Spiritual Quest, 6-7 October, 2018, IIT Bhubaneswar, Bhubaneswar, India (pp. 195-226). Kokata, India: The Bhaktivedanta Institute, Kolkata, www.binstitute.org. doi:10.13140/RG.2.2.31921.84323

Fuenmayor, D., & Benzmüller, C. (2018). Computational Hermeneutics: Using Computers to Interpret Philosophical Arguments (Abstract). In Logical Correctness, Workshop at UNILOG'2018, UNILOG'2018 Book of Abstracts (pp. 250-251). Vichy, France: Universit ́e Clermont Auvergne.
Peer reviewed

Benzmüller, C., & Parent, X. (2018). First Experiments with a Flexible Infrastructure for Normative Reasoning. ORBilu-University of Luxembourg. https://orbilu.uni.lu/handle/10993/37466.

Benzmüller, C., & Parent, X. (2018). I/O Logic in HOL --- First Steps. ORBilu-University of Luxembourg. https://orbilu.uni.lu/handle/10993/37467.

Benzmüller, C., Parent, X., & van der Torre, L. (2018). A Deontic Logic Reasoning Infrastructure. In Sailing Routes in the World of Computation, 14th Conference on Computability in Europe, CiE 2018, Kiel, Germany, July 30 – August 3, 2018, Proceedings (pp. 60-69). Springer. doi:10.1007/978-3-319-94418-0_6
Peer reviewed

Benzmüller, C. (2017). Recent Successes with a Meta-Logical Approach to Universal Logical Reasoning (Extended Abstract). In C. Benzmüller, Formal Methods: Foundations and Applications - 20th Brazilian Symposium SBMF 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings (pp. 7-11). Springer. doi:10.1007/978-3-319-70848-5_2

Kirchner, D., Benzmüller, C., & Zalta, E. N. (2017). Mechanizing Principia Logico-Metaphysica in Functional Type Theory. (v1). ORBilu-University of Luxembourg. https://orbilu.uni.lu/handle/10993/33700.

Benzmüller, C., Lisetti, C., & Theobald, M. (Eds.). (2017). GCAI 2017: 3rd Global Conference on Artificial Intelligence, Miami, FL, USA, 18-22 October 2017. EPiC Series in Computing, EasyChair.

Benzmüller, C., Lisetti, C., & Theobald, M. (Eds.). (2017). GCAI 2017. 3rd Global Conference on Artificial Intelligence. Manchester, United Kingdom: EasyChair Proceedings.

Benzmüller, C., & Fuenmayor, D. (2017). Computer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument. Archive of Formal Proofs.
Peer reviewed

Fuenmayor, D., & Benzmüller, C. (2017). Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic. In KI 2017: Advances in Artificial Intelligence 40th Annual German Conference on AI. Cham, Switzerland: Springer International Publishing AG. doi:10.1007/978-3-319-67190-1_9
Peer reviewed

Benzmüller, C., Farjami, A., Parent, X., & van der Torre, L. (06 July 2017). Implementation of Carmo and Jones Dyadic Deontic Logic in Isabelle/HOL [Paper presentation]. Workshop on Computational Aspects of Arguments and LogiC (CAALC 2017), Belgrade, Serbia.

Benzmüller, C., Steen, A., & Wisniewski, M. (2017). Leo-III Version 1.1 (System description). In IWIL Workshop and LPAR Short Presentations (pp. 16). Manchester, United Kingdom: EasyChair.
Peer reviewed

Steen, A., Wisniewski, M., & Benzmüller, C. (2017). Going Polymorphic - TH1 Reasoning for Leo-III. In IWIL Workshop and LPAR Short Presentations (pp. 13). Maun, Botswana, Unknown/unspecified: EasyChair.
Peer reviewed

Steen, A., Wisniewski, M., Schurr, H.-J., & Benzmüller, C. (2017). Capability Discovery for Automated Reasoning Systems. In IWIL Workshop and LPAR Short Presentations (pp. 6). Maun, Botswana, Unknown/unspecified: EasyChair.
Peer reviewed

Gleißner, T., Steen, A., & Benzmüller, C. (2017). Theorem Provers for Every Normal Modal Logic. In T. Eiter & D. Sands (Eds.), LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 14-30). Manchester, United Kingdom: EasyChair.
Peer reviewed

Fuenmayor, D., & Benzmüller, C. (2017). Types, Tableaus and Gödel's God in Isabelle/HOL. Archive of Formal Proofs.
Peer reviewed

Benzmüller, C. (2017). Universal Reasoning, Rational Argumentation and Human-Machine Interaction. (v1). ORBilu-University of Luxembourg. https://orbilu.uni.lu/handle/10993/33919.

Benzmüller, C., Weber, L., & Woltzenlogel Paleo, B. (23 February 2017). Computer-Assisted Analysis of the Anderson-Hájek Controversy. Logica Universalis, 11 (1), 139-151. doi:10.1007/s11787-017-0160-9
Peer reviewed

Benzmüller, C., & Woltzenlogel Paleo, B. (February 2017). Experiments in Computational Metaphysics: Gödel's Proof of God's Existence. Savijnanam: scientific exploration for a spiritual paradigm. Journal of the Bhaktivedanta Institute, 9, 43-57.
Peer reviewed

Fuenmayor, D., Benzmüller, C., Steen, A., & Wsinieswki, M. (2017). The Virtues of Automated Theorem Proving in Metaphysics --- A Case Study: E. J. Lowe's Modal Ontological Argument. In The 2nd World Congress on Logic and Religion -- Book of Abstracts (pp. 18). Warsaw, Poland: Instytut Filozofii Uniwersytetu Warszawskiego.
Peer reviewed

Benzmüller, C. (January 2017). Cut-Elimination for Quantified Conditional Logic. Journal of Philosophical Logic, 46 (3), 333–353. doi:10.1007/s10992-016-9403-0
Peer Reviewed verified by ORBi

Wisniewski, M., Steen, A., & Benzmüller, C. (2016). TPTP and Beyond: Representation of Quantified Non-Classical Logics. In C. Benzmüller & J. Otten (Eds.), ARQNL 2016. Automated Reasoning in Quantified Non-Classical Logics (pp. 51-65). CEUR-WS.org.
Peer reviewed

Steen, A., Wisniewski, M., & Benzmüller, C. (2016). Tutorial on Reasoning in Expressive Non-Classical Logics with Isabelle/HOL. In C. Benzmüller, G. Sutcliffe, ... R. Rojas (Eds.), GCAI 2016, 2nd Global Conference on Artificial Intelligence (pp. 1-10). Berlin,, Germany: EasyChair. doi:10.29007/4dsr
Peer reviewed

Steen, A., Wisniewski, M., & Benzmüller, C. (2016). Agent-Based HOL Reasoning. In G. Greuel, T. Koch, P. Paule, ... A. Sommese (Eds.), Mathematical Software -- ICMS 2016, 5th International Congress, Proceedings (pp. 75-81). Berlin, Germany, Unknown/unspecified: Springer. doi:10.1007/978-3-319-42432-3_10
Peer reviewed

Wisniewski, M., Steen, A., Kern, K., & Benzmüller, C. (2016). Effective Normalization Techniques for HOL. In N. Olivetti & A. Tiwari (Eds.), Automated Reasoning --- 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 -- July 2, 2016, Proceedings (pp. 362-370). Springer. doi:10.1007/978-3-319-40229-1_25
Peer reviewed

Steen, A., Wisniewski, M., & Benzmüller, C. (2016). Leo-III.

Wisniewski, M., Steen, A., & Benzmüller, C. (2016). Einsatz von Theorembeweisern in der Lehre. In A. Schwill & U. Lucke (Eds.), Hochschuldidaktik der Informatik: 7. Fachtagung des GI-Fachbereichs Informatik und Ausbildung/Didaktik der Informatik; 13.-14. September 2016 an der Universität Potsdam (pp. 81-92). Potsdam, Germany: Universitätsverlag Potsdam.
Peer reviewed

Steen, A., & Benzmüller, C. (2016). Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic. Logic and Logical Philosophy, 25 (4), 535-554. doi:10.12775/LLP.2016.021
Peer Reviewed verified by ORBi

Steen, A., & Benzmüller, C. (2015). There Is No Best Beta-Normalization Strategy for Higher-Order Reasoners. In M. Davis, A. Fehnker, A. McIver, ... A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) (pp. 329-339). Suva, Fiji, Unknown/unspecified: Springer. doi:10.1007/978-3-662-48899-7_23
Peer reviewed

Wisniewski, M., Steen, A., & Benzmüller, C. (2015). LeoPARD - A Generic Platform for the Implementation of Higher-Order Reasoners. In M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, ... V. Sorge (Eds.), Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings (pp. 325--330). Springer. doi:10.1007/978-3-319-20615-8_22
Peer reviewed

Benzmüller, C., Wisniewski, M., & Steen, A. (2015). Computational Metaphysics.

Wisniewski, M., Steen, A., & Benzmüller, C. (2014). The Leo-III Project. In A. Bolotov & M. Kerber (Eds.), Proceedings of the Joint Automated Reasoning Workshop and Deduktionstreffen: As part of the Vienna Summer of Logic – IJCAR 23-24 July 2014 (pp. 38).
Peer reviewed

Contact ORBilu