Keywords: Henkin Semantics
2013
[23] 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]
[22] 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]
2011
[21] 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]
2010
[20] 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]
[19] 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]
2009
[18] LEO-II im Ontologieschliessen -- Antrag auf ein Forschungsvorhaben an die DFG (Christoph Benzmüller), 2009. [bibtex] [pdf]
[17] 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]
[16] Automating Access Control Logic in Simple Type Theory with LEO-II (Christoph Benzmüller), In Emerging Challenges for Security, Privacy and Trust, 24th IFIP TC 11 International Information Security Conference, SEC 2009, Pafos, Cyprus, May 18-20, 2009. Proceedings (Dimitris Gritzalis, Javier López, eds.), Springer, IFIP, volume 297, pp. 387-398, 2009. (slides) [bibtex] [pdf] [doi]
2008
[15] 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]
[14] 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]
[13] 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]
2006
[12] Cumulative Habilitation Script (Christoph Benzmüller), Saarland University, Germany, pp. 1-357, 2006. [bibtex] [pdf]
[11] 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]
2005
[10] 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]
[9] 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]
2004
[8] 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]
2003
[7] 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]
[6] 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
[5] 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]
1999
[4] 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]
[3] 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]
1998
[2] 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]
[1] 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]
Powered by bibtexbrowser