nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Logic-Independent Proof Search in Logical Frameworks

(Short Paper)

verfasst von : Michael Kohlhase, Florian Rabe, Claudio Sacerdoti Coen, Jan Frederik Schaefer

Erschienen in: Automated Reasoning

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

Logical frameworks like LF allow to specify the syntax and (natural deduction) inference rules for syntax/proof-checking a wide variety of logical systems. A crucial feature that is missing for prototyping logics is a way to specify basic proof automation. We try to alleviate this problem by generating \(\lambda \)Prolog (ELPI) inference predicates from logic specifications and controlling them by logic-independent helper predicates that encapsulate the prover characteristics. We show the feasibility of the approach with three experiments: We directly automate ND calculi, we generate tableau theorem provers and model generators.

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel Integrating Induction and Coinduction via Closure Operators and Proof Cycles

Nächstes Kapitel Layered Clause Selection for Theory Reasoning

[Ben+08]

Benzmüller, C., Paulson, L.C., 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). https://doi.org/10.1007/978-3-540-71070-7_14CrossRef

[CMR13]

Chihani, Z., Miller, D., Renaud, F.: Checking foundational proof certificates for first-order logic. In: Blanchette, J., Urban, J. (eds.) Proof Exchange for Theorem Proving. EasyChair, pp. 58–66 (2013)

[Cod+11]

Codescu, M., Horozal, F., Kohlhase, M., Mossakowski, T., Rabe, F.: Project Abstract: Logic Atlas and Integrator (LATIN). In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) CICM 2011. LNCS (LNAI), vol. 6824, pp. 289–291. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22673-1_24CrossRef

[Coq15]

Coq Development Team: The Coq proof assistant: reference manual. Technical report INRIA (2015)

[GD]

GLIF Demo. https://gl.kwarc.info/COMMA/glif-demo-ijcar-2020. Accessed 27 Jan 2020

[GEP]

Generated ELPI Provers. https://gl.mathhub.info/MMT/LATIN2/tree/devel/elpi. Accessed 26 Jan 2020

[HHP93]

Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. Assoc. Comput. Mach. 40(1), 143–184 (1993)MathSciNetCrossRef

[KK03]

Kohlhase, M., Koller, A.: Resource-adaptive model generation as a performance model. Log. J. IGPL 11(4), 435–456 (2003). http://jigpal.oxfordjournals.org/cgi/content/abstract/11/4/435

[Koh+20]

Kohlhase, M., et al.: Logic-independent proof search in logical frameworks (extended report). Extended Report of Conference Submission (2020). https://kwarc.info/kohlhase/submit/mmtelpi.pdf

[KS19]

Kohlhase, M., Schaefer, J.F.: GF + MMT = GLF - from language to semantics through LF. In: Miller, D., Scagnetto, I., (eds.) Proceedings of the Fourteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2019). Electronic Proceedings in Theoretical Computer Science (EPTCS), vol. 307, pp. 24–39 (2019). https://doi.org/10.4204/EPTCS.307.4

[LATIN]

LATIN2 - Logic Atlas Version 2. https://gl.mathhub.info/MMT/LATIN2. Accessed 02 June 2017

[Mil]

Miller, D: \(\lambda \)Prolog. http://www.lix.polytechnique.fr/Labo/ Dale. Miller/lProlog/

[Pau93]

Paulson, L.C.: Isabelle: The Next 700 Theorem Provers. In: arXiv CoRR cs.LO/9301106 (1993). https://arxiv.org/abs/cs/9301106

[Pau94]

Paulson, L.C. (ed.): Isabelle: A Generic Theorem Prover. LNCS, vol. 828. Springer, Heidelberg (1994). https://doi.org/10.1007/BFb0030541CrossRefMATH

[Rab17]

Rabe, F.: How to identify, translate, and combine logics? J. Log. Comput. 27(6), 1753–1798 (2017)MathSciNetCrossRef

[Rab18]

Rabe, F.: A modular type reconstruction algorithm. ACM Trans. Comput. Log. 19(4), 1–43 (2018)MathSciNetCrossRef

[Ran04]

Ranta, A.: Grammatical framework, a type-theoretical grammar formalism. J. Funct. Programm. 14(2), 145–189 (2004)MathSciNetCrossRef

[SCT15]

Coen, C.S., Tassi, E.: The ELPI system (2015). https://github.com/LPCIC/elpi

[TSK]

Tishkovsky, D., Schmidt, R.A., Khodadadi, M.: MetTeL2: towards a tableau prover generation platform. In: Proceedings of the Third Workshop on Practical As- pects of Automated Reasoning (PAAR-2012), p. 149 (2012)

Titel: Logic-Independent Proof Search in Logical Frameworks
verfasst von: Michael Kohlhase
Florian Rabe
Claudio Sacerdoti Coen
Jan Frederik Schaefer
Verlag: Springer International Publishing
Buch: Automated Reasoning
Print ISBN: 978-3-030-51073-2

Electronic ISBN: 978-3-030-51074-9

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-51074-9_22

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner