New Formalized Results on the Meta-Theory of a Paraconsistent Logic

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

18 Downloads (Pure)

Abstract

Classical logics are explosive, meaning that everything follows from a contradiction. Paraconsistent logics are logics that are not explosive. This paper presents the meta-theory of a paraconsistent infinite-valued logic, in particular new results showing that while the question of validity for a given formula can be reduced to a consideration of only finitely many truth values, this does not mean that the logic collapses to a finite-valued logic. All definitions and theorems are formalized in the Isabelle/HOL proof assistant.
Original languageEnglish
Title of host publication24th International Conference on Types for Proofs and Programs
EditorsPeter Dybjer, José Espírito Santo, Luís Pinto
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Publication date2019
Pages5:1–5:15
Article number5
ISBN (Print)978-3-95977-106-1
Publication statusPublished - 2019
Event24th International Conference on Types for Proofs and Programs - University of Minho, Braga, Portugal
Duration: 18 Jun 201821 Jun 2018
https://types2018.projj.eu/

Conference

Conference24th International Conference on Types for Proofs and Programs
LocationUniversity of Minho
CountryPortugal
CityBraga
Period18/06/201821/06/2018
Internet address
SeriesLeibniz International Proceedings in Informatics
ISSN1868-8969

Keywords

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

Fingerprint Dive into the research topics of 'New Formalized Results on the Meta-Theory of a Paraconsistent Logic'. Together they form a unique fingerprint.

Cite this