Year: .*
2018
[245](Invited) tba (Christoph Benzmüller), HaPoC celebration event for Martin Davis’ 90st birthday, 2018.
2017
[244](Invited keynote) Recent Successes with a Meta-Logical Approach to Universal Logical Reasoning (Christoph Benzmüller), XX Brazilian Symposium on Formal Methods (SMBF), Recife, Brazil, 2017. (December)
[243](Invited keynote) tba (Christoph Benzmüller), 3. BMG Tag, Berliner Mathematische Gesellschaft e.V., Berlin, 2017. (November)
[242]Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic (Christoph Benzmüller), KI 2017 - 40th German Conference on Artificial Intelligence, 25-29 September 2017 in Dortmund, Germany, 2017.
[241](Invited) Automating Free Logic in HOL, with an Experimental Application in Category Theory (Christoph Benzmüller), Dagstuhl Seminar 17371: Deduction Beyond First-Order Logic, Dagstuhl, 2017.
[240](Invited tutorial) Universal Logical Reasoning via Semantical Embeddings in HOL (Christoph Benzmüller), 2nd CLE Colloquium for Philosophy and History of Formal Sciences (CLE4Science), University of Campinas, Brasil, 2017. (zip-file)
[239](Invited keynote) Computational Metaphysics: The Virtues of Formal Proofs Beyond Math (Christoph Benzmüller), 2nd CLE Colloquium for Philosophy and History of Formal Sciences (CLE4Science), University of Campinas, Brasil, 2017.
[238]Universal Logic Theorem Proving via Semantical Embeddings in HOL (Christoph Benzmüller), International Workshop on Logic-Based Formalisms for Legal Reasoning (LBFLR 2017), 2017. (May)
[237](Invited tutorial) Tutorial on Universal Logic Theorem Proving in HOL (Christoph Benzmüller), ILIAS group, University of Luxembourg, 2017. (May)
[236](Invited) Computational Metaphysics: The Virtues of Formal Computer Proofs Beyond Maths and Computer Science (Christoph Benzmüller), S-2: The Ubiquity of Computing: historical and philosophical issues---Commission for Computing HaPoC--- 25th International Congress of History of Science and Technology, Rio de Janeiro, Brasil, 2017. (July)
[235]Innovative Teaching of Computational Metaphysics (Christoph Benzmüller), Session on Innovative and Effective Teaching in History of Science and Technology --- 25th International Congress of History of Science and Technology, Rio de Janeiro, Brasil, 2017. (July)
[234](Invited public talk) Calculemus!: Analyse von Kurt Gödel's Gottesbeweis mit dem Computer (Christoph Benzmüller), Urania, Berlin, 2017. (June)
[233]Davis-Putnam-Logemann-Loveland Algrithums (Christoph Benzmüller), Alpen-Adria Universität Klagenfurt, 2017. (April)
[232](Invited) Calculemus! --- Progress in Universal Logic Reasoning and Computational Metaphysics (Christoph Benzmüller), Alpen-Adria Universität Klagenfurt, 2017. (April)
[231](Invited) Universal Logic Reasoning via Shallow Semantical Embeddings (Christoph Benzmüller), Workshop on Rational Enterprise Architecture Logic and Reasoning (REAL), University of Luxembourg, 2017. (April)
[230](Invited) Computational Metaphysics: The Virtues of Formal Proofs Beyond Math (Christoph Benzmüller), ILIAS Distinguished Lectures, University of Luxembourg, 2017. (March)
[229](Invited) Künstliche Intelligenz --- Bemerkungen zur Historie und zu aktuellen Entwicklungen (Christoph Benzmüller), Innovationsregion Lausitz GmbH, Cottbus, 2017. (February)
[228](Invited) System Demonstration: Interactive and Automated Reasoning in Isabelle/HOL (Christoph Benzmüller), Workshop "bettermarks und Mathematische Beweise", bettermarks GmbH, Berlin, 2017. (January)
2016
[227](Invited) Uniform Proofs via Shallow Semantic Embeddings? (Christoph Benzmüller), Dagstuhl Seminar 15381 --- Universality of Proofs, Dagstuhl, 2016. (slides)
[226]Tutorial on Reasoning in Expressive Non-Classical Logics with Isabelle/HOL (Christoph Benzmüller), Second Global Conference on Artificial Intelligence (GCAI), Berlin, 2016. (course material)
[225]An Object-Logic Explanation for the Inconsistency in Gödel's OntologicalTheory (Christoph Benzmüller), KI 2016 - 39th German Conference on Artificial Intelligence, 26-30 September 2016 in Klagenfurt, Austria, 2016. (slides)
[224]Axiomatising Category Theory in Isabelle/HOL (Christoph Benzmüller), Deduktionstreffen, 26 September 2016 in Klagenfurt, Austria, 2016. (slides)
[223]Einsatz von Theorembeweisern in der Lehre (Christoph Benzmüller), Hochschuldidaktik der Informatik: 7. Fachtagung des GI-Fachbereichs Informatik und Ausbildung/Didaktik der Informatik; 13.-14. September 2016 an der Universität Potsdam, 2016. (slides)
[222](Invited talk) Computational Metaphysics: The Virtues of Formal Proofs Beyond Maths (Christoph Benzmüller), Colloquium of the Berlin Mathematical School (BMS Fridays), Berlin, 2016. (slides (without movies))
[221]An Object-Logic Explanation for the Inconsistency in Gödel’s Ontological Theory (Christoph Benzmüller), 39th German Conference on Artificial Intelligence (KI), 2016. (September)
[220]Axiomatizing Category Theory in Free Logic (Christoph Benzmüller), Deduktionstreffen 2016, 2016. (September)
[219](Poster) The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics (Christoph Benzmüller), Intl. Congress on Mathematical Software (ICMS 2016), 2016. (poster)
[218]Automating Free Logic in Isabelle/HOL (Christoph Benzmüller), Intl. Congress on Mathematical Software (ICMS 2016), 2016. (slides, Isabelle/HOL_paper_source, Isabelle/HOL_further_experiments)
[217](Invited Panel) Erwachen der Roboter – lernende Maschinen und die Intelligenz der Zukunft (Christoph Benzmüller), Bundeszentrale für politische Bildung – bpb, Berlin, 2016. (July)
[216]Hands-on Higher-order Modal Logics in Isabelle/HOL (Christoph Benzmüller), UITP 2016, Coimbra, Portugal, 2016. (July)
[215]TPTP and Beyond: Representation of Quantified Non-Classical Logics (Christoph Benzmüller), ARQNL 2016, Coimbra, Portugal, 2016. (July)
[214](Invited) Automatisierung von Gödel's Gottesbeweis im Computer (Christoph Benzmüller), Auticon GmbH, Berlin, 2016. (June)
[213](Invited keynote) Künstliche Intelligenz---Wohin geht die Reise? (Christoph Benzmüller), Shared Services and Outsourcing Woche (http://www.sharedserviceswoche.de/mediacenter), Berlin, 2016. (slides (without movies))
[212](Invited) Computational Metaphysics (Christoph Benzmüller), Central Teaching Award Acceptance Speech at FU Berlin, 2016. (slides (without movies))
[211](Invited) Computational Metaphysics (Christoph Benzmüller), Thematic trimester 'Current Issues in the Philosophy of Practice of Mathematics and Informatics', Centre International de Mathématiques et d'Informatique de Toulouse (CIMI), France, 2016. (June)
[210](Invited) The Inconsistency in Gödel’s Ontological Argument: An Application of Mathematical Proof Assistants in Metaphysics (Christoph Benzmüller), Mathematical Logic Seminar, Stanford University, USA, 2016. (slides)
[209](Invited tutorial) A Universal Logic Theorem Proving Approach (Christoph Benzmüller), Berkeley-Stanford Circle in Logic and Philosophy, San Francisco, USA, 2016. (February)
[208](Invited) A Success Story of Higher-Order Theorem Proving in Computational Metaphysics (Christoph Benzmüller), Logic Colloquium, University of California, Berkeley, USA, 2016. (February)
2015
[207](Invited keynote) On a (Quite) Universal Theorem Proving Approach and its Application to Metaphysics (Christoph Benzmüller), Tableaux 2015, Wroclaw, Poland, 2015. (slides)
[206](Invited lecture course) Higher-Order Modal Logics: Automation and Applications (Christoph Benzmüller, Bruno Woltzenlogel Paleo), The 11th Reasoning Web Summer School, 2015. (slides)
[205](Invited) Experiments in Computational Metaphysics (Christoph Benzmüller), SRI International, Menlo Park, USA, 2015. (December)
[204](Invited lecture course) Higher-Order Modal Logics (Christoph Benzmüller, Bruno Woltzenlogel Paleo), Logic Summer School, ANU Canberra, Australia, 2015. (slides)
[203](Invited keynote) Experiments in Computational Metaphysics (Christoph Benzmüller), 9th All India Students' Conference on Science and Spiritual Quest (AISSQ), IIT Kharagpur, India, 2015. (slides)
[202](Invited) Experiments in Computational Metaphysics (Christoph Benzmüller), Computational Logic Seminar (MUGS), Stanford University, USA, 2015. (October)
[201](Invited) Higher-Order Proofs and Models -- Examples from Meta-Logical Reasoning and Metaphysics (Christoph Benzmüller), Dagstuhl Seminar 15381 --- Deduction: Models and Proofs, 2015. (October)
[200](Invited) ''Gottesbeweis'' reloaded --- Analyzing Variants of the Ontological Argument with the Computer (Christoph Benzmüller), Lange Nacht der Wissenschaften, Berlin, Germany, 2015. (slides)
[199]Einführung in die Komplexitätsklassen P und NP (Christoph Benzmüller), Universität Leipzig, 2015.
[198](Invited) Towards Computational Metaphysics (Christoph Benzmüller), Universität Leipzig, 2015.
[197](Invited keynote) Gödel's Ontological Argument Revisited -- Findings from a Computer-supported Analysis (Christoph Benzmüller), 1st World Congress on Logic and Religion, João Pessoa, Brazil, 2015. (slides)
[196](Invited) Towards Computational Metaphysics --- Bridging between Mathematical Logic, Artificial Intelligence and Philosophy (Christoph Benzmüller), Berlin Mathematical School, lecture series on 'Bridges between mathematics and its applications', Technical University Berlin, Germany, 2015.
[195]Der ABox-Vervollständigungsalgorithmus für ALC (Christoph Benzmüller), Friedrich-Alexander-Universität, Erlangen-Nürnberg, Germany, 2015.
[194](Invited) Towards Computational Metaphysics --- Techniques and Tools for Knowledge Representation and Reasoning in Expressive Ontologies (Christoph Benzmüller), Friedrich-Alexander-Universität, Erlangen-Nürnberg, Germany, 2015.
2014
[193](Invited keynote) On Logic Embeddings and Gödel's God (Christoph Benzmüller), 21. Jahrestagung der GI-Fachgruppe `Logik in der Informatik', University of Kassel, Germany, 2014. (slides)
[192](Invited keynote) On Logic Embeddings and Gödel's God (Christoph Benzmüller), 22nd International Workshop on Algebraic Development Techniques, Sinaia, Romania, 2014. (slides)
[191]Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers (Christoph Benzmüller), 21st European Conference on Artificial Intelligence (ECAI), Prague, Czech Republic, 2014. (slides)
[190]HOL based First-order Modal Logic Provers (Christoph Benzmüller), ARQNL Workshop at VSL'2014, Vienna, Austria, 2014. (slides)
[189](Invited tutorial) Higher-Order Automated Theorem Provers (Christoph Benzmüller), APPA Workshop at VSL'2014, Vienna, Austria, 2014. (slides)
[188]Gödel's Unvollständigkeitssätze (Christoph Benzmüller), Freie Universität Berlin, Germany, 2014. (slides)
[187](Invited) Kurt Gödel's Gottesbeweis auf dem Computer (Christoph Benzmüller), Marburg, Germany, 2014. (slides)
[186](Invited) Gödel's God on the Computer (Christoph Benzmüller), IT University Copenhagen, Denmark, 2014.
[185](Invited) Gödel's God on the Computer (Christoph Benzmüller), Informatikkolloquium, The University of Innsbruck, Austria, 2014.
[184](Invited) Kurt Gödel's Gottesbeweis auf dem Computer (Christoph Benzmüller), Lange Nacht der Wissenschaften, Berlin, Germany, 2014.
[183]Gödel's Proof of God's Existence (Christoph Benzmüller, Bruno Woltzenlogel-Paleo), World Congress on the Square of Opposition VI, Vatican, 2014. (slides)
2013
[182]A Top-down Approach to Combining Logics (Christoph Benzmüller), 5th International Conference on Agents and Artificial Intelligence, Barcelona, Spain, 2013. (slides)
[181]HOL based Universal Reasoning (Christoph Benzmüller), 4th World Congress and School on Universal Logic, Rio de Janeiro, Brazil, 2013. (slides)
[180]Cut-free calculi for challenge logics in a lazy way (Christoph Benzmüller), International Workshop on Algebraic Logic in Computer Science (ALCS 2013), Stellenbosch, South Africa, 2013. (slides)
[179](Invited keynote) Gödel's God on the Computer (Christoph Benzmüller), The 10th International Workshop on the Implementation of Logics (IWIL 2013), Stellenbosch, South Africa, 2013. (slides)
[178]HOL based First-order Modal Logic Provers (Christoph Benzmüller), The 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2013), Stellenbosch, South Africa, 2013. (slides)
[177]Formalization, Mechanization and Automation of Gödel's Proof of God's Existence (Christoph Benzmüller, Bruno Woltzenlogel Paleo), Informatik Kolloquium, Freie Universität Berlin, Germany, 2013. (slides)
[176]Automating Quantified Conditional Logics is (relatively) Easy (Christoph Benzmüller), Deduktionstreffen 2013, Koblenz, Germany, 2013. (slides)
[175]Automated Consistency Checking of Expressive Ontologies --- Beware of the Wrong Interpretation of Success! (Christoph Benzmüller), The 5th International Workshop on Acquisition, Representation and Reasoning with Contextualized Knowledge (ARCOE-LogIC 2013), Corunna, Spain, 2013. (slides)
[174]Automating Quantified Conditional Logics in HOL (Christoph Benzmüller), 23rd International Joint Conference on Artificial Intelligence (IJCAI 2013), Beijing, China, 2013. (poster)
[173]The Watson System -- An Overview (Christoph Benzmüller), Freie Universität Berlin, Germany, 2013.
[172]LEO-II version 1.5 (Christoph Benzmüller), Third International Workshop on Proof Exchange for Theorem Proving (PxTP 2013), Lake Placid, NY, USA, 2013. (slides)
2012
[171]Gödel's Unvollständigkeitssätze (Christoph Benzmüller), Freie Universität Berlin, Germany, 2012. (slides)
[170](Invited) Konzepte und Nutzen von Lambda-Ausdrücken in Java 8 (und Scala) (Christoph Benzmüller), Beuth Hochschule für Technik, Berlin, Germany, 2012. (slides)
[169]Implementing and Evaluating Provers for First-order Modal Logics (Christoph Benzmüller, Jens Otten), European Conference on Artificial Intelligence (ECAI-2012), Montpellier, France, 2012. (slides)
[168](Invited) LEO-II --- Eine universelle Logikmaschine (Christoph Benzmüller), Beuth Hochschule für Technik, Berlin, Germany, 2012.
[167](Invited) Automating Expressive Classical and Non-Classical Logics with LEO-II, Computer Science Colloquium (Christoph Benzmüller), Computer Science Colloquium, Freie Universität Berlin, Germany, 2012.
[166](Invited) Utilizing Higher-order Automated Theorem Provers as Universal Logic Engines (Christoph Benzmüller), Retirement Celebration of Peter Andrews, Carnegie Mellon University, USA, 2012. (slides)
[165](Invited) Utilizing Church's Type Theory as a Universal Logic (Christoph Benzmüller), Collegium Logicum Lecture Series, Kurt Gödel Society, Vienna, Austria, 2012. (slides)
2011
[164](Invited) Mechanization and Automation of Combinations of Classical and Non-Classical Logics in Classical Higher Order Logics (Christoph Benzmüller), Colloquium New Trends in Computational Logic, TU Dresden, Germany, 2011.
[163](Invited) Mechanisierung und Automatisierung von Kombinationen klassischer und nichtklassischer Logiken in klassischer Logik höherer Stufe (Christoph Benzmüller), University of Hamburg, Germany, 2011.
[162](Invited) Der Automatische Theorembeweiser LEO-II (Christoph Benzmüller), BMW Group, Munich, Germany, 2011.
[161](Invited) Intelligente Werkzeuge zur Erhebung, Bereitstellung, Analyse und Kommunikation von diversifiziertem, personifiziertem, interoperablen semantischen Wissen (Christoph Benzmüller), Deutsches Institut für Wirtschaftsforschung, Berlin, Germany, 2011.
[160]Quantified Conditional Logics are Fragments of HOL (Christoph Benzmüller), The International Conference on Non-classical Modal and Predicate Logics Guangzhou, China, 2011. (slides, [movie])
[159](Invited) Automating Expressive Non-classical Logics and their Combinations in Classical Higher Order Logic (Christoph Benzmüller), University of Potsdam, Germany, 2011. (slides)
2010
[158]Simple Type Theory as Framework for Combining Logics (Christoph Benzmüller), Contest presentation at the World Congress and School on Universal Logic III (UNILOG'2010), Lisbon, Portugal, 2010. (slides)
[157]Progress in Automating Higher-Order Ontology Reasoning (Christoph Benzmüller), Workshop on Practical Aspects of Automated Reasoning (PAAR-2010), Edinburgh, UK, 2010. (slides)
[156]Combining Logics in Simple Type Theory (Christoph Benzmüller), 11th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA XI), Lisbon, Portugal, 2010. (slides)
[155]Ontology Archaeology: Mining a Decade of Effort on the Suggested Upper Ontology (Christoph Benzmüller), The ECAI-10 Workshop on Automated Reasoning about Context and Ontology Evolution (ARCOE-10), Lisbon, Portugal, 2010. (slides)
[154]Reasoning with Embedded Formulas and Modalities in SUMO (Christoph Benzmüller), The ECAI-10 Workshop on Automated Reasoning about Context and Ontology Evolution (ARCOE-10), Lisbon, Portugal, 2010. (slides)
[153]Sigma: An Integrated Development Environment for Logical Theory Development (Christoph Benzmüller), The ECAI 2010 Workshop on Intelligent Engineering Techniques for Knowledge Bases (IKBET'2010), Lisbon, Portugal, 2010. (slides)
[152](Invited) Combining Logics in Simple Type Theory (and an Application in Ontology Reasoning) (Christoph Benzmüller), SRI International, Menlo Park, USA, 2010. (slides)
[151](Invited) Winner Presentation: LEO-II (Christoph Benzmüller), CASC-J5, Fifth International Joint Conference on Automated Reasoning (IJCAR 2010), Edinburgh, UK, 2010. (slides)
[150](Invited) Adaptive Assertion-Level Proofs (Christoph Benzmüller, Marvin Schiller), The IJCAR 2010 Workshop on Evaluation Methods for Solvers and Quality Metrics for Solutions, Edinburgh, UK, 2010. (slides)
[149](Invited) Three presentations at Dagstuhl Seminar 10412 QSTRLib: A Benchmark Problem Repository for Qualitative Spatial and Temporal Reasoning, Dagstuhl, Germany, October 10-13, 2010: Reasoning within and about Combinations of Logics in Simple Type Theory (talk and system demonstration), Participant Introduction, and QSTRLib Use Case: Educational Question Answering on Spatial Configurations of Countries, States, and Cities. (Christoph Benzmüller), Dagstuhl Seminar 10412: QSTRLib, Schloss Dagstuhl, Germany, 2010.
2009
[148]Automating Quantified Multimodal Logics in HOL --- My very first Region Connection Calculus Prover (Christoph Benzmüller), AAAI 2009 Spring Symposia, Stanford, USA, 2009.
[147]Handover of the Festschrift to Peter B. Andrews (Christoph Benzmüller), CADE-22, Montreal, Canada, 2009.
[146]Automating Access Control Logics in Simple Type Theory with LE0-II (Christoph Benzmüller), 24th IFIP International Information Security Conference, Pafos, Cyprus, 2009. (slides)
[145]Granularity-Adaptive Proof Presentation (poster) (Marvin Schiller, Christoph Benzmüller), AIED, 2009. (poster)
2008
[144]Some Results of the LEO-II Project (Christoph Benzmüller), CIAO Workshop, TU Darmstadt, Germany, 2008.
[143]Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II (Christoph Benzmüller), Automated Reasoning Group Lunch Talk, The University of Cambridge, UK, 2008.
[142]Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II (Christoph Benzmüller), Deduktionstreffen, Saarbrücken, Germany, 2008.
[141]LEO-II Demo (Christoph Benzmüller), ESHOL Workshop at the 4th International Joint Conference on Automated Reasoning (IJCAR 2008), Sydney, Australia, 2008. (slides)
[140]THF0 --- The Core TPTP Language for Classical Higher-Order Logic (Christoph Benzmüller), The 4th International Joint Conference on Automated Reasoning (IJCAR 2008), Sydney, Australia, 2008.
[139]LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) (Christoph Benzmüller), The 4th International Joint Conference on Automated Reasoning (IJCAR 2008), Sydney, Australia, 2008. (slides)
[138](Invited) Exploring Properties of Multimodal Logics with the Cooperative Automatic Higher-Order Theorem Prover LEO-II (Christoph Benzmüller), SRI International, Menlo Park, USA, 2008. (slides)
[137]LEO-II, A Higher-Order Theorem Prover (poster) (Christoph Benzmüller), VSI, 2008. (poster)
[136](Invited) Tool Support for Formalized Mathematics: Cooperative Higher-Order Theorem Proving with LEO-II, Tutorial Dialogues on Proofs with the DIALOG demonstrator, and the PLATO/OMEGA Proof Assistant Plug-in for TeXmacs (Christoph Benzmüller), Formal Mathematics Seminar, University of Bonn, Germany, 2008. (slides)
[135](Invited) LEO-II --- A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (Christoph Benzmüller), Microsoft Research, Redmond, USA, 2008.
[134](Invited) Automating Access Control Logics and Multimodal Logics in the Automatic Higher-Order Theorem Prover LEO-II (Christoph Benzmüller), Kestrel Institute, Palo Alto, USA, 2008.
[133](Invited) Automating Access Control Logics and Multimodal Logics in the Automatic Higher-Order Theorem Prover LEO-II (Christoph Benzmüller), Pure and Applied Logic Seminar, Carnegie Mellon University, Pittsburgh, USA, 2008. (slides)
2007
[132]The LEO-II Project (Christoph Benzmüller), Omega-Ultra-Texmacs Mini Workshop, Saarbrücken, Germany, 2007.
[131]The LEO-II Project (Christoph Benzmüller), Deduktionstreffen, Koblenz, Germany, 2007.
[130]The LEO-II Project (Christoph Benzmüller), Automated Reasoning Workshop, London, UK, 2007.
[129]Progress Report on LEO-II: An Automatic Theorem Prover for Higher-Order Logic (Christoph Benzmüller), Automated Reasoning Group Lunch Talk, The University of Cambridge, UK, 2007. (slides)
[128]Progress Report on LEO-II: An Automatic Theorem Prover for Higher-Order Logic (Christoph Benzmüller), TPHOLs, Kaiserslautern, Germany, 2007. (slides)
[127](Invited) Challenges for Automated Theorem Proving in Classical Higher Order Logics (Christoph Benzmüller), Heriot-Watt University, Edinburgh, Scotland, 2007.
[126](Invited) Challenges for Automated Theorem Proving in Classical Higher Order Logics (Christoph Benzmüller), University of St. Andrews, St. Andrews, Scotland, 2007. (slides)
[125](Invited) Challenges for Automated Theorem Proving in Classical Higher Order Logics (Christoph Benzmüller), The University of Edinburgh, Scotland, 2007.
[124](Invited tutorial) Semantics of Higher-Order Logics (Christoph Benzmüller), Invited Lecture Course at ITU Copenhagen, Denmark, 2007. (slides)
[123](Invited) Effiziente Automatisierung von Logik höherer Stufe ---- realisierbarer Traum oder ewiger Albtraum? (Christoph Benzmüller), Inaugural Lecture (Privatdozent) at Saarland University, Germany, 2007.
[122]Deep Inference for Automated Proof Tutoring (poster) (Christoph Benzmüller, Dominik Dietrich, Marvin Schiller, Serge Autexier), KI, 2007. (poster)
[121]LEO-II, A Higher-Order Theorem Prover (poster) (Christoph Benzmüller), TPHOLs, 2007. (poster)
[120]The LEO-II Project (poster) (Christoph Benzmüller), University of Cambridge Project Poster, 2007. (poster)
[119]The LEO-II Project (poster) (Christoph Benzmüller), Deduktionstreffen, 2007. (poster)
[118]Term Indexing for the LEO-II Prover (poster) (Frank Theiss, Christoph Benzmüller), Deduktionstreffen, 2007.
2006
[117]Dialog mit einem Beweisassistenten in natürlicher Sprache (Christoph Benzmüller), Ringvorlesung, FR Informatik, Universität des Saarlandes, Germany, 2006. (slides)
[116]Underspecification in Math-DIALOG (Christoph Benzmüller), C-Tag, SFB 378, Saarland University, Germany, 2006. (slides)
[115]Cut-Simulation in Impredicative Logics (Christoph Benzmüller), Third International Joint Conference on Automated Reasoning (IJCAR 2006), LNAI , Seattle, USA, 2006. (slides)
[114]Term Indexing for the LEO-II Prover (Christoph Benzmüller), IWIL-6 workshop at LPAR 2006: The 6th International Workshop on the Implementation of Logics, Pnom Penh, Cambodia, 2006. (slides)
[113]Judging Granularity for Automated Mathematics Teaching (Christoph Benzmüller), Short paper at LPAR 2006: 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning, Pnom Penh, Cambodia, 2006. (slides)
[112](Invited) Semantics of Higher-Order Logics (Christoph Benzmüller), Invited Lecture Course at ESSLLI 2006, Malaga, Spain, 2006. (slides)
[111](Invited) Service Oriented Architectures for Mathematics Assistance Systems (Christoph Benzmüller), Fachhochschule Frankfurt am Main, Germany, 2006.
[110](Invited) Classical Higher-Order Logic --- Semantics, Proof Theory and Automation (Christoph Benzmüller), University of Potsdam, Germany, 2006.
[109](Invited) Classical Higher-Order Logic --- Theory, Applications and Problems (Christoph Benzmüller), Saarland University (scientific habilitation talk), Germany, 2006. (slides)
[108]Granularity Judgments in Proof Tutoring (poster) (Marvin Schiller, Christoph Benzmüller), KI, 2006. (poster)
2005
[107]Can a Higher-Order and a First-Order Theorem Prover Cooperate? (Christoph Benzmüller), LPAR'04 Conference, Montevideo, Uruguay, 2005. (slides)
[106]New Directions in the OMEGA Project (Christoph Benzmüller), CIAO'05 Workshop, Nottingham, UK, 2005. (slides)
[105]Designing a Proof GUI for non-Experts: Evaluation of an Experiment (Christoph Benzmüller), UITP'05 Workshop (ETAPS Satellite Workshop), Edinburgh, Scotland, 2005. (slides)
[104]New Directions in the OMEGA Project (Christoph Benzmüller), First Saarbrücken-Nancy Workshop on Higher-order Logic and Hybrid Logics, 2005.
[103]Mathematical Domain Reasoning Tasks in Tutorial Natural Language Dialog on Proofs (Christoph Benzmüller), Twentieth National Conference on Artificial Intelligence (AAAI-05), Pittsburgh, Pennsylvania, USA, 2005. (slides)
[102]Mathematical Domain Reasoning Tasks in Tutorial Natural Language Dialog on Proofs (Christoph Benzmüller), Dream Group Reunion, Edinburgh, UK, 2005. (slides)
[101](Invited) A Structured Set of Higher-Order Problems (Christoph Benzmüller), Dagstuhl Seminar 05431: Deduction and Applications, Schloss Dagstuhl, Germany, 2005. (slides)
[100]Mathematical Domain Reasoning Tasks in Tutorial Natural Language Dialog on Proofs (Christoph Benzmüller), Theorema-Ultra-Omega-Workshop, Saarbrücken, Germany, 2005. (slides)
[99]Combining Proofs of Higher-Order and First-Order Automated Theorem Provers (Christoph Benzmüller), LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL), Montego Bay, Jamaica, 2005.
[98]System Description: LEO --- A Resolution based Higher-Order Theorem Prover (Christoph Benzmüller), LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL), Montego Bay, Jamaica, 2005.
[97](Invited) Three Approaches for Guiding the Cooperation of Mathematical Reasoning Systems: Proof Planning, Agent-based Reasoning, and Autometad Composition of Reasoning Web Service (Christoph Benzmüller), QSL Theme day: Integration of deductive tools. Nancy, France, 2005. (slides)
[96](Invited) Can a Higher-Order and a First-Order Theorem Prover Cooperate? (Christoph Benzmüller), LORIA, Nancy, France, 2005. (slides)
[95](Invited) Logik höherer Stufe: Ein geeignetes Fundament für die Mathematik und für Formale Methoden? (Christoph Benzmüller), TU Darmstadt, Germany, 2005.
[94]OMEGA (poster) (Christoph Benzmüller, OMEGA Group), Begehung SFB 378, 2005. (poster-1, poster-2, poster-3, poster-4)
[93]DIALOG (poster) (Christoph Benzmüller, Dialog Group), Begehung SFB 378, 2005. (poster-1, poster-2, poster-3, poster-4)
2004
[92]DIALOG: Natural Language-based Interaction with a Mathematical Assistance System (Christoph Benzmüller), OMEGA talk series, Saarbrücken, Germany, 2004. (slides)
[91]Agent-oriented Proof Planning (Christoph Benzmüller), Evaluation of the Collaborative Research Centre SFB378 Resource-adaptive Cognitive Processes, Saarbrücken, Germany, 2004.
[90]Semantics and Automation of Higher-Order Logic, (Christoph Benzmüller), Workshop on Logic, Proofs, and Programs, Nancy, France, 2004. (slides)
[89]CALCULEMUS Quo Vadis? (Christoph Benzmüller), Special Session at the IJCAR 2004 Workshop on Computer-Supported Mathematical Theory Development together with J. Siekmann, J. Calmet, and W. Windsteiger, Cork, Ireland, 2004.
[88]DIALOG: Natural Language-based Interaction with a Mathematical Assistance System (Christoph Benzmüller), Deduktionstreffen, Saarbrücken, Germany, 2004. (slides)
[87]OMEGA and DIALOG (Christoph Benzmüller), Workshop on Logic, Proofs, and Programs, Saarbrücken, Germany, 2004.
[86](Invited) OMEGA: A Mathematical Assistance System (Christoph Benzmüller), Automated Reasoning Group, Cambridge University, Cambridge, UK, 2004. (slides)
2003
[85]OMEGA (Christoph Benzmüller), Meeting in camera of the Special Research Centre SFB 378, Dagstuhl, Germany, 2003. (slides)
[84]OMEGA - Ein Assistenzsystem für die Mathematik (Christoph Benzmüller), Open day, Saarland University, Saarbrücken, Germany, 2003. (slides)
[83]The CALCULEMUS Research Training Network --- A short Overview (Christoph Benzmüller), First QPQ Workshop on Deductive Software (QPQ'03), CADE-19, Miami, Florida, USA, 2003. (slides)
[82]Tutorial Dialogs on Mathematical Proofs (Christoph Benzmüller), IJCAI-03 Workshop on Knowledge Representation and Automated Reasoning for E-Learning Systems, Acapulco, Mexico, 2003. (slides)
[81]A New Framework for Reasoning Agents (Christoph Benzmüller), IJCAI-03 Workshop on Agents and Automated Reasoning, Acapulco, Mexico, 2003. (slides)
[80]Assertion Application in Theorem Proving and Proof Planning (poster) (Christoph Benzmüller), IJCAI-03 Poster Presentation, Acapulco, Mexico, 2003. (poster)
[79]The CALCULEMUS Research Training Network --- A short Overview (Christoph Benzmüller), CALCULEMUS Symposium 2003, Rome, Italy, 2003. (slides)
[78]Bemerkungen zur Semantik und Mechanisierung von Logik hoeherer Stufe (Christoph Benzmüller), Deduktionstreffen, Augsburg, Germany, 2003. (slides)
[77](Invited) OMEGA --- From Proof Planning towards Mathematical Knowledge Management (Christoph Benzmüller), MKM Symposium 2003, Edinburgh, Scotland, 2003. (slides)
[76]CALCULEMUS Midterm Review Report (Christoph Benzmüller), Midterm Review of the European Union Research Training Network CALCULEMUS, Saarbrücken, Germany, 2003. (slides)
[75]Saarland University Node Report (Christoph Benzmüller), Midterm Review of the European Union Research Training Network CALCULEMUS, Saarbrücken, Germany, 2003. (slides)
[74]CALCULEMUS - Systems for Integrated Deduction and Computation (Christoph Benzmüller), Mathematics on the Semantic Web, Eindhoven, The Netherlands, 2003. (slides)
[73]Proof Development with OMEGA --- Square root of 2 is Irrational (Christoph Benzmüller), Theorema-Omega'03 Workshop, Schloss Hagenberg, Austria, 2003. (slides)
2002
[72](Invited) Tutorial Dialog with a Mathematical Assistant System (Christoph Benzmüller), Computer Science Department, The University of Birmingham, UK, 2002.
[71](Invited tutorial) From Natural Deduction to Sequent Calculus and back (Christoph Benzmüller), CALCULEMUS Autumn School 2002, Pisa, Italy, 2002.
[70]Agent Based Theorem Proving (poster) (Christoph Benzmüller), AISB, 2002. (poster)
[69]Ressource-Adaptive Proof Planning with OMEGA (Christoph Benzmüller), Meeting in camera of the Special Research Centre SFB 378, Wallerfangen, Germany, 2002. (slides)
[68]Tutorial Dialog with a Mathematical Assistant System (Christoph Benzmüller), Meeting in camera of the Special Research Centre SFB 378, Wallerfangen, Germany, 2002. (slides)
[67]Agent based proof search with Indexed Formulas (Christoph Benzmüller), CALCULEMUS 2002, Marseille, France, 2002. (slides)
[66]Tutorial Dialog with a Mathematical Assistant System (Christoph Benzmüller), Computer Science Department, The University of Birmingham, UK, 2002. (slides)
[65]Reasoning Services in the MathWeb-SB for Symbolic Verification of Hybrid Systems (Christoph Benzmüller), VERIFY'02 Workshop at FLOC 2002, Copenhagen, Denmark, 2002.
[64]Proof Development with OMEGA (Christoph Benzmüller), CADE-18, Copenhagen, Denmark, 2002. (slides)
[63]Proof Development with OMEGA: Sqrt(2) is irrational (Christoph Benzmüller), LPAR 2002, Tbilisi, Georgia,, 2002. (slides)
2001
[62](Invited) Concurrent Resource Guided Deduction (Christoph Benzmüller), Theoretical Computer Science Seminar, School of Computer Science, The University of Birmingham, Birmingham, UK, 2001. (slides)
[61](Invited keynote) An Agent-based Approach to Reasoning (Christoph Benzmüller), AISB'01 Convention Agents and Cognition in conjunction with 8th Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice, University of York, UK, 2001. (slides)
[60](Invited) Panel member of the IJCAR 2001 Workshop Future Directions in Automated Reasoning --- Problems and Ideas for a New Millennium (Christoph Benzmüller), IJCAR 2001, Siena, Italy, 2001.
[59](Invited) Agent-oriented Reasoning with O-ANTS (Christoph Benzmüller), Department of Computer Science, Cornell University, Ithaca, NY, USA, 2001.
[58](Invited) Agent-oriented Reasoning with O-ANTS (Christoph Benzmüller), Pure and Applied Logic Seminar, Carnegie Mellon University, Pittsburgh, PA, USA, 2001. (slides)
[57]A Lost Proof (poster) (Christoph Benzmüller, Manfred Kerber), TPHOLs, 2001. (poster)
[56]Proof Transformation and Expansion with a Parameterizable Inference Machine (poster) (Christoph Benzmüller), AISB, 2001. (poster)
[55]OMEGA (poster) (Christoph Benzmüller), Begehung SFB 378, 2001. (poster)
[54]DIALOG (poster) (Christoph Benzmüller), Begehung SFB 378, 2001. (poster)
[53]Tutorielle Kommunikation für ein mathematisches Assistenzsystem (Christoph Benzmüller), Meeting in camera of the Special Research Division SFB378, Schloss Dagstuhl, Germany, 2001.
[52]OMEGA --- Ressourcenadaptives Beweisplanen (Christoph Benzmüller), Meeting in camera of the Special Research Division SFB378, Schloss Dagstuhl, Germany, 2001.
[51]Agents in OMEGA (Christoph Benzmüller), Meeting in camera of the OMEGA group, Saarbrücken, Germany, 2001.
[50]Agent-oriented theorem proving and proof planning in OMEGA (Christoph Benzmüller), C++ days of SFB 378 Resource adaptive cognitive processes, Mertesdorf, Germany, 2001.
[49]A lost proof (Christoph Benzmüller), TPHOLS 2001, Edinburgh, Scotland, 2001.
[48]An Agent-oriented approach to reasoning (Christoph Benzmüller), CALCULEMUS Workshop 2001, Siena, Italy, 2001.
[47]Experiments with an Agent-oriented Reasoning System (Christoph Benzmüller), KI 2001, Wien, Austria, 2001. (slides)
[46]Distributed Assertion Retrieval (Christoph Benzmüller), First International Workshop on Mathematical Knowledge Management RISC-Linz, Schloss Hagenberg, Austria, 2001. (slides)
2000
[45](Invited) OANTS --- An Open Approach at Combining Interactive and Automated Theorem Proving (Christoph Benzmüller), Centre for Agent Research and Development CARD, Department of Computer Science, Manchester Metropolitan University, UK, 2000. (slides)
[44](Invited) Towards Agent based Theorem Proving and Proof Planning in OMEGA (Christoph Benzmüller), Department of Computer Science, The University of York, UK, 2000.
[43](Invited) OMEGA, MATHWEB and Friends (Christoph Benzmüller), Department of Artificial Intelligence, The University of Edinburgh, Edinburgh, Scotland, 2000.
[42](Invited) Resource Guided Concurrent Deduction with O-ANTS (Christoph Benzmüller), Department of Artificial Intelligence, The University of Edinburgh, Edinburgh, Scotland, 2000.
[41]Proof Planning based on a Multi Agent Architecture?">Proof Planning based on a Multi Agent Architecture? (Christoph Benzmüller), 9th CLAM - INKA - OMRS Workshop (CIAO), Schloss Dagstuhl, Germany, 2000.
[40]System demonstration: OMEGA, O-ANTS, and LEO (Christoph Benzmüller), Department of Computer Science, The University of York, York, UK, 2000.
[39]Resource Guided Concurrent Deduction (poster) (Christoph Benzmüller), AISB, 2000. (poster)
[38]Resource Guided Concurrent Deduction (Christoph Benzmüller), Short talk and poster presentation at Automated Reasoning Workshop 2000, King's College, London, UK, 2000.
[37]Towards agent based proof planning (Christoph Benzmüller), Deduktionstreffen, Saarland University, Saarbrücken, Germany, 2000.
[36]OANTS --- An open approach at combining Interactive and Automated Theorem Proving (Christoph Benzmüller), CALCULEMUS Symposium 2000, St. Andrews, Scotland, 2000. (slides)
[35]Eine übersicht zur AG Siekmann (Christoph Benzmüller), Deduktionstreffen, Saarland University, Saarbrücken, Germany, 2000.
[34]Agent based proof planning with O-ANTS (Christoph Benzmüller), Systemdemonstration at the Deduktionstreffen, Saarland University, Saarbrücken, Germany, 2000. (slides)
1999
[33](Invited) Extensional Higher Order Resolution, Paramodulation and RUE-Resolution (Christoph Benzmüller), Theoretical Computer Science Seminar, School of Computer Science, The University of Birmingham, UK, 1999. (slides)
[32](Invited) A two layered Agent Approach for Guiding Interactive Proofs (Christoph Benzmüller), Theoretical Computer Science Seminar, School of Computer Science, The University of Birmingham, UK, 1999.
[31]Towards Fine-Grained Proof Planning with Critical Agents (poster) (Christoph Benzmüller), AISB, 1999. (poster)
[30]Agent based Proof Planning (poster) (Christoph Benzmüller), Poster at the 6th Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice; in conjunction with AISB'99 Convention, Edinburgh, Scotland, 1999.
[29]On Automated Higher-Theorem Proving and Henkin Completeness (Christoph Benzmüller), Forschungskolloquium der Studienstiftung des Deutschen Volkes, Berlin, Germany, 1999. (slides)
[28]Extensional Higher-Order Paramodulation and RUE-Resolution (Christoph Benzmüller), 16th Conference on Automated Deduction, Trento, Italy, 1999. (slides)
[27]Agent Based Mathematical Reasoning (Christoph Benzmüller), CALCULEMUS Workshop, Trento, Italy, 1999. (slides)
[26]Gleichheit und Extensionalität im automatischen Beweisen in Logik höherer Stufe (Christoph Benzmüller), Promotionskolloquium, Saarbrücken, Germany,, 1999.
[25]Critical Agents Supporting Interactive Theorem Proving (Christoph Benzmüller), 9th Portuguese Conference on Artificial Intelligence, Evora, Portugal, 1999. (slides)
[24]Ressourcenadaptive Vorschlagsagenten im Interaktiven Beweisen (Christoph Benzmüller), Kollegiatentag im Rahmen der Herbstschule Kognitionswissenschaft, Saarbrücken, Germany, 1999.
[23]Ist KI eine empirische Wissenschaft? (Christoph Benzmüller), SAG-WAS der AG Siekmann, Schloss Dagstuhl, Germany, 1999.
1998
[22]LEO -- A Higher Order Theorem Prover (Christoph Benzmüller), CADE, 1998. (poster)
[21]Model Existence for Higher-Order Logic (Christoph Benzmüller), Oberseminar AG Siekmann, Saarland University, Saarbrücken, Germany, 1998.
[20]Integrating TPS with OMEGA (Christoph Benzmüller, Volker Sorge), Oberseminar AG Siekmann, Saarland University, Saarbrücken, Germany, 1998.
[19]System Demonstration: OMEGA --- A mathematical Assistant (Christoph Benzmüller), Evaluation of the SFB 378, Max-Planck Institute für Informatik (MPI), Saarbrücken, Germany, 1998.
[18]Exploiting past proof experience + Experiments in the Automatic Selection of Problem-solving Strategies (Christoph Benzmüller), SAG-WAS'98 der AG Siekmann, Schloss Dagstuhl, Germany, 1998.
[17]LEO --- A Higher-Order Theorem Prover (Christoph Benzmüller), The 15th International Conference on Automated Deduction, Lindau, Germany, 1998.
[16]System Demonstration: LEO --- A Higher-Order Theorem Prover (Christoph Benzmüller), The 15th International Conference on Automated Deduction, Lindau, Germany, 1998.
[15]Integrating TPS with OMEGA (Christoph Benzmüller), Workshop Inference Mechanisms in Knowledge-Based Systems: Theory and Applications, KI'98, Bremen, Germany, 1998.
[14]System Demonstration: Integrating TPS with OMEGA (Christoph Benzmüller), Workshop Inference Mechanisms in Knowledge-Based Systems: Theory and Applications, KI'98, Bremen, Germany, 1998.
[13]Constraint Solving in Logig Programming and Automated Theorem Proving: a comparison (Christoph Benzmüller), 8th International Conference on Artificial Intelligence: Methodology, Systems, Applications (AIMSA'98), Sozopol, Bulgaria, 1998.
[12]System Demonstration: OMEGA --- a Mathematical Assistant (Christoph Benzmüller), 8th International Conference on Artificial Intelligence: Methodology, Systems, Applications (AIMSA'98), Sozopol, Bulgaria, 1998.
[11]System Demonstration: OMEGA --- a Mathematical Assistant (Christoph Benzmüller), Deduktionstreffen, Munich, Germany, 1998.
[10]System Demonstration: OMEGA --- a Mathematical Assistant (Christoph Benzmüller), Informatikforum '98 (Max-Planck-Institut für Informatik, Deutsches Forschungszentrum für Künstliche Intelligenz und Fachbereich Informatik der Uni des Saarlandes) Saarbrücken, Germany, 1998.
1997
[9]LEO --- Towards Higher-Order Resolution (Christoph Benzmüller), Automated theorem proving seminar, Department of Mathematics, Carnegie Mellon Univerity, Pittsburgh, USA, 1997. (slides)
[8]Equalizing terms by Difference Reduction and Abstraction (Christoph Benzmüller), Automated theorem proving seminar, Department of Mathematics, Carnegie Mellon Univerity, Pittsburgh, USA, 1997.
[7]Embedding Extensionality in Higher-Order Resolution (Christoph Benzmüller), Oberseminar AG Siekmann, Saarland University, Saarbrücken, Germany, 1997.
[6]Extensionale Resolution höherer Stufe (Christoph Benzmüller), Deduktionstreffen, Schloss Dagstuhl, Germany, 1997.
[5]Extensionale Resolution höherer Stufe (Christoph Benzmüller), Forschungskolloquium der Studienstiftung des Deutschen Volkes, Kochl am See, Germany, 1997.
1996
[4]Higher-Order Resolution and Extensionality (Christoph Benzmüller), Oberseminar AG Siekmann, Saarland University, Saarbrücken, Germany, 1996. (slides)
[3]Ein kategorieller Kalkül ebener und räumlicher Netze (Christoph Benzmüller), Sommerakademie der Studienstiftung des Deutschen Volkes, St. Johann, Südtirol, Italy, 1996.
1995
[2]HO-Differenzreduzierung (Christoph Benzmüller), Oberseminar AG Siekmann, Saarland University, Saarbrücken, Germany, 1995.
[1]Towards Higher-Order Theorem Proving with equality (Christoph Benzmüller), Deduktionstreffen, Saarland University, Saarbrücken, Germany, 1995. (slides)
Powered by bibtexbrowser