Formalizing a Paraconsistent Logic in the Isabelle Proof Assistant

Jørgen Villadsen, Anders Schlichtkrull

Research output: Contribution to journalJournal articleResearchpeer-review

911 Downloads (Pure)


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.
Original languageEnglish
JournalTransactions on Large-Scale Data- and Knowledge-Centered Systems
Pages (from-to)92-122
Publication statusPublished - 2017


  • Paraconsistent logic
  • Many-valued logic
  • Formalization
  • Isabelle proof assistant
  • Inconsistency
  • Paraconsistency


Dive into the research topics of 'Formalizing a Paraconsistent Logic in the Isabelle Proof Assistant'. Together they form a unique fingerprint.

Cite this