Journal article · Book chapter
Formalizing a Paraconsistent Logic in the Isabelle Proof Assistant
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.
Language: | English |
---|---|
Publisher: | Springer Berlin Heidelberg |
Year: | 2017 |
Pages: | 92-122 |
Series: | Lecture Notes in Computer Science |
Journal subtitle: | Special Issue on Consistency and Inconsistency in Data-centric Applications |
ISBN: | 3662559463 , 3662559471 , 9783662559468 and 9783662559475 |
ISSN: | 25104942 , 18691994 , 16113349 and 03029743 |
Types: | Journal article and Book chapter |
DOI: | 10.1007/978-3-662-55947-5_5 |
ORCIDs: | Villadsen, Jørgen and Schlichtkrull, Anders |