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

DOI10.1016/J.TCS.2015.07.016MaRDI QIDQ744990zbMATH OpenOpenAlexWikidataFDO

Authors Carlos Caleiro, João Marcos, Marco Volpe

Publication date 12 October 2015

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

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

zbMATH Keywords

bivalent semanticsproof complexitycompositionalitytableauxanalyticitytruth-functionality

Mathematics Subject Classification ID

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

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.

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

Cites work

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

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
• Translating non-classical logics into classical logic by using hidden variables
• SUSZKO’S PROBLEM: MIXED CONSEQUENCE AND COMPOSITIONALITY

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)