Higher Order Logic; Automated Reasoning; LEO Prover
Disciplines :
Computer science
Author, co-author :
Steen, Alexander ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Wisniewski, Max; 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 :
Agent-Based HOL Reasoning
Publication date :
July 2016
Event name :
5th International Congress on Mathematical Software
Event place :
Berlin, Germany
Event date :
July 11 to July 14, 2016
Audience :
International
Main work title :
Mathematical Software -- ICMS 2016, 5th International Congress, Proceedings
Benzmüller, C., Brown, C., Kohlhase, M.: Higher-order semantics and extensionality. J. Symbolic Logic 69(4), 1027-1088 (2004)
Barendregt, H.P., Dekkers,W., Statman, R.: Lambda Calculus with Types. Perspectives in Logic. Cambridge University Press, Cambridge (2013)
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.: Invited talk: on a (quite) universal theorem proving approach and its application in metaphysics. In: De Nivelle, H. (ed.) TABLEAUX 2015. LNCS, vol. 9323, pp. 213-220. Springer, Heidelberg (2015)
Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Logic Comput. 4(3), 217-247 (1994)
Benzmüller, C., Miller, D.: Automation of higher-order logic. In: Gabbay, D.M., Siekmann, J.H., Woods, J. (eds.) Handbook of the History of Logic. Computational Logic, vol. 9, pp. 215-254. Elsevier, North Holland (2014)
Benzmüller, C., Paulson, L.C., Sultana, N., Theiß, F.: The higher-order prover LEO-II. J. Autom. Reasoning 55(4), 389-404 (2015)
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)
Chalkiadakis, G., Elkind, E., Wooldridge, M.: Computational Aspects of Cooperative Game Theory. Synthesis Lectures on Artificial Intelligence and Machine Learning. Morgan & Claypool Publishers, San Rafael (2011)
Church, A.: A formulation of the simple theory of types. J. Symbolic Logic 5(2), 56-68 (1940)
Frege, G.: Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Verlag von Louis Nebert, Halle (1879)
Gödel, K.: über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme. Monatshefte für Mathematik und Physik 38(1), 173-198 (1931)
Henkin, L.: Completeness in the theory of types. J. Symbolic Logic 15(2), 81-91 (1950)
Meng, J., Paulson, L.C.: Lightweight relevance filtering for machinegenerated resolution problems. J. Appl. Logic 7(1), 41-57 (2009)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reasoning 43(4), 337-362 (2009)
Wisniewski, M., Benzmüller, C.: Is it reasonable to employ agents in theorem proving? In: van den Heerik, J., Filipe, J. (eds.) Proceedings of the 8th International Conference on Agents and Artificial Intelligence (ICAART), Rome, Italy, 2016, vol. 1, pp. 281-286. SCITEPRESS - Science and Technology Publications, Lda (2016)
Weiss, G. (ed.): Multiagent Systems. MIT Press, Cambridge (2013)
Wisniewski, M.: Agent-based Blackboard Architecture for a Higher-Order Theorem Prover. Master’s thesis, Freie Universität Berlin (2014)
Wisniewski, M., Steen, A., Benzmüller, C.: LeoPARD - a generic platform for the implementation of higher-order reasoners. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 325-330. Springer, Heidelberg (2015)
Wisniewski, M., Steen, A., Kern, K., Benzmüller, C.: Effective normalization techniques for HOL. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 362-370. Springer, Heidelberg (2016). doi: 10.1007/978-3-319-40229-1_25