Type: Techreport
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] 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]
[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 --- Scientific (Christoph Benzmüller, Geoff Sutcliffe), Saarland University, 2009. [bibtex] [pdf]
[25] 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]
[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. [bibtex] [pdf]
2004
[19] A Dialogue Manager for the DIALOG Demonstrator (Mark Buckley, Christoph Benzmüller), SEKI Publications (ISSN 1437-4447), number SR-04-01, 2004. [bibtex] [pdf]
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. [bibtex] [pdf]
[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. [bibtex] [pdf]
[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. [bibtex] [pdf]
[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. [bibtex] [pdf]
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. [bibtex] [pdf]
[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. [bibtex] [pdf]
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. [bibtex] [pdf]
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. [bibtex] [pdf]
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. [bibtex] [pdf]
[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. [bibtex] [pdf]
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. [bibtex] [pdf]
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. [bibtex] [pdf]
[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. [bibtex] [pdf]
[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. [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