Skip to main content
SpringerLink
Log in

Formalizing a Paraconsistent Logic in the Isabelle Proof Assistant

  • Chapter
  • First Online:
Transactions on Large-Scale Data- and Knowledge-Centered Systems XXXIV

Part of the book series: Lecture Notes in Computer Science ((TLDKS,volume 10620))

  • 374 Accesses

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 16.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

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

    MATH  Google Scholar 

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

    Google Scholar 

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

  4. 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

    Book  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  7. 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

  8. 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

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

    Google Scholar 

  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

    Book  MATH  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  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). Springer

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

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

    MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  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  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

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

    MATH  Google Scholar 

  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 1969

    Article  MathSciNet  MATH  Google Scholar 

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

    MathSciNet  MATH  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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 paraconsistency

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

  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)

    Google Scholar 

  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

    Chapter  Google Scholar 

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

    Google Scholar 

Download references

Acknowledgements

Thanks to Andreas Halkjær From, Alexander Birch Jensen and John Bruntse Larsen for comments on drafts of the paper. Also thanks to Hendrik Decker and the anonymous reviewers for many constructive comments.

Author information

Authors and Affiliations

  1. DTU Compute, Technical University of Denmark, 2800, Kongens Lyngby, Denmark

    Jørgen Villadsen & Anders Schlichtkrull

Authors
  1. Jørgen Villadsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Anders Schlichtkrull
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jørgen Villadsen .

Editor information

Editors and Affiliations

  1. IRIT, Paul Sabatier University, Toulouse, France

    Abdelkader Hameurlain

  2. FAW, University of Linz, Linz, Austria

    Josef Küng

  3. FAW, University of Linz, Linz, Austria

    Roland Wagner

  4. Polytechnic University of Valencia, Valencia, Spain

    Hendrik Decker

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer-Verlag GmbH Germany

About this chapter

Cite this chapter

Villadsen, J., Schlichtkrull, A. (2017). Formalizing a Paraconsistent Logic in the Isabelle Proof Assistant. In: Hameurlain, A., Küng, J., Wagner, R., Decker, H. (eds) Transactions on Large-Scale Data- and Knowledge-Centered Systems XXXIV. Lecture Notes in Computer Science(), vol 10620. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-55947-5_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-55947-5_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-55946-8

  • Online ISBN: 978-3-662-55947-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation