Keywords: LEO Prover
2017
[61] Capability Discovery for Automated Reasoning Systems (Alexander Steen, Max Wisniewski, Hans-Jörg Schurr, Christoph Benzmüller), In IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, Maun, Botswana, May 7-12, 2017 (Thomas Eiter, David Sands, Geoff Sutcliffe, Andrei Voronkov, eds.), EasyChair, Kalpa Publications in Computing, volume 1, 2017. [bibtex] [pdf]
[60] Going Polymorphic - TH1 Reasoning for Leo-III (Alexander Steen, Max Wisniewski, Christoph Benzmüller), In IWIL@LPAR 2017 Workshop and LPAR-21 Short < Presentations, Maun, Botswana, May 7-12, 2017 (Thomas Eiter, David Sands, Geoff Sutcliffe, Andrei Voronkov, eds.), EasyChair, Kalpa Publications in Computing, volume 1, 2017. [bibtex] [pdf]
[59] Leo-III Version 1.1 (System description) (Christoph Benzmüller, Alexander Steen, Max Wisniewski), In IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, Maun, Botswana, May 7-12, 2017 (Thomas Eiter, David Sands, Geoff Sutcliffe, Andrei Voronkov, eds.), EasyChair, Kalpa Publications in Computing, volume 1, 2017. [bibtex] [pdf]
[58] The Virtues of Automated Theorem Proving in Metaphysics --- A Case Study: E. J. Lowe's Modal Ontological Argument (David Fuenmayor, Christoph Benzmüller, Alexander Steen, Max Wisniewski), In Handbook of the 2nd World Congress on Logic and Religion, Warsaw, Poland (Stanislaw Krajewski, Piotr Balcerowicz, eds.), pp. 3, 2017. [bibtex] [pdf]
2016
[57] Automating Free Logic in Isabelle/HOL (Christoph Benzmüller, Dana Scott), In Mathematical Software -- ICMS 2016, 5th International Congress, Proceedings (G.-M. Greuel, T. Koch, P. Paule, A. Sommese, eds.), Springer, LNCS, volume 9725, pp. 43-50, 2016. [bibtex] [pdf] [doi]
[56] Agent-Based HOL Reasoning (Alexander Steen, Max Wisniewski, Christoph Benzmüller), In Mathematical Software -- ICMS 2016, 5th International Congress, Proceedings (G.-M. Greuel, T. Koch, P. Paule, A. Sommese, eds.), Springer, LNCS, volume 9725, pp. 75-81, 2016. [bibtex] [pdf] [doi]
[55] The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In IJCAI 2016 (Subbarao Kambhampati, ed.), AAAI Press, volume 1-3, pp. 936-942, 2016. (poster, proceedings-version) ((Acceptance rate $\leq 25\%$)) [bibtex] [pdf]
[54] Effective Normalization Techniques for HOL (Max Wisniewski, Alexander Steen, Kim Kern, Christoph Benzmüller), In Automated Reasoning --- 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 -- July 2, 2016, Proceedings (Nicola Olivetti, Ashish Tiwari, eds.), Springer, LNCS, volume 9706, pp. 362-370, 2016. [bibtex] [pdf] [doi]
[53] Is it Reasonable to Employ Agents in Theorem Proving? (Max Wisniewski, Christoph Benzmüller), In Proceedings of the 8th International Conference on Agents and Artificial Intelligence (ICAART 2016) -- Volume 1, pages 281-286 (Jan van den Heerik, Joaquim Filipe, eds.), SCITEPRESS -- Science and Technology Publications, Lda, volume 1, pp. 281-286, 2016. [bibtex] [pdf] [doi]
2015
[52] HOL Provers for First-order Modal Logics --- Experiments (Christoph Benzmüller), In ARQNL 2014. Automated Reasoning in Quantified Non-Classical Logics (Christoph Benzmüller, Jens Otten, eds.), EasyChair, EPiC Series in Computing, volume 33, pp. 37-41, 2015. [bibtex] [pdf]
[51] The Higher-Order Prover LEO-II (Christoph Benzmüller, Nik Sultana, Lawrence C. Paulson, Frank Theiß), In Journal of Automated Reasoning, volume 55, number 4, pp. 389-404, 2015. [bibtex] [pdf] [doi]
[50] There Is No Best Beta-Normalization Strategy for Higher-Order Reasoners (Alexander Steen, Christoph Benzmüller), In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) (M. Davis, A. Fehnker, A. McIver, A. Voronkov, eds.), Springer, LNAI, volume 9450, pp. 329-339, 2015. [bibtex] [pdf] [doi]
[49] Proofs and reconstructions (Nik Sultana, Christoph Benzmüller, Lawrence C. Paulson), In FroCoS 2015 (Carsten Lutz, Silvio Ranise, eds.), Springer, LNAI, volume 9322, pp. 256-271, 2015. [bibtex] [pdf] [doi]
[48] Systematic Verification of the Modal Logic Cube in Isabelle/HOL (Christoph Benzmüller, Maximilian Claus, Nik Sultana), In PxTP 2015 (Cezary Kaliszyk, Andrei Paskevich, eds.), EPTCS, volume 186, pp. 27-41, 2015. (slides) [bibtex] [pdf] [doi]
[47] Higher-Order Modal Logics: Automation and Applications (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In Reasoning Web 2015 (Adrian Paschke, Wolfgang Faber, eds.), Springer, LNCS, number 9203, pp. 32-74, 2015. ((Invited paper)) [bibtex] [pdf] [doi]
[46] LeoPARD - A Generic Platform for the Implementation of Higher-Order Reasoners (Max Wisniewski, Alexander Steen, Christoph Benzmüller), In Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings (Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, Volker Sorge, eds.), Springer, LNCS, volume 9150, pp. 325--330, 2015. [bibtex] [pdf] [doi]
[45] Interacting with Modal Logics in the Coq Proof Assistant (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In Computer Science - Theory and Applications - 10th International Computer Science Symposium in Russia, CSR 2015, Listvyanka, Russia, July 13-17, 2015, Proceedings (Lev D. Beklemishev, Daniil V. Musatov, eds.), Springer, LNCS, volume 9139, pp. 398--411, 2015. [bibtex] [pdf] [doi]
[44] Gödel's Ontological Argument Revisited -- Findings from a Computer-supported Analysis (invited) (Christoph Benzmüller), In Handbook of the 1st World Congress on Logic and Religion, João Pessoa, Brazil (Ricardo Souza Silvestre, Jean-Yves Béziau, eds.), pp. 13, 2015. ((Invited abstract)) [bibtex] [pdf]
[43] Computer-Assisted Analysis of the Anderson-Hájek Ontological Controversy (Christoph Benzmüller, Leon Weber, Bruno Woltzenlogel Paleo), In Handbook of the 1st World Congress on Logic and Religion, Joao Pessoa, Brasil (Ricardo Souza Silvestre, Jean-Yves Béziau, eds.), pp. 53-54, 2015. ((superseded by 2016 article in Logica Universalis)) [bibtex] [pdf]
2014
[42] The Leo-III Project (Max Wisniewski, Alexander Steen, Christoph Benzmüller), In Joint Automated Reasoning Workshop and Deduktionstreffen (Alexander Bolotov, Manfred Kerber, eds.), pp. 38, 2014. [bibtex] [pdf]
[41]Modal Logic in Coq and Scott's Version of Gödel's Proof of God's Existence (Rough Diamond Proof Pearl) (Christoph Benzmüller, Bruno Woltzenlogel Paleo), 2014. ((Non-reviewed, superseded by CSR-2015 paper)) [bibtex]
[40] Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In ECAI 2014 (Torsten Schaub, Gerhard Friedrich, Barry O'Sullivan, eds.), IOS Press, Frontiers in Artificial Intelligence and Applications, volume 263, pp. 93 -- 98, 2014. (slides) ((Acceptance rate $\leq 28\%$)) [bibtex] [pdf] [doi]
[39] Gödel's Proof of God's Existence (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In Handbook of the World Congress on the Square of Opposition IV (Jean-Yves Beziau, Katarzyna Gan-Krzywoszynska, eds.), pp. 22-23, 2014. ((superseded by ECAI-2014 paper)) [bibtex] [pdf]
2013
[38] LEO-II Version 1.5 (Christoph Benzmüller, Nik Sultana), In PxTP 2013 (Jasmin Christian Blanchette, Josef Urban, eds.), EasyChair, EPiC Series in Computing, volume 14, pp. 2-10, 2013. [bibtex] [pdf]
[37] Gödel's God on the Computer (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In Proceedings of the 10th International Workshop on the Implementation of Logics (S. Schulz, G. Sutcliffe, B. Konev, eds.), 2013. (event-website) ((Invited paper)) [bibtex] [pdf]
[36] Automated Consistency Checking of Expressive Ontologies --- Beware of the Wrong Interpretation of Success! (Christoph Benzmüller, Marco Ziener), In The 5th International Workshop on Acquisition, Representation and Reasoning with Contextualized Knowledge (ARCOE-LogIC 2013) (Michael Fink, Martin Homola, Alessandra Mileo, Ivan Jose Varzinczak, eds.), 2013. [bibtex] [pdf]
[35] Understanding LEO-II's Proofs (Nik Sultana, Christoph Benzmüller), In IWIL 2012 (Konstantin Korovin, Stephan Schulz, Eugenia Ternovska, eds.), EasyChair, EPiC Series in Computing, volume 22, pp. 33-52, 2013. [bibtex] [pdf]
[34] Formalization, Mechanization and Automation of Gödel's Proof of God's Existence (Christoph Benzmüller, Bruno Woltzenlogel Paleo), 2013. (complete-formalisation) ((not reviewed, superseded by ECAI-2014 paper)) [bibtex] [pdf]
[33]Automated Verification and Reconstruction of Gödel's Proof of God's Existence (Bruno Woltzenlogel Paleo, Christoph Benzmüller), In OCG Journal, 2013. ((Invited article)) [bibtex]
[32] Gödel's God in Isabelle/HOL (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In Archive of Formal Proofs, 2013. (This publication is formally verified with Isabelle/HOL) [bibtex] [pdf]
[31] Automating Quantified Conditional Logics in HOL (Christoph Benzmüller), In 23rd International Joint Conference on Artificial Intelligence (IJCAI-13) (Francesca Rossi, ed.), AAAI Press, pp. 746-753, 2013. (poster) [bibtex] [pdf]
[30] HOL based Universal Reasoning (Christoph Benzmüller), In Handbook of the 4th World Congress and School on Universal Logic (J.Y. Beziau, A. Buchsbaum, A. Costa-Leite, A. Altair, eds.), pp. 232-233, 2013. (slides) ((Superseded by ICAART-2013 paper)) [bibtex] [pdf]
2012
[29] FMLtoHOL (version 1.0): Automating First-order Modal Logics with LEO-II and Friends (Christoph Benzmüller, Thomas Raths), Technical report, Freie Universität Berlin, Germany, 2012. (arXiv:1207.6685) [bibtex] [pdf]
2010
[28] Multimodal and Intuitionistic Logics in Simple Type Theory (Christoph Benzmüller, Lawrence Paulson), In The Logic Journal of the IGPL, volume 18, number 6, pp. 881-892, 2010. [bibtex] [pdf] [doi]
[27] Simple Type Theory as Framework for Combining Logics (Christoph Benzmüller), In Contest paper at the World Congress and School on Universal Logic III (UNILOG), 2010. (slides) (The conference had no published proceedings; the paper is available as arXiv:1004.5500v1) [bibtex] [pdf]
[26] Verifying the Modal Logic Cube is an Easy Task (for Higher-Order Automated Reasoners) (Christoph Benzmüller), Chapter in Verification, Induction, Termination Analysis - Festschrift for Christoph Walther on the Occasion of His 60th Birthday (Simon Siegler, Nathan Wasser, eds.), Springer, LNCS, volume 6463, pp. 117-128, 2010. ((Superseded by PxTP-2015 paper)) [bibtex] [pdf] [doi]
2009
[25] A Note on LEO-II and the Basic Fragment of Simple Type Theory (Christoph Benzmüller), Technical report, AAR Newsletter No. 84, 2009. [bibtex] [pdf]
[24] Effective Higher-Order Automated Theorem Proving with integrated Descente Infinie and Presburger Arithmetic LEO-III (Christoph Benzmüller, Claus-Peter Wirth), 2009. [bibtex] [pdf]
[23] LEO-II im Ontologieschliessen -- Antrag auf ein Forschungsvorhaben an die DFG (Christoph Benzmüller), 2009. [bibtex] [pdf]
[22] Automating Access Control Logic in Simple Type Theory with LEO-II (Christoph Benzmüller), In Emerging Challenges for Security, Privacy and Trust, 24th IFIP TC 11 International Information Security Conference, SEC 2009, Pafos, Cyprus, May 18-20, 2009. Proceedings (Dimitris Gritzalis, Javier López, eds.), Springer, IFIP, volume 297, pp. 387-398, 2009. (slides) [bibtex] [pdf] [doi]
2008
[21] Automating Access Control Logics in Simple Type Theory with LEO-II (Christoph Benzmüller), SEKI Publications (ISSN 1437-4447), number SR-2008-01, 2008. (arXiv:0901.3574) [bibtex] [pdf]
[20] Combined Reasoning by Automated Cooperation (Christoph Benzmüller, Volker Sorge, Mateja Jamnik, Manfred Kerber), In Journal of Applied Logic, volume 6, number 3, pp. 318-342, 2008. [bibtex] [pdf] [doi]
[19] LEO-II - A Cooperative Automatic Theorem Prover for Higher-Order Logic (System Description) (Christoph Benzmüller, Frank Theiss, Lawrence Paulson, Arnaud Fietzke), In Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings (Alessandro Armando, Peter Baumgartner, Gilles Dowek, eds.), Springer, LNCS, volume 5195, pp. 162-170, 2008. (slides) [bibtex] [pdf] [doi]
[18] Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II (Christoph Benzmüller, Lawrence Paulson), Chapter in Reasoning in Simple Type Theory --- Festschrift in Honor of Peter B. Andrews on His 70th Birthday (Christoph Benzmüller, Chad Brown, Jörg Siekmann, Richard Statman, eds.), College Publications, Studies in Logic, Mathematical Logic and Foundations, pp. 386-406, 2008. ((Superseded by 2013 article in Logica Universalis)) [bibtex] [pdf]
2007
[17] Progress Report on LEO-II -- An Automatic Theorem Prover for Higher-Order Logic (Christoph Benzmüller, Lawrence Paulson, Frank Theiss, Arnaud Fietzke), In TPHOLs 2007 Emerging Trends Proceedings, Internal Report 364/07 at Department of Computer Science, pp. 33-48, 2007. (slides) [bibtex] [pdf]
[16] The LEO-II Project (Christoph Benzmüller, Lawrence Paulson, Frank Theiss, Arnaud Fietzke), In Proceedings of the Fourteenth Workshop on Automated Reasoning, Bridging the Gap between Theory and Practice, Imperial College, London, England, 2007. ((Mildly reviewed)) [bibtex] [pdf]
2006
[15] Term Indexing for the LEO-II Prover (Frank Theiss, Christoph Benzmüller), In IWIL-6 workshop at LPAR 2006: The 6th International Workshop on the Implementation of Logics, 2006. (slides) [bibtex] [pdf]
[14] Cumulative Habilitation Script (Christoph Benzmüller), Saarland University, Germany, pp. 1-357, 2006. [bibtex] [pdf]
2005
[13] System Description: LEO -- A Resolution based Higher-Order Theorem Prover (Christoph Benzmüller), In Proceedings of the LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL), pp. 25-44, 2005. (arXiv:cs/0601042) [bibtex] [pdf]
[12] Can a Higher-Order and a First-Order Theorem Prover Cooperate? (Christoph Benzmüller, Volker Sorge, Mateja Jamnik, Manfred Kerber), In Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings (Franz Baader, Andrei Voronkov, eds.), Springer, LNCS, number 3452, pp. 415-431, 2005. (slides) [bibtex] [pdf] [doi]
2003
[11] Semantic Techniques for Cut-Elimination in Higher Order Logic. (Christoph Benzmüller, Chad Brown, Michael Kohlhase), Technical report, Saarland University, Saarbrücken, Germany and Carnegie Mellon University, Pittsburgh, USA, 2003. [bibtex] [pdf]
[10] Higher Order Semantics and Extensionality. (Christoph Benzmüller, Chad Brown, Michael Kohlhase), Technical report, Carnegie Mellon University, Pittsburgh, PA, number CMU-01-03, pp. 1-74, 2003. [bibtex] [pdf]
2002
[9] Comparing Approaches to Resolution based Higher-Order Theorem Proving (Christoph Benzmüller), In Synthese, volume 133, number 1-2, pp. 203-235, 2002. [bibtex] [pdf] [doi]
2001
[8] OANTS -- Combining Interactive and Automated Theorem Proving (Christoph Benzmüller, Volker Sorge), In Symbolic Computation and Automated Reasoning (Manfred Kerber, Michael Kohlhase, eds.), A.K.Peters, pp. 81-97, 2001. (slides) [bibtex] [pdf]
[7] Experiments with an Agent-oriented Reasoning system (Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge), In KI 2001: Advances in Artificial Intelligence, Joint German/Austrian Conference on AI, Vienna, Austria, September 19-21, 2001, Proceedings (Franz Baader, Gerhard Brewka, Thomas Eiter, eds.), Springer, LNCS, number 2174, pp. 409-424, 2001. (slides) [bibtex] [pdf] [doi]
2000
[6] Resource Guided Concurrent Deduction (Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge), In Symbolic Computation and Automated Reasoning (Manfred Kerber, Michael Kohlhase, eds.), A.K.Peters, pp. 245-246, 2000. [bibtex] [pdf]
1999
[5] Equality and Extensionality in Higher-Order Theorem Proving (Christoph Benzmüller), PhD thesis, Naturwissenschaftlich-Technische Fakultät I, Saarland University, Saarbrücken, Germany, pp. 1-174, 1999. [bibtex] [pdf]
[4] Equality and Extensionality in Higher-Order Theorem Proving (Christoph Benzmüller), Technical report, Saarland University, SEKI Publications (ISSN 1437-4447), number SR-99-08, pp. 1-139, 1999. [bibtex] [pdf]
[3] Critical Agents Supporting Interactive Theorem Proving (Christoph Benzmüller, Volker Sorge), In Progress in Artificial Intelligence, 9th Portuguese Conference on Artificial Intelligence, EPIA '99, Évora, Portugal, September 21-24, 1999, Proceedings (Pedro Borahona, Jose J. Alferes, eds.), Springer, LNCS, number 1695, pp. 208-221, 1999. (slides) [bibtex] [pdf] [doi]
1998
[2] LEO -- A Higher-Order Theorem Prover (Christoph Benzmüller, Michael Kohlhase), In Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings (Claude Kirchner, Hélène Kirchner, eds.), Springer, LNCS, number 1421, pp. 139-143, 1998. (slides) [bibtex] [pdf] [doi]
[1] Extensional Higher-Order Resolution (Christoph Benzmüller, Michael Kohlhase), In Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings (Claude Kirchner, Hélène Kirchner, eds.), Springer, LNAI, number 1421, pp. 56-71, 1998. [bibtex] [pdf] [doi]
Powered by bibtexbrowser