Skip to main content

2015 | OriginalPaper | Buchkapitel

LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners

verfasst von : Max Wisniewski, Alexander Steen, Christoph Benzmüller

Erschienen in: Intelligent Computer Mathematics

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

LeoPARD supports the implementation of knowledge representation and reasoning tools for higher-order logic(s). It combines a sophisticated data structure layer (polymorphically typed \(\lambda \)-calculus with nameless spine notation, explicit substitutions, and perfect term sharing) with an ambitious multi-agent blackboard architecture (supporting prover parallelism at the term, clause, and search level). Further features of LeoPARD include a parser for all TPTP dialects, a command line interpreter, and generic means for the integration of external reasoners.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literatur
1.
Zurück zum Zitat 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) 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)
2.
Zurück zum Zitat Arrow, K.J.: Social Choice and Individual Values. Wiley, New York (1951)MATH Arrow, K.J.: Social Choice and Individual Values. Wiley, New York (1951)MATH
3.
Zurück zum Zitat Barendregt, H.P.: Introduction to generalized type systems. J. of Funct. Program. 1(2), 125–154 (1991)MathSciNetMATH Barendregt, H.P.: Introduction to generalized type systems. J. of Funct. Program. 1(2), 125–154 (1991)MathSciNetMATH
4.
Zurück zum Zitat 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) CrossRef 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) CrossRef
5.
Zurück zum Zitat 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.: 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)
6.
Zurück zum Zitat Benzmüller, C., Sorge, V., Jamnik, M., Kerber, M.: Combined reasoning by automated cooperation. J. Appl. Log. 6(3), 318–342 (2008)MathSciNetCrossRefMATH Benzmüller, C., Sorge, V., Jamnik, M., Kerber, M.: Combined reasoning by automated cooperation. J. Appl. Log. 6(3), 318–342 (2008)MathSciNetCrossRefMATH
7.
Zurück zum Zitat 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) CrossRef 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) CrossRef
8.
9.
Zurück zum Zitat Bonacina, M.P.: A taxonomy of parallel strategies for deduction. Ann. Math. Artif. Intell. 29(1–4), 223–257 (2000)CrossRefMATH Bonacina, M.P.: A taxonomy of parallel strategies for deduction. Ann. Math. Artif. Intell. 29(1–4), 223–257 (2000)CrossRefMATH
10.
Zurück zum Zitat 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) CrossRef 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) CrossRef
11.
Zurück zum Zitat 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)MathSciNetCrossRefMATH 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)MathSciNetCrossRefMATH
13.
Zurück zum Zitat 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) CrossRef 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) CrossRef
14.
Zurück zum Zitat Girard, J.Y.: Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. Ph.D. thesis, Paris VII (1972) Girard, J.Y.: Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. Ph.D. thesis, Paris VII (1972)
15.
Zurück zum Zitat 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)CrossRefMATH 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)CrossRefMATH
16.
Zurück zum Zitat 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)CrossRef 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)CrossRef
17.
Zurück zum Zitat Liang, C., Mitchell, D.: System description: Teyjus - a compiler and abstract machine based implementation of \(\lambda \)Prolog. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 287–291. Springer, Heidelberg (1999) CrossRef Liang, C., Mitchell, D.: System description: Teyjus - a compiler and abstract machine based implementation of \(\lambda \)Prolog. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 287–291. Springer, Heidelberg (1999) CrossRef
18.
Zurück zum Zitat 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) CrossRef 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) CrossRef
19.
Zurück zum Zitat Riazanov, A.: Implementing an efficient theorem prover. Ph.D. thesis, University of Manchester (2003) Riazanov, A.: Implementing an efficient theorem prover. Ph.D. thesis, University of Manchester (2003)
20.
Zurück zum Zitat 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) CrossRef 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) CrossRef
22.
Zurück zum Zitat Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 43(4), 337–362 (2009)CrossRefMATH Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 43(4), 337–362 (2009)CrossRefMATH
23.
Zurück zum Zitat Sutcliffe, G., Benzmüller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formaliz. Reason. 3(1), 1–27 (2010)MathSciNetMATH Sutcliffe, G., Benzmüller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formaliz. Reason. 3(1), 1–27 (2010)MathSciNetMATH
24.
Zurück zum Zitat Weiss, G. (ed.): Multiagent Systems. MIT Press, Cambridge (2013) Weiss, G. (ed.): Multiagent Systems. MIT Press, Cambridge (2013)
Metadaten
Titel
LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners
verfasst von
Max Wisniewski
Alexander Steen
Christoph Benzmüller
Copyright-Jahr
2015
DOI
https://doi.org/10.1007/978-3-319-20615-8_22