Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
With Extreme Scale Computing the Rules Have Changed Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Agent-Based HOL Reasoning

Authors : Alexander Steen, Max Wisniewski, Christoph Benzmüller

Published in: Mathematical Software – ICMS 2016

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

In the Leo-III project, a new agent-based deduction system for classical higher-order logic is developed. Leo-III combines its predecessor’s concept of cooperating external specialist systems with a novel agent-based proof procedure. Key goals of the system’s development involve parallelism on various levels of the proof search, adaptability for different external specialists, and native support for reasoning in expressive non-classical logics.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
previous chapter Automated Deduction in Ring Theory
next chapter An Automated Deduction and Its Implementation for Solving Problem of Sequence at University Entrance Examination
Footnotes
1
Detailed information about typed \(\lambda \)-calculi and formal aspects of HOL can e.g. be found in [BDS13, BM14, Ben15a, BBK04] and references therein.
 
2
Further information can e.g. be found in [WB16, Wis14].
 
3
The reasoning in such non-classical logics is enabled by a semantical embedding of the target logic into HOL. Detailed information about this approach can be found, e.g. in [Ben15b] and the references therein.
 
Literature
[BBK04]
[BDS13]
Barendregt, H.P., Dekkers, W., Statman, R.: Lambda Calculus with Types. Perspectives in Logic. Cambridge University Press, Cambridge (2013)CrossRefMATH
[Ben15a]
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)
[Ben15b]
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)CrossRef
[BG94]
Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Logic Comput. 4(3), 217–247 (1994)MathSciNetCrossRefMATH
[BJR15]
Blanqui, F., Jouannaud, J.-P., Rubio, A.: The computability path ordering (2015). CoRR, abs/1506.03943
[BM14]
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)
[BPST15]
Benzmüller, C., Paulson, L.C., Sultana, N., Theiß, F.: The higher-order prover LEO-II. J. Autom. Reasoning 55(4), 389–404 (2015)MathSciNetCrossRefMATH
[Bro12]
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
[CEW11]
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)MATH
[Chu40]
[Fre79]
Frege, G.: Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Verlag von Louis Nebert, Halle (1879)
[God31]
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)CrossRefMATH
[Hen50]
[MP09]
Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Logic 7(1), 41–57 (2009)MathSciNetCrossRefMATH
[NPW02]
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)MATH
[Sut09]
Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reasoning 43(4), 337–362 (2009)CrossRefMATH
[WB16]
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)
[Wei13]
Weiss, G. (ed.): Multiagent Systems. MIT Press, Cambridge (2013)
[Wis14]
Wisniewski, M.: Agent-based Blackboard Architecture for a Higher-Order Theorem Prover. Master’s thesis, Freie Universität Berlin (2014)
[WSB15]
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)CrossRef
[WSKB16]
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 CrossRef
Metadata
Title
Agent-Based HOL Reasoning
Authors
Alexander Steen
Max Wisniewski
Christoph Benzmüller
Copyright Year
2016
Book
Mathematical Software – ICMS 2016

Print ISBN: 978-3-319-42431-6

Electronic ISBN: 978-3-319-42432-3

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-319-42432-3_10

Premium Partner

    Image Credits