Higher Order Logic; Automated Reasoning; LEO Prover
Disciplines :
Computer science
Author, co-author :
Wisniewski, Max; Freie Universität Berlin
Steen, Alexander ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Kern, Kim; Freie Universität Berlin
Benzmüller, Christoph ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
External co-authors :
yes
Language :
English
Title :
Effective Normalization Techniques for HOL
Publication date :
June 2016
Event name :
International Joint Conference on Automated Reasoning
Event place :
Coimbra, Portugal
Event date :
Jun 27, 2016 – Jul 2, 2016
Audience :
International
Main work title :
Automated Reasoning --- 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 -- July 2, 2016, Proceedings
Andrews, P.: Church’s type theory. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Stanford University, Spring (2014)
Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC 4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171-177. Springer, Heidelberg (2011)
Benzmüller, C.: Higher-order automated theorem provers. In: Delahaye, D., Woltzenlogel Paleo, B. (eds.) All about Proofs, Proof for All. Mathematical Logic and Foundations, pp. 171-214. College Publications, London (2015)
Benzmüller, C., Paulson, L.C., Sultana, N., Theiß, F.: The higher-order prover LEO-II. J. Autom. Reason. 55(4), 389-404 (2015)
Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131-146. Springer, Heidelberg (2010)
Brown, C.E.: Satallax: an automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 111-117. Springer, Heidelberg (2012)
Kern, K.: Improved computation of CNF in higher-order logics. Bachelor thesis, Freie Universität Berlin (2015)
Niles, I., Pease, A.: Towards a standard upper ontology. In: Proceedings of the International Conference on Formal Ontology in Information Systems, pp. 2-9. ACM (2001)
Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle/HOL-A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Nonnengart, A., Rock, G., Weidenbach, C.: On generating small clause normal forms. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, pp. 397-411. Springer, Heidelberg (1998)
Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, J., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, pp. 335-367. Gulf Professional Publishing, Houston (2001)
Paulson, L.C.: A generic tableau prover and its integration with isabelle. J. Univers. Comput. Sci. 5(3), 73-87 (1999)
Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 43(4), 337-362 (2009)
Sutcliffe, G., Benzmüller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formaliz. Reason. 3(1), 1-27 (2010)
Weidenbach, C., Gaede, B., Rock, G.: SPASS & FLOTTER version 0. 42. In: McRobbie, M.A., Slaney, J.K. (eds.) Cade-13. LNCS, vol. 1104, pp. 141-145. Springer, Heidelberg (1996)
Wisniewski, M., Steen, A., Benzmüller, C.: The Leo-III project. In: Bolotov, A., Kerber, M. (eds.) Joint Automated Reasoning Workshop and Deduktionstreffen, p. 38 (2014)
