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.
Original language | English |
---|---|
Journal | Transactions on Large-Scale Data- and Knowledge-Centered Systems |
Volume | 34 |
Pages (from-to) | 92-122 |
ISSN | 1869-1994 |
DOIs | |
Publication status | Published - 2017 |
Keywords
- Paraconsistent logic
- Many-valued logic
- Formalization
- Isabelle proof assistant
- Inconsistency
- Paraconsistency