Type: Techreport
2019
[39] Harnessing Higher-Order (Meta-)Logic to Represent and Reason with Complex Ethical Theories (David Fuenmayor, Christoph Benzmüller), Technical report, CoRR, 2019. (http://arxiv.org/abs/1804.02929) [bibtex] [pdf]
2018
[38] First Experiments with a Flexible Infrastructure for Normative Reasoning (Christoph Benzmüller, Xavier Parent), Technical report, CoRR, 2018. (http://arxiv.org/abs/1804.02929) [bibtex] [pdf]
[37] I/O Logic in HOL --- First Steps (Christoph Benzmüller, Xavier Parent), Technical report, CoRR, 2018. (https://arxiv.org/abs/1803.09681) [bibtex] [pdf]
[36] Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL (Christoph Benzmüller, Ali Farjami, Xavier Parent), Technical report, CoRR, 2018. (https://arxiv.org/abs/1802.08454) [bibtex] [pdf]
[35] The Higher-Order Prover Leo-III (Extended Version) (Alexander Steen, Christoph Benzmüller), Technical report, CoRR, 2018. (https://arxiv.org/abs/1802.02732, preprint of IJCAR 2018 paper) [bibtex] [pdf]
2017
[34] A Case Study on Computational Hermeneutics: E. J. Lowe's Modal Ontological Argument (David Fuenmayor, Christoph Benzmüller), Technical report, PhilPapers, 2017. (https://philpapers.org/rec/FUEACS) [bibtex] [pdf]
[33] Mechanizing Principia Logico-Metaphysica in Functional Type Theory (Daniel Kirchner, Christoph Benzmüller, Edward N. Zalta), Technical report, CoRR, 2017. (Preprint of submitted article) [bibtex] [pdf]
[32] Universal Reasoning, Rational Argumentation and Human-Machine Interaction (Christoph Benzmüller), Technical report, CoRR, 2017. (http://arxiv.org/abs/1703.09620) [bibtex] [pdf]
2016
[31] Axiomatizing Category Theory in Free Logic (Christoph Benzmüller, Dana S. Scott), Technical report, CoRR, 2016. (http://arxiv.org/abs/1609.01493) [bibtex] [pdf]
2015
[30]News --- 25th International Conference on Automated Deduction (CADE-25) (Christoph Benzmüller, Alexander Steen, Max Wisniewski), Technical report, , 2015. (Künstliche Intelligenz 29(4):451-452; non-reviewed conference report) [bibtex] [doi]
2012
[29] FMLtoHOL (version 1.0): Automating First-order Modal Logics with LEO-II and Friends (Christoph Benzmüller, Thomas Raths), Technical report, Freie Universität Berlin, Germany, 2012. (arXiv:1207.6685) [bibtex] [pdf]
2011
[28] 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]
2009
[27]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. (Url (preprint): http://christoph-benzmueller.de/papers/R50.pdf) [bibtex]
[26]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. (Url (preprint): http://christoph-benzmueller.de/papers/R49.pdf) [bibtex]
[25] A Note on LEO-II and the Basic Fragment of Simple Type Theory (Christoph Benzmüller), Technical report, AAR Newsletter No. 84, 2009. [bibtex] [pdf]
[24] 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]
[23] 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]
[22] 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]
2008
[21] Automating Access Control Logics in Simple Type Theory with LEO-II (Christoph Benzmüller), SEKI Publications (ISSN 1437-4447), number SR-2008-01, 2008. (arXiv:0901.3574) [bibtex] [pdf]
2006
[20]Cut-Simulation in Impredicative Logics (extended version) (Christoph Benzmüller, Chad Brown, Michael Kohlhase), SEKI Publications (ISSN 1437-4447), number SR-2006-01, 2006. (Url (preprint): http://christoph-benzmueller.de/papers/R39.pdf) [bibtex]
2004
[19]A Dialogue Manager for the DIALOG Demonstrator (Mark Buckley, Christoph Benzmüller), SEKI Publications (ISSN 1437-4447), number SR-04-01, 2004. (Url (preprint): http://christoph-benzmueller.de/papers/R35.pdf) [bibtex]
2003
[18]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. (Url (preprint): http://christoph-benzmueller.de/papers/R21.pdf) [bibtex]
[17]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. (Url (preprint): http://christoph-benzmueller.de/papers/R20.pdf) [bibtex]
[16]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. (Url (preprint): http://christoph-benzmueller.de/papers/R19.pdf) [bibtex]
[15]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. (Url (preprint): http://christoph-benzmueller.de/papers/R18.pdf) [bibtex]
2002
[14] 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]
[13]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. (Url (preprint): http://christoph-benzmueller.de/papers/R16.pdf) [bibtex]
[12]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. (Url (preprint): http://christoph-benzmueller.de/papers/R15.pdf) [bibtex]
2001
[11]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. (Url (preprint): http://christoph-benzmueller.de/papers/R14.pdf) [bibtex]
2000
[10]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. (Url (preprint): http://christoph-benzmueller.de/papers/R13.pdf) [bibtex]
1999
[9] 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]
[8]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. (Url (preprint): http://christoph-benzmueller.de/papers/R11.pdf) [bibtex]
[7]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. (Url (preprint): http://christoph-benzmueller.de/papers/R10.pdf) [bibtex]
1998
[6]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. (Url (preprint): http://christoph-benzmueller.de/papers/R7.pdf) [bibtex]
1997
[5]Henkin Completeness of Higher-Order Resolution (Christoph Benzmüller, Michael Kohlhase), SEKI Publications (ISSN 1437-4447), number SR-97-10, pp. 1-12, 1997. (Url (preprint): http://christoph-benzmueller.de/papers/R6.pdf) [bibtex]
[4]Model Existence for Higher-Order Logic (Christoph Benzmüller, Michael Kohlhase), SEKI Publications (ISSN 1437-4447), number SR-97-09, pp. 1-34, 1997. (Url (preprint): http://christoph-benzmueller.de/papers/R5.pdf) [bibtex]
[3]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. (Url (preprint): http://christoph-benzmueller.de/papers/R4.pdf) [bibtex]
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. (Url (preprint): http://christoph-benzmueller.de/papers/R2.pdf) [bibtex]
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. (Url (preprint): http://christoph-benzmueller.de/papers/R1.pdf) [bibtex]
Powered by bibtexbrowser