Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics

DOI10.1016/J.TCS.2015.07.016zbMATH Open1331.03024arXiv1408.3775OpenAlexW2098322793WikidataQ61593294 ScholiaQ61593294MaRDI QIDQ744990FDOQ744990

Authors: Carlos Caleiro, João Marcos, Marco Volpe 

Publication date: 12 October 2015

Published in: Theoretical Computer Science (Search for Journal in Brave)

Abstract: The paper is a contribution both to the theoretical foundations and to the actual construction of efficient automatizable proof procedures for non-classical logics. We focus here on the case of finite-valued logics, and exhibit: (i) a mechanism for producing a classic-like description of them in terms of an effective variety of bivalent semantics; (ii) a mechanism for extracting, from the bivalent semantics so obtained, uniform (classically-labeled) cut-free standard analytic tableaux with possibly branching invertible rules and paired with proof strategies designed to guarantee termination of the associated proof procedure; (iii) a mechanism to also provide, for the same logics, uniform cut-based tableau systems with linear rules. The latter tableau systems are shown to be adequate even when restricted to analytic cuts, and they are also shown to polynomially simulate truth-tables, a feature that is not enjoyed by the former standard type of tableau systems (not even in the 2-valued case). The results are based on useful generalizations of the notions of analyticity and compositionality, and illustrate a theory that applies to many other classes of non-classical logics.

Full work available at URL: https://arxiv.org/abs/1408.3775

Recommendations

• Classic-Like Analytic Tableaux for Finite-Valued Logics
• Classic-like cut-based tableau systems for finite-valued logics
• scientific article; zbMATH DE number 512980
• scientific article; zbMATH DE number 63610
• Systematization of finite many-valued logics through the method of tableaux

zbMATH Keywords

bivalent semanticsproof complexitycompositionalitytableauxanalyticitytruth-functionality

Mathematics Subject Classification ID

Many-valued logic (03B50) Mechanization of proofs and logical operations (03B35)

Cites Work

• Truth and falsehood. An inquiry into generalized logical values
• Theory of logical calculi. Basic theory of consequence operations
• Title not available (Why is that?)
• Title not available (Why is that?)
• Algebraizable logics
• The Taming of the Cut. Classical Refutations with Analytic Cut
• A Machine-Oriented Logic Based on the Resolution Principle
• On notation for ordinal numbers
• A non-deterministic view on non-classical negations
• Resolution decision procedures
• Axiom schemes for m-valued propositions calculi
• A semantical analysis of the calculi \(C_n\)
• Classic-Like Analytic Tableaux for Finite-Valued Logics
• Title not available (Why is that?)
• Title not available (Why is that?)
• Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence
• Automated deduction for many-valued logics
• Tableau methods for classical propositional logic
• Don't eliminate cut
• Title not available (Why is that?)
• What is a non-truth-functional logic?
• Remarks on Łukasiewicz's three-valued logic
• Title not available (Why is that?)
• Cut-free ordinary sequent calculi for logics having generalized finite-valued semantics
• Effective finite-valued semantics for labelled calculi
• Classic-like cut-based tableau systems for finite-valued logics
• Title not available (Why is that?)
• Many-valuedness meets bivalence: using logical values in an effective way
• Title not available (Why is that?)
• Finitely many-valued logics and natural deduction

Cited In (15)

• An inferentially many-valued two-dimensional notion of entailment
• Proof search on bilateralist judgments over non-deterministic semantics
• Non-distributive relatives of ETL and NFL
• Classic-Like Analytic Tableaux for Finite-Valued Logics
• Two-sided sequent calculi for \textit{FDE}-like four-valued logics
• An informational view of classical logic
• Rasiowa-Sikorski deduction systems with the rule of cut: a case study
• A note on two's company: ``The humbug of many logical values
• Compositional meaning in logic
• Classic-like cut-based tableau systems for finite-valued logics
• Axiomatizing non-deterministic many-valued generalized consequence relations
• Monadicity of non-deterministic logical matrices is undecidable
• On Axioms and Rexpansions
• SUSZKO’S PROBLEM: MIXED CONSEQUENCE AND COMPOSITIONALITY
• Translating non-classical logics into classical logic by using hidden variables

This page was built for publication: Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q744990)