Datastructures; Automated Reasoning; LEO Prover; Higher Order Logic; Agents
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)
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 :
LeoPARD - A Generic Platform for the Implementation of Higher-Order Reasoners
Publication date :
June 2015
Event name :
Intelligent Computer Mathematics. CICM 2015
Event place :
Washington D.C., United States
Event date :
July 13-17, 2015
Audience :
International
Main work title :
Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings
Abadi, M., Cardelli, L., Curien, P.-L., Levy, J.-J.: Explicit substitutions. In: Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1990, pp. 31–46, ACM, New York (1990)
Arrow, K.J.: Social Choice and Individual Values. Wiley, New York (1951)
Barendregt, H.P.: Introduction to generalized type systems. J. of Funct. Program. 1(2), 125–154 (1991)
Benzmüller, C.E., Kohlhase, M.: System description: LEO - a higher-order theorem prover. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, p. 139. Springer, Heidelberg (1998)
Benzmüller, C., Sorge, V.: OANTS - combining interactive and automated theorem proving. In: Kerber, M., Kohlhase, M. (eds.) Symbolic Computation and Automated Reasoning, pp. 81–97. A.K.Peters, Massachusetts (2001)
Benzmüller, C., Sorge, V., Jamnik, M., Kerber, M.: Combined reasoning by automated cooperation. J. Appl. Log. 6(3), 318–342 (2008)
Benzmüller, C., Paulson, L., Theiss, F., Fietzke, A.: LEO-II - a cooperative automatic theorem prover for classical higher-order logic (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 162–170. Springer, Heidelberg (2008)
Blanchette, J., Böhme, S., Paulson, L.: Extending sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109–128 (2013)
Bonacina, M.P.: A taxonomy of parallel strategies for deduction. Ann. Math. Artif. Intell. 29(1–4), 223–257 (2000)
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)
De Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. INDAG. MATH 34, 381–392 (1972)
Cervesato, I., Pfenning, F.: A linear spine calculus. J. Log. Comput. 13(5), 639–688 (2003)
Gacek, A.: The Abella interactive theorem prover (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 154–161. Springer, Heidelberg (2008)
Girard, J.Y.: Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. Ph.D. thesis, Paris VII (1972)
Kfoury, A.J., Ronchi Della Rocca, S., Tiuryn, J., Urzyczyn, P.: Della Rocca, J. Tiuryn, and P. Urzyczyn. Alpha-conversion and typability. Inf. Comput. 150(1), 1–21 (1999)
Reynolds, J.C.: Towards a theory of type structure. In: Robinet, B. (ed.) Symposium on Programming. LNCS, vol. 19, pp. 408–423. Springer, Heidelberg (1974)
Liang, C., Mitchell, D.: System description: Teyjus - a compiler and abstract machine based implementation of λProlog. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 287–291. Springer, Heidelberg (1999)
Pfenning, F., Schürmann, C.: System description: Twelf - a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)
Riazanov, A.: Implementing an efficient theorem prover. Ph.D. thesis, University of Manchester (2003)
Sekar, R., Ramakrishnan, I.V., Voronkov, A.: Term indexing. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1853–1964. Elsevier Science Publishers B.V., Amsterdam (2001)
Steen, A.: Efficient data structures for automated theorem proving in expressive higher-order logics. Master’s thesis, Freie Universit¨at Berlin (2014). http://userpage.fu-berlin.de/∼lex/drop/steendatastructures.pdf
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)
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). http://userpage.fu-berlin.de/∼lex/drop/wisniewski_architecture.pdf
