nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Formalizing a Paraconsistent Logic in the Isabelle Proof Assistant

verfasst von : Jørgen Villadsen, Anders Schlichtkrull

Erschienen in: Transactions on Large-Scale Data- and Knowledge-Centered Systems XXXIV

Verlag: Springer Berlin Heidelberg

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

We present a formalization of a so-called paraconsistent logic that avoids the catastrophic explosiveness of inconsistency in classical logic. The paraconsistent logic has a countably infinite number of non-classical truth values. We show how to use the proof assistant Isabelle to formally prove theorems in the logic as well as meta-theorems about the logic. In particular, we formalize a meta-theorem that allows us to reduce the infinite number of truth values to a finite number of truth values, for a given formula, and we use this result in a formalization of a small case study.

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 A Second Generation of Peer-to-Peer Semantic Wikis

Nächstes Kapitel A Proximity-Based Understanding of Conditionals

Akama, S. (ed.): Towards Paraconsistent Engineering. Intelligent Systems Reference Library, vol. 110. Springer, Cham (2016). doi:10.1007/978-3-319-40418-9 MATH

Batens, D., Mortensen, C., Priest, G., Van-Bendegem, J. (eds.): Frontiers in Paraconsistent Logic. Research Studies Press, Philadelphia (2000)

Berghofer, S.: First-Order Logic According to Fitting. Archive of Formal Proofs (2007). http://isa-afp.org/entries/FOL-Fitting.shtml

Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development – Coq’Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science. Springer, Heidelberg (2004). doi:10.1007/978-3-662-07964-5 CrossRefMATH

Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109–128 (2013)MathSciNetCrossRefMATH

Blanchette, J.C., Popescu, A., Traytel, D.: Soundness and completeness proofs by coinductive methods. J. Autom. Reason. 58(1), 149–179 (2017)MathSciNetCrossRefMATH

Breitner, J., Lohner, D.: The Meta Theory of the Incredible Proof Machine. Archive of Formal Proofs (2016). http://isa-afp.org/entries/Incredible_Proof_Machine.shtml

Brucker, A.D., Tuong, F., Wolff, B.: Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5. Archive of Formal Proofs (2014). http://isa-afp.org/entries/Featherweight_OCL.shtml

Carnielli, W.A., Coniglio, M.E., D’Ottaviano, I.M.L. (eds.): Paraconsistency: The Logical Way to the Inconsistent. Marcel Dekker, New York (2002)

10.

Ciungu, L.C.: Non-commutative Multiple-Valued Logic Algebras. Springer Monographs in Mathematics. Springer, Cham (2014). doi:10.1007/978-3-319-01589-7 CrossRefMATH

11.

Decker, H., Villadsen, J., Waragai, T. (eds.) International Workshop on Paraconsistent Computational Logic, vol. 95. Roskilde University, Computer Science, Technical reports (2002)

12.

From, A.H.: Formalized First-Order Logic. B.Sc. thesis, Technical University of Denmark (2017)

13.

Georgescu, G., Leustean, L., Preoteasa, V.: Pseudo Hoops. Archive of Formal Proofs (2011). http://isa-afp.org/entries/PseudoHoops.shtml

14.

Geuvers, H.: Proof assistants: history, ideas and future. Sadhana 34(1), 3–25 (2009). SpringerMathSciNetCrossRefMATH

15.

Gödel, K.: On formally undecidable propositions of principia mathematica and related systems. In: van Heijenoort, J. (ed.) From Frege to Gödel. Harvard University Press (1967)

16.

Gottwald, S.: A Treatise on Many-Valued Logics. Research Studies Press, Baldock (2001)MATH

17.

Hansson, S.O.: Logic of belief revision. In: Zalta, E.N. et al. (eds.) Stanford Encyclopedia of Philosophy (2016). http://plato.stanford.edu/entries/logic-belief-revision/. Winter Edition

18.

Huffman, B.: Reasoning with Powerdomains in Isabelle/HOLCF. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. Emerging Trends Proceedings, pp. 45–56. Technical report, Concordia University (2008)

19.

Jensen, A.B., Schlichtkrull, A., Villadsen, J.: First-Order Logic According to Harrison. Archive of Formal Proofs (2017). http://isa-afp.org/entries/FOL_Harrison.shtml

20.

Jensen, A.S., Villadsen, J.: Paraconsistent computational logic. In: Blackburn, P., Jørgensen, K.F., Jones, N., Palmgren, E. (eds.) 8th Scandinavian Logic Symposium: Abstracts, pp. 59–61. Roskilde University (2012)

21.

Krauss, A.: Defining Recursive Functions in Isabelle/HOL. Isabelle Distribution (2017). http://isabelle.in.tum.de/doc/functions.pdf

22.

Lamport, L.: How to write a proof. Am. Math. Mon. 102(7), 600–608 (1995)MathSciNetCrossRefMATH

23.

Lamport, L.: How to write a 21st century proof. J. Fixed Point Theor. Appl. 11(1), 43–63 (2012)MathSciNetCrossRefMATH

24.

Marcos, J.: Automatic generation of proof tactics for finite-valued logics. In: Proceedings of Tenth International Workshop on Rule-Based Programming, pp. 91–98 (2009)

25.

Michaelis, J., Nipkow, T.: Propositional Proof Systems. Archive of Formal Proofs (2017). http://isa-afp.org/entries/Propositional_Proof_Systems.shtml

26.

Milner, R.: Logic for computable functions: description of a machine implementation. Stanford University (1972)

27.

Müller, O., Nipkow, T., Oheimb, D., Slotosch, O.: HOLCF = HOL + LCF. J. Funct. Program. 9(2), 191–223 (1999)MathSciNetCrossRefMATH

28.

Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). doi:10.1007/3-540-45949-9

29.

Nipkow, T., Klein, G.: Concrete Semantics — With Isabelle/HOL. Springer, Cham (2014). doi:10.1007/978-3-319-10542-0 MATH

30.

Paulson, L.C.: A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets. Rev. Symb. Log. 7(3), 484–498 (2014)MathSciNetCrossRefMATH

31.

Priest, G., Routley, R., Norman, J. (eds.): Paraconsistent Logic: Essays on the Inconsistent. Philosophia Verlag, Munich (1989)MATH

32.

Priest, G., Tanaka, K., Weber, Z.: Paraconsistent logic. In: Zalta, E.N. et al. (eds.) Stanford Encyclopedia of Philosophy (2016). http://plato.stanford.edu/entries/logic-paraconsistent. Winter Edition

33.

Regensburger, F.: HOLCF: higher order logic of computable functions. In: Schubert, E.T., Windley, P.J., Alves-Foss, J. (eds.) TPHOLs 1995. LNCS, vol. 971, pp. 293–307. Springer, Heidelberg (1995). doi:10.1007/3-540-60275-5_72

34.

Regensburger, F.: The type of lifted booleans. Isabelle Distribution (2017). http://isabelle.in.tum.de/library/HOL/HOLCF/Tr.html

35.

Ridge, T.: A Mechanically Verified, Efficient, Sound and Complete Theorem Prover for First Order Logic. Archive of Formal Proofs (2004). http://isa-afp.org/entries/Verified-Prover.shtml

36.

Schlichtkrull, A.: The Resolution Calculus for First-Order Logic. Archive of Formal Proofs (2016). http://isa-afp.org/entries/Resolution_FOL.shtml

37.

Schlichtkrull, A., Villadsen, J.: Paraconsistency. Archive of Formal Proofs (2017). http://isa-afp.org/entries/Paraconsistency.shtml

38.

Scott, D.S.: A type-theoretical alternative to ISWIM, CUCH, OWHY. Theor. Comput. Sci. 121, 411–440 (1993). Annotated version of an unpublished manuscript from 1969MathSciNetCrossRefMATH

39.

Steen, A., Benzmüller, C.: Sweet SIXTEEN: automation via embedding into classical higher-order logic. Log. Log. Philos. 25(4), 535–554 (2016)MathSciNetMATH

40.

Villadsen, J.: Combinators for paraconsistent attitudes. In: de Groote, P., Morrill, G., Retoré, C. (eds.) LACL 2001. LNCS, vol. 2099, pp. 261–278. Springer, Heidelberg (2001). doi:10.1007/3-540-48199-0_16 CrossRef

41.

Villadsen, J.: Paraconsistent assertions. In: Lindemann, G., Denzinger, J., Timm, I.J., Unland, R. (eds.) MATES 2004. LNCS, vol. 3187, pp. 99–113. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30082-3_8 CrossRef

42.

Villadsen, J.: A paraconsistent higher order logic. In: Buchberger, B., Campbell, J.A. (eds.) AISC 2004. LNCS, vol. 3249, pp. 38–51. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30210-0_5

43.

Villadsen, J.: Supra-logic: using transfinite type theory with type variables for paraconsistency. J. Appl. Non Class. Log. 15(1), 45–58 (2005). Logical approaches to paraconsistencyMathSciNetCrossRefMATH

44.

Villadsen, J., Jensen, A.B., Schlichtkrull, A.: NaDeA: a natural deduction assistant with a formalization in Isabelle. IFCoLog J. Log. Appl. 4(1), 55–82 (2017)

45.

Villadsen, J., Schlichtkrull, A.: Formalization of many-valued logics. In: Christiansen, H., Jiménez-López, M.D., Loukanova, R., Moss, L.S. (eds.) Partiality and Underspecification in Information, Languages, and Knowledge, Chap. 7. Cambridge Scholars Publishing (2017)

46.

Weber, Z.: Paraconsistent Logic. The Internet Encyclopedia of Philosophy (2017). http://www.iep.utm.edu/para-log

47.

Wenzel, M.: Isar — a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Théry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 167–183. Springer, Heidelberg (1999). doi:10.1007/3-540-48256-3_12 CrossRef

48.

Wiedijk, F. (ed.): The Seventeen Provers of the World. LNCS (LNAI), vol. 3600. Springer, Heidelberg (2006)

Titel: Formalizing a Paraconsistent Logic in the Isabelle Proof Assistant
verfasst von: Jørgen Villadsen
Anders Schlichtkrull
Verlag: Springer Berlin Heidelberg
Buch: Transactions on Large-Scale Data- and Knowledge-Centered Systems XXXIV
Print ISBN: 978-3-662-55946-8

Electronic ISBN: 978-3-662-55947-5

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-662-55947-5_5

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"