Type: Inproceedings
2017
[124]Implementation of Carmo and Jones Dyadic Deontic Logic in Isabelle/HOL (Christoph Benzmüller, Ali Farjami, Xavier Parent, Leon van der Torre), In Workshop on Computational Aspects of Arguments and LogiC (CAALC 2017), 2017. [bibtex]
[123] 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]
[122] 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]
[121] Recent Successes with a Meta-Logical Approach to Universal Logical Reasoning (Extended Abstract) (Christoph Benzmüller), In Formal Methods: Foundations and Applications - 20th Brazilian Symposium, SBMF 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings (Simone André da Costa Cavalheiro, José Luiz Fiadeiro, eds.), Springer, Lecture Notes in Computer Science, volume 10623, pp. 7--11, 2017. [bibtex] [pdf]
[120] Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic (David Fuenmayor, Christoph Benzmüller), In KI 2017: Advances in Artificial Intelligence 40th Annual German Conference on AI, Springer, LNAI, 2017. [bibtex] [pdf]
[119] 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]
[118] 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]
[117] Theorem Provers for Every Normal Modal Logic (Tobias Gleißner, Alexander Steen, Christoph Benzmüller), In LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (Thomas Eiter, David Sands, eds.), EasyChair, EPiC Series in Computing, volume 46, pp. 14-30, 2017. [bibtex] [pdf]
2016
[116] TPTP and Beyond: Representation of Quantified Non-Classical Logics (Max Wisniewski, Alexander Steen, Christoph Benzmüller), In ARQNL 2016. Automated Reasoning in Quantified Non-Classical Logics (Christoph Benzmüller, Jens Otten, eds.), CEUR Workshop Proceedings, http://ceur-ws.org, volume 1770, pp. 51-65, 2016. [bibtex] [pdf]
[115] Tutorial on Reasoning in Expressive Non-Classical Logics with Isabelle/HOL (Alexander Steen, Max Wisniewski, Christoph Benzmüller), In GCAI 2016, 2nd Global Conference on Artificial Intelligence (Christoph Benzüller, Raul Rojas, Geoff Sutcliffe, eds.), EasyChair, EPiC Series in Computing, volume 41, pp. 1-10, 2016. [bibtex] [pdf]
[114] An Object-Logic Explanation for the Inconsistency in Gödel's Ontological Theory (Extended Abstract, Sister Conferences) (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In KI 2016: Advances in Artificial Intelligence, Proceedings (Malte Helmert, Franz Wotawa, eds.), Springer, LNCS, pp. 244-250, 2016. [bibtex] [pdf] [doi]
[113] Translating Higher-Order Modal Logic from RuleML to TPTP (Harold Boley, Christoph Benzmüller, Meng Luan, Zhendong Sha), In 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) (A. Giurca, W. Van Woensel, R. Grütter, K. Teymourian, T. Athan, M. Proctor, eds.), CEUR-WS.org, CEUR Workshop Proceedings, volume Vol-1620, 2016. [bibtex] [pdf]
[112] Einsatz von Theorembeweisern in der Lehre (Max Wisniewski, Alexander Steen, Christoph Benzmüller), In Hochschuldidaktik der Informatik: 7. Fachtagung des GI-Fachbereichs Informatik und Ausbildung/Didaktik der Informatik; 13.-14. September 2016 an der Universität Potsdam (Andreas Schwill, Ulrike Lucke, eds.), Universitätsverlag Potsdam, Commentarii informaticae didacticae (CID), 2016. [bibtex] [pdf]
[111] 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]
[110] 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]
[109] 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]
[108] 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]
[107] 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
[106] On Logic Embeddings and Gödel's God (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In Recent Trends in Algebraic Development Techniques: 22nd International Workshop, WADT 2014, Sinaia, Romania, September 4-7, 2014, Revised Selected Papers (Mihai Codescu, Razvan Diaconescu, Ionut Tutu, eds.), Springer, LNCS, number 9563, pp. 3-6, 2015. ((Invited paper)) [bibtex] [pdf] [doi]
[105] 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]
[104] Experiments in Computational Metaphysics: Gödel's Proof of God's Existence (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In Science & Spiritual Quest, Proceedings of the 9th All India Students' Conference, 30th October -- 1 November, 2015, IIT Kharagpur, India (Subhash C. Mishram, Ramgopal Uppaluri, Varun Agarwal, eds.), Bhaktivedanta Institute, Kolkata, www.binstitute.org, pp. 23-40, 2015. (slides) ((Invited paper)) [bibtex] [pdf]
[103] 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]
[102] Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics (Christoph Benzmüller), In TABLEAUX 2015 (Hans De Nivelle, ed.), Springer, LNAI, volume 9323, pp. 213-220, 2015. ((Invited paper)) [bibtex] [pdf] [doi]
[101] Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic (Alexander Steen, Christoph Benzmüller), In 7th International Conference Non-Classical Logic -- Theory and Applications, Torun, Poland, 2015. [bibtex] [pdf]
[100] 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]
[99] 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]
[98] 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]
[97] 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]
[96] 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]
[95] 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]
[94] 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
[93] 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]
[92] 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]
[91] 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
[90] 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]
[89] Cut-free Calculi for Challenge Logics in a Lazy Way (Christoph Benzmüller), In Proceedings of the International Workshop on Algebraic Logic in Computer Science (Petr Cintula Carles Noguera Clint van Alten, ed.), 2013. (event-website) [bibtex] [pdf]
[88] 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]
[87] 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]
[86] Implementing Different Proof Calculi for First-order Modal Logics (Christoph Benzmüller, Jens Otten, Thomas Raths), In PAAR-2012 (Pascal Fontaine, Renate A. Schmidt, Stephan Schulz, eds.), EasyChair, EPiC Series in Computing, volume 21, pp. 12-18, 2013. [bibtex] [pdf]
[85] 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]
[84] HOL based First-order Modal Logic Provers (Christoph Benzmüller, Thomas Raths), In Proceedings of the 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) (Kenneth L. McMillan, Aart Middeldorp, Andrei Voronkov, eds.), Springer, LNCS, volume 8312, pp. 127-136, 2013. [bibtex] [pdf] [doi]
[83] 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]
[82] 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]
[81] A Top-down Approach to Combining Logics (Christoph Benzmüller), In Proc. of the 5th International Conference on Agents and Artificial Intelligence (ICAART) (Joaquim Filipe, Ana Fred, eds.), SCITEPRESS -- Science and Technology Publications, Lda, volume 1, pp. 346-351, 2013. (slides) [bibtex] [pdf] [doi]
2012
[80] Adaptive Assertion-Level Proofs (Christoph Benzmüller, Marvin Schiller), In EMSQMS 2010 -- Workshop on Evaluation Methods for Solvers and Quality Metrics for Solutions (Aaron Stump, Geoff Sutcliffe, Cesare Tinelli, eds.), EasyChair, EPiC Series in Computing, volume 6, pp. 39-40, 2012. [bibtex] [pdf]
[79] Progress in Automating Higher-Order Ontology Reasoning (Christoph Benzmüller, Adam Pease), In PAAR-2010 -- Workshop on Practical Aspects of Automated Reasoning (Renate A. Schmidt, Stephan Schulz, Boris Konev, eds.), EasyChair, EPiC Series in Computing, volume 9, pp. 22-32, 2012. (slides) [bibtex] [pdf]
[78] Implementing and Evaluating Provers for First-order Modal Logics (Christoph Benzmüller, Jens Otten, Thomas Raths), In ECAI 2012 (Luc De Raedt, Christian Bessiere, Didier Dubois, Patrick Doherty, Paolo Frasconi, Fredrik Heintz, Peter Lucas, eds.), IOS Press, Frontiers in Artificial Intelligence and Applications, volume 242, pp. 163-168, 2012. (slides) [bibtex] [pdf] [doi]
2011
[77] Quantified Conditional Logics are Fragments of HOL (Christoph Benzmüller, Valerio Genovese), In The International Conference on Non-classical Modal and Predicate Logics (NCMPL), 2011. ([slides], [movie]) ((The conference had no published proceedings; the paper is available as arXiv:1204.5920v1; superseded by IJCAI-2013 paper)) [bibtex] [pdf]
2010
[76] Human-Oriented Proof Techniques are Relevant for Proof Tutoring (Marvin Schiller, Christoph Benzmüller), In Workshop on Mathematically Intelligent Proof Search (MIPS 2010, affiliated with CICM 2010), 2010. [bibtex] [pdf]
[75] Reasoning with Embedded Formulas and Modalities in SUMO (Christoph Benzmüller, Adam Pease), In The ECAI-10 Workshop on Automated Reasoning about Context and Ontology Evolution (ARCOE-10) (A. Bundy, J. Lehmann, G. Qi, I. J. Varzinczak, eds.), 2010. (slides) ((Superseded by 2012 article in Journal of Web Semantics)) [bibtex] [pdf]
[74] Ontology Archaeology: Mining a Decade of Effort on the Suggested Upper Merged Ontology (Adam Pease, Christoph Benzmüller), In The ECAI-10 Workshop on Automated Reasoning about Context and Ontology Evolution (ARCOE-10) (A. Bundy, J. Lehmann, G. Qi, I. J. Varzinczak, eds.), 2010. (slides) [bibtex] [pdf]
[73] Sigma: An Integrated Development Environment for Logical Theory Development (Adam Pease, Christoph Benzmüller), In The ECAI 2010 Workshop on Intelligent Engineering Techniques for Knowledge Bases (IKBET'2010), 2010. (slides) ((Superseded by 2013 article in AI Communications)) [bibtex] [pdf]
[72] Combining Logics in Simple Type Theory (Christoph Benzmüller), In Computational Logic in Multi-Agent Systems, 11th International Workshop, CLIMA XI, Lisbon, Portugal, August 16-17, 2010. Proceedings (Jürgen Dix, Joao Leite, Guido Governatori, Woitek Jamroga, eds.), Springer, Lecture Notes in Artifical Intelligence, volume 6245, pp. 33-48, 2010. [bibtex] [pdf] [doi]
[71] 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]
2009
[70] Presenting Proofs with Adapted Granularity (Marvin Schiller, Christoph Benzmüller), In KI 2009: Advances in Artificial Intelligence, 32nd Annual German Conference on AI, Paderborn, Germany, September 15-18, 2009. Proceedings (Bärbel Mertsching, Marcus Hund, Muhammad Zaheer Aziz, eds.), Springer, LNAI, volume 5803, pp. 289-297, 2009. [bibtex] [pdf] [doi]
[69] Granularity-Adaptive Proof Presentation (Marvin Schiller, Christoph Benzmüller), In 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, IOS Press, Frontiers in Artificial Intelligence and Applications, volume 200, pp. 599-601, 2009. [bibtex] [pdf]
[68] Progress in the Development of Automated Theorem Proving for Higher-order Logic (Geoff Sutcliffe, Christoph Benzmüller, Chad Brown, Frank Theiss), In Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings (Renate Schmidt, ed.), Springer, LNCS, volume 5663, pp. 116-130, 2009. [bibtex] [pdf] [doi]
[67] Proof Granularity as an Empirical Problem? (Marvin Schiller, Christoph Benzmüller), In CSEDU 2009 - Proceedings of the First International Conference on Computer Supported Education, Lisboa, Portugal, March 23-26, 2009 - Volume 1 (José A. Moinhos Cordeiro, Boris Shishkov, Alexander Verbraeck, Markus Helfert, eds.), SciTePress Digital Library, pp. 350-354, 2009. [bibtex] [pdf] [doi]
[66] 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
[65] Evaluation of Systems for Higher-order Logic (ESHOL) (Christoph Benzmüller, Florian Rabe, Carsten Schürmann, Geoff Sutcliffe), In Proceedings of the First International Workshop on Practical Aspects of Automated Reasoning, Sydney, Australia, August 10-11, 2008 (Boris Konev, Renate A. Schmidt, Stephan Schulz, eds.), CEUR-WS.org, CEUR Workshop Proceedings, volume 373, 2008. ((Invited non-reviewed paper)) [bibtex] [pdf]
[64] 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]
[63] THF0 -- The Core of the TPTP Language for Classical Higher-Order Logic (Christoph Benzmüller, Florian Rabe, Geoff Sutcliffe), 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. 491-506, 2008. [bibtex] [pdf] [doi]
2007
[62] Towards Computer-Assisted Proof Tutoring (Marvin Schiller, Dominik Dietrich, Christoph Benzmüller), In JEM Workshop on identifying and supporting (scientific) communities in education and research, 2007. ((Mildly reviewed)) [bibtex] [pdf]
[61] 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]
[60] 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]
[59] Deep Inference for Automated Proof Tutoring? (Christoph Benzmüller, Dominik Dietrich, Marvin Schiller, Serge Autexier), In KI 2007: Advances in Artificial Intelligence, 30th Annual German Conference on AI, KI 2007, Osnabrück, Germany, September 10-13, 2007, Proceedings (Joachim Hertzberg, Michael Beetz, Roman Englert, eds.), Springer, volume 4667, pp. 435-439, 2007. [bibtex] [pdf] [doi]
[58] DiaWOz-II - A Tool for Wizard-of-Oz Experiments in Mathematics (Christoph Benzmüller, Helmut Horacek, Henri Lesourd, Ivana Kruijff-Korbayova, Marvin Schiller, Magdalena Wolska), In KI 2006: Advances in Artificial Intelligence, 29th Annual German Conference on AI, KI 2006, Bremen, Germany, June 14-17, 2006, Proceedings (Christian Freksa, Michael Kohlhase, Kerstin Schill, eds.), Springer, LNCS, volume 4314, pp. 159-173, 2007. [bibtex] [pdf] [doi]
[57] An Agent-based Architecture for Dialogue Systems (Mark Buckley, Christoph Benzmüller), In Perspectives of Systems Informatics, 6th International Andrei Ershov Memorial Conference, PSI 2006, Novosibirsk, Russia, June 27-30, 2006. Revised Papers (Irina Virbitskaite, Andrei Voronkov, eds.), Springer, LNCS, volume 4378, pp. 135-147, 2007. [bibtex] [pdf] [doi]
2006
[56] 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]
[55] Judging Granularity for Automated Mathematics Teaching (Marvin Schiller, Christoph Benzmüller, Ann van de Veire), In Short papers at LPAR 2006: 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning, 2006. (slides) [bibtex] [pdf]
[54] Granularity Judgments in Proof Tutoring (Marvin Schiller, Christoph Benzmüller), In Poster papers at KI 2006: Advances in Artificial Intelligence: 29th Annual German Conference on AI, 2006. [bibtex] [pdf]
[53] Cut-Simulation in Impredicate Logics (Christoph Benzmüller, Chad Brown, Michael Kohlhase), In Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings (Ulrich Furbach, Natarajan Shankar, eds.), Springer, LNCS, volume 4130, pp. 220-234, 2006. (slides) [bibtex] [pdf] [doi]
[52] A corpus of tutorial dialogs on theorem proving; the influence of the presentation of the study-material (Christoph Benzmüller, Helmut Horacek, Henri Lesourd, Ivana Kruijff-Korbayova, Marvin Schiller, Magdalena Wolska), In Proceedings of International Conference on Language Resources and Evaluation (LREC 2006), ELDA, 2006. [bibtex] [pdf]
[51] A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity (Serge Autexier, Christoph Benzmüller, Dominik Dietrich, Andreas Meier, Claus-Peter Wirth), In Mathematical Knowledge Management, 4th International Conference, MKM 2005, Bremen, Germany, July 15-17, 2005, Revised Selected Papers (Michael Kohlhase, ed.), Springer, LNCS, volume 3863, pp. 126-142, 2006. [bibtex] [pdf] [doi]
2005
[50] Combining Proofs of Higher-Order and First-Order Automated Theorem Provers (Christoph Benzmüller, Volker Sorge, Mateja Jamnik, Manfred Kerber), In Proceedings of the LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL), pp. 45-58, 2005. (arXiv:cs/0601042) [bibtex] [pdf]
[49] 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]
[48] Integrating Proof Assistants as Reasoning and Verification Tools into a Scientific WYSIWIG Editor (Mark Buckley, Christoph Benzmüller), In Proceedings of the ETAPS Satellite Workshop on User Interfaces for Theorem Provers (UITP), pp. 16-39, 2005. [bibtex] [pdf]
[47] System Description: A Dialog Manager supporting Tutorial Natural Language Dialogue on Proofs (Mark Buckley, Christoph Benzmüller), In Proceedings of the ETAPS Satellite Workshop on User Interfaces for Theorem Provers (UITP), pp. 40-67, 2005. [bibtex] [pdf]
[46] Mathematical Domain Reasoning Tasks in Natural Language Tutorial Dialog on Proofs (Christoph Benzmüller, Bao Quoc Vo), In Proceedings, The Twentieth National Conference on Artificial Intelligence and the Seventeenth Innovative Applications of Artificial Intelligence Conference, July 9-13, 2005, Pittsburgh, Pennsylvania, USA (Manuela Veloso, Subbarao Kambhampati, eds.), AAAI Press / The MIT Press, pp. 516-522, 2005. (slides) [bibtex] [pdf]
[45] A Structured Set of Higher-Order Problems (Christoph Benzmüller, Chad Brown), In Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings (Joe Hurd, Thomas F. Melham, eds.), Springer, LNCS, number 3603, pp. 66-81, 2005. [bibtex] [pdf] [doi]
[44] 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]
2004
[43] OMEGA: Computer Supported Mathematics (Jörg Siekmann, Christoph Benzmüller), In KI 2004: Advances in Artificial Intelligence, 27th Annual German Conference on AI, KI 2004, Ulm, Germany, September 20-24, 2004, Proceedings (Susanne Biundo, Thom W. Frühwirth, Günther Palm, eds.), LNCS, number 3228, pp. 3-28, 2004. [bibtex] [pdf] [doi]
[42] An annotated corpus of tutorial dialogs on mathematical theorem proving (Magdalena Wolska, Bao Quoc Vo, Dimitra Tsovaltzi, Ivana Kruijff-Korbayova, Elena Karagjosova, Helmut Horacek, Malte Gabsdil, Armin Fiedler, Christoph Benzmüller), In Proceedings of International Conference on Language Resources and Evaluation (LREC 2004), ELDA, 2004. [bibtex] [pdf]
2003
[41] OMEGA --- From Proof Planning towards Mathematical Knowledge Management (Serge Autexier, Christoph Benzmüller), In Mathematical Knowledge Management Symposium, 2003. (slides) [bibtex] [pdf]
[40] Towards a Principled Approach to Tutoring Mathematical Proofs (Christoph Benzmüller, Armin Fiedler, Malte Gabsdil, Helmut Horacek, Ivana Kruijff-Korbayova, Dimitra Tsovaltzi, Bao Quoc Vo, Magdalena Wolska), In Proceedings of the Workshop on Expressive Media and Intelligent Tools for Learning, German Conference on AI (KI 2003), 2003. [bibtex] [pdf]
[39] Language Phenomena in Tutorial Dialogs on Mathematical Proofs (Christoph Benzmüller, Armin Fiedler, Malte Gabsdil, Helmut Horacek, Ivana Kruijff-Korbayova, Dimitra Tsovaltzi, Bao Quoc Vo, Magdalena Wolska), In Proceedings of the 7th Workshop on the semantics and pragmatics of dialogue (DiaBruck), 2003. [bibtex] [pdf]
[38] Interactive Proof Construction at the Task Level (Malte Hübner, Christoph Benzmüller, Serge Autexier, Andreas Meier), In Proceedings of the Workshop User Interfaces for Theorem Provers (UITP 2003), ARACNE EDITRICE S.R.L. (ISBN 88-7999-545-6), pp. 81-100, 2003. (Also available as: Technical Report No. 189, Institut für Informatik, Albert-Ludwig-Universität, Freiburg) [bibtex] [pdf]
[37] A Wizard of Oz Experiment for Tutorial Dialogues in Mathematics (Christoph Benzmüller, Armin Fiedler, Malte Gabsdil, Helmut Horacek, Ivana Kruijff-Korbayova, Manfred Pinkal, Jörg Siekmann, Dimitra Tsovaltzi, Bao Quoc Vo, Magdalena Wolska), In Proceedings of AI in Education (AIED 2003) Workshop on Advanced Technologies for Mathematics Education, 2003. [bibtex] [pdf]
[36] The CALCULEMUS research training network: A short overview (Christoph Benzmüller), In Proceedings of the First QPQ Workshop on Deductive Software Components at CADE-19, pp. 13-27, 2003. (slides) [bibtex] [pdf]
[35] The CALCULEMUS research training network: A short overview (Christoph Benzmüller), In Proceedings of the 11th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (CALCULEMUS 2003), MMIII ARACNE EDITRICE S.R.L. (ISBN 88-7999-545-6), pp. 1-16, 2003. (slides) [bibtex] [pdf]
[34] Tutorial Dialogs on Mathematical Proofs (Christoph Benzmüller, Armin Fiedler, Malte Gabsdil, Helmut Horacek, Ivana Kruijff-Korbayova, Manfred Pinkal, Jörg Siekmann, Dimitra Tsovaltzi, Bao Quoc Vo, Magdalena Wolska), In Proceedings of IJCAI-03 Workshop on Knowledge Representation and Automated Reasoning for E-Learning Systems, pp. 12-22, 2003. (slides) [bibtex] [pdf]
[33] Assertion Application in Theorem Proving and Proof Planning (Bao Quoc Vo, Christoph Benzmüller, Serge Autexier), In Proceedings of the 10th Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice, 2003. [bibtex] [pdf]
[32] Assertion Application in Theorem Proving and Proof Planning (Quoc Bao Vo, Christoph Benzmüller, Serge Autexier), In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI) (G. Gottlob, T. Walsh, eds.), 2003. (poster) (ISBN 0-127-05661-0) [bibtex] [pdf]
2002
[31] Automatic Learning of Proof Methods in Proof Planning (Mateja Jamnik, Manfred Kerber, Martin Pollet, Christoph Benzmüller), In Proceedings of the 9th Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice, pp. 1-2, 2002. [bibtex] [pdf]
[30] Reasoning Services in the MathWeb-SB for Symbolic Verification of Hybrid Systems (Christoph Benzmüller, Corrado Giromini, Andreas Nonnengart, Jürgen Zimmer), In Proceedings of the Verification Workshop - VERIFY'02 in connection with FLOC 2002, pp. 29-39, 2002. [bibtex] [pdf]
[29] Symbolic Verification of Hybrid Systems supported by Mathematical Services (Christoph Benzmüller, Corrado Giromini, Andreas Nonnengart), In Additonal Proceedings of 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (CALCULEMUS 2002), pp. 1-10, 2002. [bibtex] [pdf]
[28] Agent-based Proof Search with Indexed Formulas (Malte Hübner, Serge Autexier, Christoph Benzmüller), In Additonal Proceedings of 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (CALCULEMUS 2002), pp. 11-20, 2002. (slides) [bibtex] [pdf]
[27] Agent-based Theorem Proving (Christoph Benzmüller, Volker Sorge), In Proceedings of the 9th Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice, pp. 1-3, 2002. [bibtex] [pdf]
[26] Proof Development with OMEGA: Sqrt(2) is irrational (Jörg Siekmann, Christoph Benzmüller, Armin Fiedler, Andreas Meier, Martin Pollet), In Logic for Programming, Artificial Intelligence, and Reasoning, 9th International Conference, LPAR 2002 (Matthias Baaz, Andrei Voronkov, eds.), Springer, LNCS, number 2514, pp. 367-387, 2002. (slides) [bibtex] [pdf]
[25] Proof Development with OMEGA (Jörg Siekmann, Christoph Benzmüller, Vladimir Brezhnev, Lassaad Cheikhrouhou, Armin Fiedler, Andreas Franke, Helmut Horacek, Michael Kohlhase, Andreas Meier, Erica Melis, Markus Moschner, Immanuel Normann, Martin Pollet, Volker Sorge, Carsten Ullrich, Claus-Peter Wirth, Jürgen Zimmer), In Proceedings of the 18th International Conference on Automated Deduction (CADE-18) (Andrei Voronkov, ed.), Springer, LNCS, number 2392, pp. 144-149, 2002. (slides) [bibtex] [pdf] [doi]
2001
[24] Proof transformation and expansion with a parameterisable inference machine. (Christoph Benzmüller, Andreas Meier, Martin Pollet, Volker Sorge), In Proceedings of the Eighth Workshop on Automated Reasoning, Bridging the Gap between Theory and Practice, University of York, pp. 1-2, 2001. ((Mildly reviewed)) [bibtex] [pdf]
[23] Learning proof methods in proof planning (Mateja Jamnik, Manfred Kerber, Christoph Benzmüller), In Proceedings of the Eighth Workshop on Automated Reasoning, Bridging the Gap between Theory and Practice, University of York, pp. 5-6, 2001. ((Mildly reviewed)) [bibtex] [pdf]
[22] Towards Learning New Methods in Proof Planning (Mateja Jamnik, Manfred Kerber, Christoph Benzmüller), In Proceedings of the CADE-17 Workshop: Automated Deduction in the Context of Mathematics, pp. 1-12, 2001. [bibtex] [pdf]
[21] Distributed Assertion Retrieval (Christoph Benzmüller, Andreas Meier, Volker Sorge), In First International Workshop on Mathematical Knowledge Management, pp. 1-7, 2001. (slides) [bibtex] [pdf]
[20] A Lost Proof (Christoph Benzmüller, Manfred Kerber), In Proceedings of the IJCAR 2001 Workshop: Future Directions in Automated Reasoning, pp. 13-24, 2001. [bibtex] [pdf]
[19] Proof Planning: A Fresh Start? (Christoph Benzmüller, Andreas Meier, Erica Melis, Martin Pollet, Volker Sorge), In Proceedings of the IJCAR 2001 Workshop: Future Directions in Automated Reasoning, pp. 25-37, 2001. [bibtex] [pdf]
[18] An Agent-oriented Approach to Reasoning (Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge), In Proceedings of the Calculemus Workshop 2001, pp. 48-63, 2001. [bibtex] [pdf]
[17] An Agent Based Approach to Reasoning (Christoph Benzmüller), In Extended abstract for invited plenary talk at AISB'01 Convention `Agents and Cognition, University of York, pp. 57-58, 2001. (slides) [bibtex] [pdf]
[16] 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]
[15] 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
[14] Resource Guided Concurrent Deduction (Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge), In Proceedings of the AISB'2000 Symposium `How to design a functioning mind', pp. 137-138, 2000. ((Mildly reviewed)) [bibtex] [pdf]
[13] Adaptive Course Generation and Presentation (Jörg Siekmann, Christoph Benzmüller, Armin Fiedler, Andreas Franke, George Goguadze, Helmut Horacek, Michael Kohlhase, Paul Libbrecht, Andreas Meier, Erica Melis, Martin Pollet, Volker Sorge, Carsten Ullrich, Jürgen Zimmer), In Proceedings of the Fifth International Conference on Intelligent Tutoring Systems---Workshop W2: Adaptive and Intelligent Web-Based Education Systems (P. Brusilovski, ed.), pp. 54-61, 2000. [bibtex] [pdf]
[12] Towards Learning New Methods in Proof Planning (Mateja Jamnik, Manfred Kerber, Christoph Benzmüller), In Symbolic Computation and Automated Reasoning (Manfred Kerber, Michael Kohlhase, eds.), A.K.Peters, pp. 142-159, 2000. [bibtex] [pdf]
[11] 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
[10] Agent Based Mathematical Reasoning (Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge), In Proceedings of the Calculemus Workshop: Systems for Integrated Computation and Deduction, pp. 1-12, 1999. (slides) [bibtex] [pdf]
[9] Towards Fine-Grained Proof Planning with Critical Agents (Christoph Benzmüller, Volker Sorge), In Proceedings of the 6th Workshop on Automated Reasoning, Edinburgh College of Art & Divison of Informatics, University of Edinburgh, pp. 19-20, 1999. ((Mildly reviewed)) [bibtex] [pdf]
[8] 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]
[7] Extensional Higher-Order Paramodulation and RUE-Resolution (Christoph Benzmüller), In Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings (Harald Ganzinger, ed.), Springer, LNCS, number 1632, pp. 399-413, 1999. (slides) [bibtex] [pdf] [doi]
1998
[6] Integrating TPS with OMEGA (Christoph Benzmüller, Volker Sorge), In Theorem Proving in Higher Order Logics: Emerging Trends (Jim Grundy, Malcolm Newey, eds.), Technical Report 98-08, Department of Computer Science and Computer Science Lab, The Australian National University, pp. 1-18, 1998. [bibtex] [pdf]
[5] A Distributed Graphical User Interface for the Interactive Proof System (Jörg Siekmann, Stephan Hess, Christoph Benzmüller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Helmut Horacek, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis, Volker Sorge), In Proceedings of the International Workshop "User Interfaces for Theorem Provers 1998 (UITP'98), pp. 130-138, 1998. [bibtex] [pdf]
[4] A Blackboard Architecture for Guiding Interactive Proofs (Christoph Benzmüller, Volker Sorge), In Artificial Intelligence: Methodology, Systems, and Applications, 8th International Conference, AIMSA '98, Sozopol, Bulgaria, September 21-13, 1998, Proceedings (Fausto Giunchiglia, ed.), Springer, LNCS, number 1480, pp. 102-114, 1998. [bibtex] [pdf] [doi]
[3] 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]
[2] 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]
1997
[1] OMEGA: Towards a mathematical assistant (Christoph Benzmüller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Karsten Konrad, Erica Melis, Andreas Meier, Wolf Schaarschmidt, Jörg Siekmann, Volker Sorge), In Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings (William McCune, ed.), Springer, LNCS, number 1249, pp. 252-255, 1997. [bibtex] [pdf] [doi]
Powered by bibtexbrowser