Year: .*
2017
[255]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]
[254] 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]
[253] 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]
[252] Mechanizing Principia Logico-Metaphysica in Functional Type Theory (Daniel Kirchner, Christoph Benzmüller, Edward N. Zalta), In arXiv, http://arxiv.org/abs/1703.09620, 2017. [bibtex] [pdf]
[251] Universal Reasoning, Rational Argumentation and Human-Machine Interaction (Christoph Benzmüller), In arXiv, http://arxiv.org/abs/1703.09620, 2017. [bibtex] [pdf]
[250] Experiments in Computational Metaphysics: Gödel's Proof of God's Existence (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In Savijnanam: scientific exploration for a spiritual paradigm. Journal of the Bhaktivedanta Institute, volume 9, pp. 43-57, 2017. [bibtex] [pdf]
[249] Types, Tableaus and Gödel's God in Isabelle/HOL (David Fuenmayor, Christoph Benzmüller), In Archive of Formal Proofs, 2017. (This publication is formally verified with Isabelle/HOL) [bibtex] [pdf]
[248] Computer-Assisted Analysis of the Anderson-Hájek Controversy (Christoph Benzmüller, Leon Weber, Bruno Woltzenlogel Paleo), In Logica Universalis, volume 11, number 1, pp. 139-151, 2017. [bibtex] [pdf] [doi]
[247] Cut-Elimination for Quantified Conditional Logic (Christoph Benzmüller), In Journal of Philosophical Logic, volume 46, number 3, pp. 333-353, 2017. (Springer Nature Link) [bibtex] [pdf] [doi]
[246]GCAI 2017. 3rd Global Conference on Artificial Intelligence, (Christoph Benzmüller, Christine Lisetti, Martin Theobald, eds.), EasyChair, EPiC Series in Computing, volume 41, 2017. (event-website) (To appear in Oct 2017) [bibtex]
[245] 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, 2017. [bibtex] [pdf]
[244] 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]
[243] 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]
[242] 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
[241] 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]
[240] Axiomatizing Category Theory in Free Logic (Christoph Benzmüller, Dana S. Scott), In arXiv, http://arxiv.org/abs/1609.01493, 2016. [bibtex] [pdf]
[239] Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic (Alexander Steen, Christoph Benzmüller), In Logic and Logical Philosophy, volume 25, pp. 535-554, 2016. [bibtex] [pdf] [doi]
[238] GCAI 2016. 2nd Global Conference on Artificial Intelligence, (Christoph Benzmüller, Geoff Sutcliffe, Raul Rojas, eds.), EasyChair, EPiC Series in Computing, volume 41, 2016. (event-website) [bibtex] [pdf]
[237] ARQNL 2016. Automated Reasoning in Quantified Non-Classical Logics, (Christoph Benzüller, Jens Otten, eds.), CEUR Workshop Proceedings, http://ceur-ws.org, volume 1770, pp. 1-86, 2016. (event-website) [bibtex] [pdf]
[236] 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]
[235] 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]
[234] 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]
[233] 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]
[232] 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]
[231] 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]
[230] 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]
[229] 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]
[228] 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]
[227] Analysis of an Ontological Proof Proposed by Leibniz (Matthias Bentert, Christoph Benzmüller, David Streit, Bruno Woltzenlogel Paleo), Chapter in Death and Anti-Death, Volume 14: Four Decades after Michael Polanyi, Three Centuries after G.W. Leibniz (Charles Tandy, ed.), Ria University Press, 2016. (Preprint: http://christoph-benzmueller.de/papers/B16.pdf) [bibtex] [pdf]
[226] The Modal Collapse as a Collapse of the Modal Square of Opposition (Christoph Benzmüller, Bruno Woltzenlogel Paleo), Chapter in The Square of Opposition: A Cornerstone of Thought (Collection of papers related to the World Congress on the Square of Opposition IV, Vatican, 2014), http://www.springer.com/us/book/9783319450612 (Jean-Yves Béziau, Gianfranco Basti, eds.), Springer International Publishing Switzerland, Studies in Universal Logic, 2016. [bibtex] [pdf] [doi]
2015
[225] 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]
[224] 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]
[223] Computational Metaphysics --- Bewerbung zum zentralen Lehrpreis der Freien Universität Berlin (Christoph Benzmüller, Max Wisniewski, Alexander Steen), 2015. (This lecture course proposal received the 2015 central teaching award of FU Berlin) [bibtex] [pdf]
[222]News --- 25th International Conference on Automated Deduction (CADE-25) (Christoph Benzmüller, Alexander Steen, Max Wisniewski), In Künstliche Intelligenz, volume 29, issue 4, pp. 451-452, 2015. (Non-reviewed conference report) [bibtex] [doi]
[221] 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]
[220] ARQNL 2014. Automated Reasoning in Quantified Non-Classical Logics, (Christoph Benzüller, Jens Otten, eds.), EasyChair, EPiC Series in Computing, volume 33, pp. 1-86, 2015. (event-website) [bibtex] [pdf]
[219] 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]
[218] 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]
[217] 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]
[216] 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]
[215] 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]
[214] 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]
[213] 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]
[212] 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]
[211] 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]
[210] 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]
[209] 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]
[208] Higher-Order Automated Theorem Provers (Christoph Benzmüller), Chapter in All about Proofs, Proof for All (David Delahaye, Bruno Woltzenlogel Paleo, eds.), College Publications, Mathematical Logic and Foundations, pp. 171-214, 2015. (publisher) [bibtex] [pdf]
2014
[207] 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]
[206] Proceedings of the 11th International Workshop on User Interfaces for Theorem Provers (UITP 2014), Vienna, Austria, (Christoph Benzüller, Bruno Woltzenlogel Paleo, eds.), Electronic Proceedings in Theoretical Computer Science (EPTCS), volume 167, pp. 1-94, 2014. [bibtex] [pdf] [doi]
[205]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]
[204] 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]
[203] 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]
[202] Automation of Higher-Order Logic (Christoph Benzmüller, Dale Miller), Chapter in Handbook of the History of Logic, Volume 9 --- Computational Logic (Dov M. Gabbay, Jörg H. Siekmann, John Woods, eds.), North Holland, Elsevier, pp. 215-254, 2014. [bibtex] [pdf] [doi]
2013
[201] 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]
[200] 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]
[199] 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]
[198] 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]
[197] 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]
[196] 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]
[195] 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]
[194] Update report: LEO-II version 1.5 (Christoph Benzmüller, Nik Sultana), In CoRR, volume abs/1303.3761, 2013. [bibtex] [pdf]
[193]CADE 2015 in Berlin: A Proposal (Christoph Benzmüller), 2013. [bibtex]
[192]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]
[191] 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]
[190] Sigma: An Integrated Development Environment for Formal Ontology (Adam Pease, Christoph Benzmüller), In AI Communications (Special Issue on Intelligent Engineering Techniques for Knowledge Bases), volume 26, number 1, pp. 79-97, 2013. [bibtex] [pdf] [doi]
[189] Quantified Multimodal Logics in Simple Type Theory (Christoph Benzmüller, Lawrence Paulson), In Logica Universalis (Special Issue on Multimodal Logics), volume 7, number 1, pp. 7-20, 2013. [bibtex] [pdf] [doi]
[188] 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]
[187] 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]
[186] 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]
[185] 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
[184] 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]
[183] 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]
[182] 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]
[181] Higher-order Aspects and Context in SUMO (Christoph Benzmüller, Adam Pease), In Journal of Web Semantics (Special Issue on Reasoning with context in the Semantic Web), volume 12-13, pp. 104-117, 2012. [bibtex] [pdf] [doi]
[180] Embedding and Automating Conditional Logics in Classical Higher-Order Logic (Christoph Benzmüller, Dov Gabbay, Valerio Genovese, Daniele Rispoli), In Annals of Mathematics and Artificial Intelligence, volume 66, number 1-4, pp. 257-271, 2012. [bibtex] [pdf] [doi]
[179] 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
[178] Embedding and Automating Conditional Logics in Classical Higher-Order Logic (Christoph Benzmüller, Dov Gabbay, Valerio Genovese, Daniele Rispoli), Technical report, Freie Universität Berlin, Germany, 2011. (arXiv:1106.3685) [bibtex] [pdf]
[177] Combining and Automating Classical and Non-Classical Logics in Classical Higher-Order Logic (Christoph Benzmüller), In Annals of Mathematics and Artificial Intelligence (Special issue Computational logics in Multi-agent Systems (CLIMA XI)), volume 62, number 1-2, pp. 103-128, 2011. (slides) [bibtex] [pdf] [doi]
[176] 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]
[175] Knowledge Engineering Tools (Christoph Benzmüller, Adam Pease), Chapter in Ontology: A Practical Guide (Adam Pease, ed.), Articulate Software Press, pp. 171-214, 2011. ((This chapter has some essential overlap with the 2012 journal article with A. Pease titled Higher-Order Aspects and Context in SUMO; non-reviewed here)) [bibtex] [pdf]
2010
[174] 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]
[173] 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]
[172] 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]
[171] 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]
[170] 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]
[169] Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure (Geoff Sutcliffe, Christoph Benzmüller), In Journal of Formalized Reasoning, volume 3, number 1, pp. 1-27, 2010. [bibtex] [pdf]
[168] 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]
[167] 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]
[166] 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]
[165] Resource-Bounded Modelling and Analysis of Human-Level Interactive Proofs (Christoph Benzmüller, Marvin Schiller, Jörg Siekmann), Chapter in Resource-Adaptive Cognitive Processes (Matthew W. Crocker, Jörg Siekmann, eds.), Springer, Cognitive Technologies, pp. 291-311, 2010. ((Final project report, DFG SFB 378)) [bibtex] [pdf] [doi]
[164] OMEGA: Resource-Adaptive Processes in an Automated Reasoning Systems (Serge Autexier, Christoph Benzmüller, Dominik Dietrich, Jörg Siekmann), Chapter in Resource-Adaptive Cognitive Processes (Matthew W. Crocker, Jörg Siekmann, eds.), Springer, Cognitive Technologies, pp. 389-423, 2010. ((Final project report, DFG SFB 378)) [bibtex] [pdf] [doi]
2009
[163] 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]
[162] Effective Higher-Order Automated Theorem Proving with integrated Descente Infinie and Presburger Arithmetic LEO-III (Christoph Benzmüller, Claus-Peter Wirth), 2009. [bibtex] [pdf]
[161] 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 (Christoph Benzmüller, Geoff Sutcliffe), Saarland University, 2009. [bibtex] [pdf]
[160] 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 (Christoph Benzmüller, Geoff Sutcliffe), Technical report, Saarland University, 2009. [bibtex] [pdf]
[159] LEO-II im Ontologieschliessen -- Antrag auf ein Forschungsvorhaben an die DFG (Christoph Benzmüller), 2009. [bibtex] [pdf]
[158] Automating Quantified Multimodal Logics in Simple Type Theory -- A Case Study (Christoph Benzmüller), SEKI Publications (ISSN 1437-4447), SEKI Working-Paper SWP-2009-02, 2009. (arXiv:0905.4369) [bibtex] [pdf]
[157] Quantified Multimodal Logics in Simple Type Theory (Christoph Benzmüller, Lawrence Paulson), SEKI Publications (ISSN 1437-4447), SEKI Report SR-2009-02 (ISSN 1437-4447), 2009. (arXiv:0905.2435) [bibtex] [pdf]
[156] Granularity-Adaptive Proof Presentation (Marvin Schiller, Christoph Benzmüller), SEKI Publications (ISSN 1437-4447), SEKI Working-Paper SWP--2009--01, 2009. (arXiv:0903.0314) [bibtex] [pdf]
[155] Lectures on Jacques Herbrand as a Logician (Claus-Peter Wirth, Jörg Siekmann, Christoph Benzmüller, Serge Autexier), SEKI Publications (ISSN 1437-4447), 2009. (arXiv:0902.4682) [bibtex] [pdf]
[154] Preface: Proceedings of the 8th Workshop on User Interfaces for Theorem Provers (UITP 2008) (Serge Autexier, Christoph Benzmüller), In Electronic Notes in Theoretical Computer Science, volume 226, number 1, pp. 1-2, 2009. [bibtex] [pdf] [doi]
[153] Cut-Simulation and Impredicativity (Christoph Benzmüller, Chad Brown, Michael Kohlhase), In Logical Methods in Computer Science, volume 5, number 1:6, pp. 1-21, 2009. [bibtex] [pdf] [doi]
[152] Proceedings of the 8th International Workshop on User Interfaces for Theorem Provers (UITP 2008), Montréal, Canada, (Serge Autexier, Christoph Benzüller, eds.), Elsevier, Electronic Notes in Theoretical Computer Science, volume 226, pp. 1-106, 2009. [bibtex] [pdf]
[151] 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]
[150] 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]
[149] 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]
[148] 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]
[147] 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]
[146] Jacques Herbrand: Life, Logic, and Automated Deduction (Claus-Peter Wirth, Jörg Siekmann, Christoph Benzmüller, Serge Autexier), Chapter in Handbook of the History of Logic, Volume 5 -- Logic from Russell to Church (Dov Gabbay, John Woods, eds.), Elsevier, 2009. [bibtex] [pdf] [doi]
2008
[145] 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]
[144] 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]
[143] DIALOG: Natural Language-based Interaction with a Mathematics Assistance System (Manfred Pinkal, Jörg Siekmann, Christoph Benzmüller, Ivana Kruijff-Korbayova), pp. 1-20, 2008. (Project report in the Collaborative Research Centre SFB 378 on Resource-adaptive Cognitive Processes) [bibtex] [pdf]
[142] OMEGA: Agent-oriented Proof Planning (Jörg Siekmann, Serge Autexier, Christoph Benzmüller), pp. 1-19, 2008. (Project report in the Collaborative Research Centre SFB 378 on Resource-adaptive Cognitive Processes) [bibtex] [pdf]
[141] Proof Step Analysis for Proof Tutoring -- A Learning Approach to Granularity (Marvin Schiller, Dominik Dietrich, Christoph Benzmüller), In Teaching Mathematics and Computer Science, volume 6, number 2, pp. 325-343, 2008. [bibtex] [pdf]
[140] Organisation, Transformation, and Propagation of Mathematical Knowledge in Omega (Serge Autexier, Christoph Benzmüller, Dominik Dietrich, Marc Wagner), In Mathematics in Computer Science, volume 2, number 2, pp. 253-277, 2008. [bibtex] [pdf] [doi]
[139] 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]
[138] 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. 460, 2008. [bibtex] [pdf]
[137] 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]
[136] 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]
[135] 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]
[134] Cut Elimination with Xi-Functionality (Christoph Benzmüller, Chad Brown, Michael Kohlhase), 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. 84-100, 2008. [bibtex] [pdf]
2007
[133] 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]
[132] 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]
[131] 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]
[130] Preface: Proceedings of the 7th Workshop on User Interfaces for Theorem Provers (UITP 2006) (Serge Autexier, Christoph Benzmüller), In Electronic Notes in Theoretical Computer Science, volume 174, number 2, pp. 1-2, 2007. [bibtex] [pdf] [doi]
[129] PLATO: A Mediator between Text-Editors and Proof Assistance Systems (Marc Wagner, Serge Autexier, Christoph Benzmüller), In Electronic Notes in Theoretical Computer Science, volume 174, number 2, pp. 87-107, 2007. [bibtex] [pdf] [doi]
[128] User Interfaces for Theorem Provers, Proceedings of UITP'06, (Serge Autexier, Christoph Benzmüller, eds.), Elsevier, Electronic Notes in Theoretical Computer Science, volume 174, number 2, pp. 1-2, 2007. [bibtex] [pdf]
[127] 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]
[126] 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]
[125] 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]
[124] Natural Language Dialog with a Tutor System for Mathematical Proofs (Christoph Benzmüller, Helmut Horacek, Ivana Kruijff-Korbayova, Manfred Pinkal, Jörg Siekmann, Magdalena Wolska), Chapter in Cognitive Systems (Ruqian Lu, Jörg Siekmann, Carsten Ullrich, eds.), Springer, LNCS, volume 4429, pp. 1-14, 2007. [bibtex] [pdf] [doi]
[123] The curious inference of Boolos in MIZAR and OMEGA (Christoph Benzmüller, Chad Brown), Chapter in From Insight to Proof -- Festschrift in Honour of Andrzej Trybulec (Roman Matuszewski, Anna Zalewska, eds.), The University of Bialystok, Polen, Studies in Logic, Grammar, and Rhetoric, volume 10(23), pp. 299-388, 2007. [bibtex] [pdf]
2006
[122] 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]
[121] 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]
[120] 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]
[119] Cumulative Habilitation Script (Christoph Benzmüller), Saarland University, Germany, pp. 1-357, 2006. [bibtex] [pdf]
[118] Cut-Simulation in Impredicative Logics (extended version) (Christoph Benzmüller, Chad Brown, Michael Kohlhase), SEKI Publications (ISSN 1437-4447), number SR-2006-01, 2006. [bibtex] [pdf]
[117] Semantics of Higher-Order Logic (Christoph Benzmüller, Chad Brown), pp. 1-50, 2006. (Course Notes from the 18th European Summer School in Logic, Language and Information (ESSLLI'06)) [bibtex] [pdf]
[116] Editorial: Towards Computer Aided Mathematics (Christoph Benzmüller), In Journal of Applied Logic, volume 4, number 4, pp. 359-365, 2006. [bibtex] [pdf] [doi]
[115] Computer Supported Mathematics with OMEGA (Jörg Siekmann, Christoph Benzmüller, Serge Autexier), In Journal of Applied Logic, volume 4, number 4, pp. 533-559, 2006. [bibtex] [pdf] [doi]
[114] Special Issue on Assistance Systems for Mathematics, (Christoph Benzmüller, ed.), Journal of Applied Logic, Elsevier, 2006. [bibtex] [pdf]
[113] Proceedings of the 6th International Workshop on the Implementation of Logics, (Christoph Benzmüller, Bernd Fischer, Geoff Sutcliffe, eds.), CEUR-WS.org, CEUR Workshop Proceedings, volume 212, 2006. [bibtex] [pdf]
[112] 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]
[111] 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]
[110] 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]
[109] OMEGA (Christoph Benzmüller, Armin Fiedler, Andreas Meier, Martin Pollet, Jörg Siekmann), Chapter in The Seventeen Provers of the World (Freek Wiedijk, ed.), Springer, LNCS, number 3600, pp. 127-141, 2006. [bibtex] [pdf] [doi]
2005
[108] 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]
[107] 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]
[106] 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]
[105] 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]
[104] System Description: A Dialog Manager supporting Tutorial Natural Language Dialogue on Proofs (Mark Buckley, Christoph Benzmüller), 2005. (This article was formally accepted for the UITP'05 post-proceedings in ENTCS; this volume did not appear though.) [bibtex] [pdf]
[103] Integrating Proof Assistants as Reasoning and Verification Tools into a Scientific WYSIWYG Editor (Serge Autexier, Christoph Benzmüller, Armin Fiedler, Henri Lesourd), 2005. (This article was formally accepted for the UITP'05 post-proceedings in ENTCS; this volume did not appear though.) [bibtex] [pdf]
[102] Proceedings of the LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL), (Christoph Benzmüller, John Harrison, Carsten Schürmann, eds.), 2005. (arXiv:cs/0601042) [bibtex] [pdf]
[101] 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]
[100] 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]
[99] 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
[98] Interactive Theorem Proving with Tasks (Malte Hübner, Serge Autexier, Christoph Benzmüller, Andreas Meier), In Electronic Notes in Theoretical Computer Science, volume 103, number C, pp. 161-181, 2004. [bibtex] [pdf] [doi]
[97] Computer-Supported Mathematical Theory Development, (Christoph Benzmüller, Wolfgang Windsteiger, eds.), RISC Report Series, number 04-14, 2004. (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.) [bibtex] [pdf]
[96] The CALCULEMUS Final Report (Christoph Benzmüller, Corinna Hahn), Saarland University, Germany, pp. 1-57, 2004. (Final report of the Marie Curie Research Training Network CALCULEMUS within the EU 5th framework) [bibtex] [pdf]
[95] A Dialogue Manager for the DIALOG Demonstrator (Mark Buckley, Christoph Benzmüller), SEKI Publications (ISSN 1437-4447), number SR-04-01, 2004. [bibtex] [pdf]
[94] Abschlussbericht Projekt HOTEL (Christoph Benzmüller, Michael Kohlhase, Jörg Siekmann), pp. 1-14, 2004. (DFG research grant report) [bibtex] [pdf]
[93] VERMATH: Distributed Mathematical Problem Solving (Serge Autexier, Christoph Benzmüller, Michael Kohlhase, Jörg Siekmann), pp. 1-22, 2004. (DFG research grant proposal) [bibtex] [pdf]
[92] ALONZO: Higher-Order Reasoning Agents and Semantical Mediation of Mathematical Knowledge (Christoph Benzmüller), pp. 1-29, 2004. (DFG research grant proposal) [bibtex] [pdf]
[91] OMEGA: Agent-oriented Proof Planning (Jörg Siekmann, Christoph Benzmüller, Serge Autexier), pp. 1-26, 2004. (Project proposal in the Collaborative Research Centre SFB 378 on Resource-adaptive Cognitive Processes) [bibtex] [pdf]
[90] DIALOG: Natural Language-based Interaction with a Mathematics Assistance System (Manfred Pinkal, Jörg Siekmann, Christoph Benzmüller, Ivana Kruijff-Korbayova), pp. 1-31, 2004. (Project proposal in the Collaborative Research Centre SFB 378 on Resource-adaptive Cognitive Processes) [bibtex] [pdf]
[89] OMEGA: Resource-adaptive Proof Planning (Jörg Siekmann, Christoph Benzmüller, Erica Melis), pp. 1-22, 2004. (Project report in the Collaborative Research Centre SFB 378 on Resource-adaptive Cognitive Processes) [bibtex] [pdf]
[88] DIALOG: Tutorial Dialog with an Assistance System for Mathematics (Manfred Pinkal, Jörg Siekmann, Christoph Benzmüller), pp. 1-24, 2004. (Project report in the Collaborative Research Centre SFB 378 on Resource-adaptive Cognitive Processes) [bibtex] [pdf]
[87] ALONZO: Higher-Order Reasoning Agents for Mathematics (Christoph Benzmüller), pp. 1-37, 2004. (EURYI project proposal) [bibtex] [pdf]
[86] Assertion-level Proof Representation with Under-Specification (Serge Autexier, Christoph Benzmüller, Armin Fiedler, Helmut Horacek, Bao Quoc Vo), In Electronic Notes in Theoretical Computer Science, volume 93, pp. 5-23, 2004. [bibtex] [pdf] [doi]
[85] Higher-Order Semantics and Extensionality (Christoph Benzmüller, Chad Brown, Michael Kohlhase), In Journal of Symbolic Logic, volume 69, number 4, pp. 1027-1088, 2004. [bibtex] [pdf] [doi]
[84] 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]
[83] 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]
[82] Bridging Theorem Proving and Mathematical Knowledge Retrieval (Christoph Benzmüller, Andreas Meier, Volker Sorge), Chapter in Mechanizing Mathematical Reasoning: Essays in Honor of Jörg Siekmann on the Occasion of His 60th Birthday (Dieter Hutter, Werner Stephan, eds.), Springer, LNCS, volume 2605, pp. 277-296, 2004. [bibtex] [pdf] [doi]
2003
[81] The CALCULEMUS Midterm Report, (Christoph Benzmüller, Corinna Hahn, eds.), Saarland University, Germany, 2003. (EU Report, Saarland University, Saarbrücken, Germany) [bibtex] [pdf]
[80] OMEGA --- From Proof Planning towards Mathematical Knowledge Management (Serge Autexier, Christoph Benzmüller), In Mathematical Knowledge Management Symposium, 2003. (slides) [bibtex] [pdf]
[79] 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]
[78] 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]
[77] 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]
[76] 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]
[75] 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]
[74] 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]
[73] 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]
[72] 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]
[71] CALCULEMUS-II: Computer-supported Mathematical Knowledge Evolution (Christoph Benzmüller, Dieter Hutter), Saarland University, Germany, pp. 1-73, 2003. (Project proposal for a Marie Curie Research Training Network within the EU 6th framework; 73 pages) [bibtex] [pdf]
[70] ALONZO: Deduktionsagenten höherer Ordnung für Mathematische Assistenzsysteme (Christoph Benzmüller), pp. 1-43, 2003. (Project proposal in the DFG Aktionsplan Informatik) [bibtex] [pdf]
[69] Towards a Framework to Integrate Proof Search Paradigms (Serge Autexier, Christoph Benzmüller, Dieter Hutter), SEKI Publications (ISSN 1437-4447), number SR-03-02, 2003. [bibtex] [pdf]
[68] An Approach to Assertion Application via Generalized Resolution (Bao Quoc Vo, Christoph Benzmüller, Serge Autexier), SEKI Publications (ISSN 1437-4447), number SR-03-01, 2003. [bibtex] [pdf]
[67] 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]
[66] 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]
[65] Automatic Learning of Proof Methods in Proof Planning (Mateja Jamnik, Manfred Kerber, Martin Pollet, Christoph Benzmüller), In The Logic Journal of the IGPL, volume 11, number 6, pp. 647-674, 2003. [bibtex] [pdf] [doi]
[64] Systems for Integrated Computation and Deduction -- Interim Report of the CALCULEMUS IHP Network, (Christoph Benzmüller, ed.), SEKI Publications (ISSN 1437-4447), 2003. (135 pages) [bibtex] [pdf]
[63] 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]
[62] Proof Development in OMEGA: The Irrationality of Square Root of 2 (Jörg Siekmann, Christoph Benzmüller, Armin Fiedler, Andreas Meier, Immanuel Normann, Martin Pollet), Chapter in Thirty Five Years of Automating Mathematics (Fairouz Kamareddine, ed.), Kluwer Academic Publishers, Applied Logic series (28), pp. 271-314, 2003. [bibtex] [pdf] [doi]
2002
[61] 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]
[60] 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]
[59] 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]
[58] 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]
[57] 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]
[56] A remark on higher order RUE-resolution with EXTRUE (Christoph Benzmüller), Technical report, Saarland University, SEKI Publications (ISSN 1437-4447), number SR-02-05, pp. 1-5, 2002. (arXiv:0901.3608) [bibtex] [pdf]
[55] Automatic Learning of Proof Methods in Proof Planning (Mateja Jamnik, Manfred Kerber, Martin Pollet, Christoph Benzmüller), Technical report, University of Birmingham, School of Computer Science, number CSRP-02-05, pp. 1-34, 2002. [bibtex] [pdf]
[54] Irrationality of square root of 2 -- A case study in OMEGA (Christoph Benzmüller, Armin Fiedler, Andreas Meier, Martin Pollet), Technical report, Saarland University, SEKI Publications (ISSN 1437-4447), number SR-02-03, pp. 1-103, 2002. [bibtex] [pdf]
[53] 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]
[52] CALCULEMUS Autumn School 2002: Course Notes (Part III), (Christoph Benzmüller, Regine Endsuleit, eds.), SEKI Publications (ISSN 1437-4447), number SR-02-09, 2002. (121 pages) [bibtex] [pdf]
[51] CALCULEMUS Autumn School 2002: Course Notes (Part II), (Christoph Benzmüller, Regine Endsuleit, eds.), SEKI Publications (ISSN 1437-4447), number SR-02-08, pp. 1-130, 2002. ((130 pages)) [bibtex] [pdf]
[50] CALCULEMUS Autumn School 2002: Course Notes (Part I), (Christoph Benzmüller, Regine Endsuleit, eds.), SEKI Publications (ISSN 1437-4447), number SR-02-07, pp. 1-168, 2002. ((168 pages)) [bibtex] [pdf]
[49] CALCULEMUS Autumn School 2002: Student Poster Abstracts, (Jürgen Zimmer, Christoph Benzmüller, eds.), SEKI Publications (ISSN 1437-4447), number SR-02-06, pp. 1-116, 2002. ((115 pages)) [bibtex] [pdf]
[48] 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]
[47] 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
[46] 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]
[45] 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]
[44] 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]
[43] 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]
[42] 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]
[41] 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]
[40] 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]
[39] 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]
[38] OMEGA: Ressourcenadaptive Beweisplanung (Jörg Siekmann, Christoph Benzmüller, Erica Melis), pp. 1-30, 2001. (Project proposal in the Collaborative Research Centre SFB 378 on Resource-adaptive Cognitive Processes) [bibtex] [pdf]
[37] DIALOG: Tutorieller Dialog mit einem Mathematik Assistenzsystem (Manfred Pinkal, Jörg Siekmann, Christoph Benzmüller), pp. 1-34, 2001. (Project proposal in the Collaborative Research Centre SFB 378 on Resource-adaptive Cognitive Processes) [bibtex] [pdf]
[36] Learning Method Outlines in Proof Planning (Mateja Jamnik, Manfred Kerber, Christoph Benzmüller), Technical report, University of Birmingham, School of Computer Science, number CSRP-01-08, pp. 1-15, 2001. [bibtex] [pdf]
[35] 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]
[34] 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
[33] 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]
[32] 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]
[31] Towards Learning new Methods in Proof Planning (Mateja Jamnik, Manfred Kerber, Christoph Benzmüller), Technical report, University of Birmingham, School of Computer Science, number CSRP-00-09, pp. 1-16, 2000. [bibtex] [pdf]
[30] 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]
[29] 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
[28] 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]
[27] 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]
[26] 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]
[25] Resource Adaptive Agents in Interactive Theorem Proving (Christoph Benzmüller, Volker Sorge), SEKI Publications (ISSN 1437-4447), number SR-99-02, pp. 1-13, 1999. [bibtex] [pdf]
[24] Forschungsinteressen am Graduiertenkolleg Kognitionswissenschaft (Christoph Benzmüller), pp. 1-17, 1999. (Draft, AG Siekmann, Saarland University) [bibtex] [pdf]
[23] OANTS for Interactive ATP (Christoph Benzmüller, Volker Sorge, John Byrnes), pp. 1-5, 1999. (Draft, AG Siekmann, Saarland University) [bibtex] [pdf]
[22] 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]
[21] Towards Concurrent Resource Guided Deduction (Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge), Technical report, Saarland University, SEKI Publications (ISSN 1437-4447), number SR-99-07, pp. 1-27, 1999. [bibtex] [pdf]
[20] Agent based Mathematical Reasoning (Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge), In Electronic Notes in Theoretical Computer Science, Elsevier, volume 23, number 3, pp. 21-33, 1999. [bibtex] [pdf] [doi]
[19] An Interactive Proof Development Environment + Anticipation = A Mathematical Assistant? (Jörg Siekmann, Helmut Horacek, Michael Kohlhase, Christoph Benzmüller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Stephan Hess, Karsten Konrad, Andreas Meier, Erica Melis, Volker Sorge), In International Journal of Computing Anticipatory Systems (CASYS), volume 3, pp. 101-110, 1999. [bibtex] [pdf]
[18] LOUI: Lovely OMEGA User Interface (Jörg Siekmann, Stephan Hess, Christoph Benzmüller, Lassaad Cheikhrouhou, Armin Fiedler, Helmut Horacek, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis, Martin Pollet, Volker Sorge), In Formal Aspects of Computing, volume 11, number 3, pp. 326-342, 1999. [bibtex] [pdf] [doi]
[17] Integrating TPS and OMEGA (Christoph Benzmüller, Matt Bishop, Volker Sorge), In Journal of Universal Computer Science, volume 5, number 3, pp. 188-207, 1999. [bibtex] [pdf] [doi]
[16] 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]
[15] 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
[14] 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]
[13] 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]
[12] An Adaptation of Paramodulation and RUE-Resolution to Higher-Order Logic (Christoph Benzmüller), SEKI Publications (ISSN 1437-4447), number SR-98-07, pp. 1-55, 1998. [bibtex] [pdf]
[11] 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]
[10] 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]
[9] 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
[8] Henkin Completeness of Higher-Order Resolution (Christoph Benzmüller, Michael Kohlhase), SEKI Publications (ISSN 1437-4447), number SR-97-10, pp. 1-12, 1997. [bibtex] [pdf]
[7] Model Existence for Higher-Order Logic (Christoph Benzmüller, Michael Kohlhase), SEKI Publications (ISSN 1437-4447), number SR-97-09, pp. 1-34, 1997. [bibtex] [pdf]
[6] A Calculus and a System Architecture for Extensional Higher-Order Resolution (Christoph Benzmüller), Technical report, Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh, USA, number 97-198, pp. 1-28, 1997. [bibtex] [pdf]
[5] 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]
1995
[4] Proposal for my PhD-Study (Christoph Benzmüller), pp. 1-26, 1995. (Draft, AG Siekmann, Saarland University) [bibtex] [pdf]
1994
[3] Eine Fallstudie zur Spezifikation von Systemanforderungen in der Spezifikationssprache OBSCURE (Christoph Benzmüller), Master's thesis, Department of Computer Science, Saarland University, Germany, pp. 1-194, 1994. [bibtex] [pdf]
1993
[2] HDMS--A und OBSCURE in KORSO--- Die Funktionale Essenz von HDMS--A aus Sicht der algorithmischen Spezifikationsmethode --- TEIL 3: Spezifikation der atomaren Funktionen (Christoph Benzmüller), Technical report, Saarland University, SEKI Publications (ISSN 1437-4447), number A/06/93, pp. 1-59, 1993. [bibtex] [pdf]
1992
[1] Das Fallbeispiel `UNIX' --- Dokumentation einer UNIX-Filesystem-Spezifikation mit OWEB (Serge Autexier, Christoph Benzmüller, Ramses A. Heckler), Technical report, Saarland University, SEKI Publications (ISSN 1437-4447), number WP 92/36, 1992. [bibtex] [pdf]
Powered by bibtexbrowser