nach oben

Erschienen in:

2021 | OriginalPaper | Buchkapitel

Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL

verfasst von : Asta Halkjær From, Agnes Moesgård Eschen, Jørgen Villadsen

Erschienen in: Intelligent Computer Mathematics

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

We formalize soundness and completeness proofs for a number of axiomatic systems for propositional logic in the proof assistant Isabelle/HOL.

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 Beautiful Formalizations in Isabelle/Naproche

Nächstes Kapitel Formalization of RBD-Based Cause Consequence Analysis in HOL

Blanchette, J.C.: Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). In: Mahboubi, A., Myreen, M.O. (eds.) Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, 14–15 January 2019, Cascais, Portugal, pp. 1–13. ACM (2019)

Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109–128 (2013). https://doi.org/10.1007/s10817-013-9278-5MathSciNetCrossRefMATH

Church, A.: Introduction to Mathematical Logic. Princeton University Press, Princeton (1956)MATH

Fitelson, B., Wos, L.: Finding missing proofs with automated reasoning. Studia Logica 68(3), 329–356 (2001). https://doi.org/10.1023/A:1012486904520MathSciNetCrossRefMATH

From, A.H.: Formalizing Henkin-style completeness of an axiomatic system for propositional logic. In: Proceedings of the Web Summer School in Logic, Language and Information (WeSSLLII) and the European Summer School in Logic, Language and Information (ESSLLI) Virtual Student Session (2020), pp. 1–12, preliminary paper. https://www.brandeis.edu/nasslli2020/pdfs/student-session-proceedings-compressed.pdf#page=8. Accepted for Springer post-proceedings

From, A.H., Villadsen, J., Blackburn, P.: Isabelle/HOL as a meta-language for teaching logic. In: Quaresma, P., Neuper, W., Marcos, J. (eds.) Proceedings 9th International Workshop on Theorem Proving Components for Educational Software, ThEdu@IJCAR 2020, 29th June 2020, Paris, France. EPTCS, vol. 328, pp. 18–34 (2020). https://doi.org/10.4204/EPTCS.328.2

From, A.H.: Epistemic logic: completeness of modal logics. Archive of Formal Proofs, October 2018. https://devel.isa-afp.org/entries/Epistemic_Logic.html, Formal proof development

From, A.H.: Formalizing a Seligman-style tableau system for hybrid logic. Archive of Formal Proofs, December 2019. https://isa-afp.org/entries/Hybrid_Logic.html, Formal proof development

Michaelis, J., Nipkow, T.: Formalized proof systems for propositional logic. In: Abel, A., Forsberg, F.N., Kaposi, A. (eds.) 23rd International Conference on Types for Proofs and Programs, TYPES 2017, 29 May–1 June 2017, Budapest, Hungary. LIPIcs, vol. 104, pp. 5:1–5:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

10.

Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9

11.

Schlichtkrull, A., Blanchette, J., Traytel, D., Waldmann, U.: Formalizing Bachmair and Ganzinger’s ordered resolution prover. J. Autom. Reason. 64(7), 1169–1195 (2020)MathSciNetCrossRef

12.

Łukasiewicz, J.: The shortest axiom of the implicational calculus of propositions. Proc. Royal Irish Acad. Sect. A: Math. Phys. Sci. 52, 25–33 (1948)

13.

Wos, L., Pieper, G.W.: Automated Reasoning and the Discovery of Missing and Elegant Proofs. Rinton Press, Princeton (2003)

Titel: Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL
verfasst von: Asta Halkjær From
Agnes Moesgård Eschen
Jørgen Villadsen
Verlag: Springer International Publishing
Buch: Intelligent Computer Mathematics
Print ISBN: 978-3-030-81096-2

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

Copyright-Jahr: 2021
DOI: https://doi.org/10.1007/978-3-030-81097-9_3

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