Semantic Scholar Open Access 2017 4 sitasi

Formalizing a Paraconsistent Logic in the Isabelle Proof Assistant

J. Villadsen Anders Schlichtkrull

Abstrak

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.

Topik & Kata Kunci

Mathematics Computer Science

Penulis (2)

J. Villadsen

Anders Schlichtkrull

Format Sitasi

APA MLA BibTeX

Villadsen, J., Schlichtkrull, A. (2017). Formalizing a Paraconsistent Logic in the Isabelle Proof Assistant. https://doi.org/10.1007/978-3-662-55947-5_5

Akses Cepat

PDF tidak tersedia langsung

Cek di sumber asli →

Lihat di Sumber doi.org/10.1007/978-3-662-55947-5_5

Informasi Jurnal

Tahun Terbit: 2017
Bahasa: en
Total Sitasi: 4×
Sumber Database: Semantic Scholar
DOI: 10.1007/978-3-662-55947-5_5
Akses: Open Access ✓