Automated deduction for many-valued logics
This Handbook chapter a reader may use as a comprehensive guide to the contemporary many-valued automated reasoning techniques based on the method of signed formulas. The authors have proved themselves to be good specialists in this field. They give an exposition of the resolution method for first-order finite-valued logics. They consider proof systems with signed formulas, i.e., expressions of many-valued logics that have sets of truth values attached to their heads. Such formulas have two-valued interpretation. The authors describe two kinds of transformations that should be applied to many-valued formulas in order to use them in resolution procedures. These two transformations are language-preserving (CNF) and structure-preserving transformations. Also the resolution inference system is constructed, and refutational and implicational completeness are proved for this system. Transformation and resolution rules are tested with a cute 2-world Kripke model example. There are some hints how one can generalize results concerning the 2-world model to the case of the \(n\)-world model which corresponds to \(2^n\)-valued logic.NEWLINENEWLINEFor the entire collection see [Zbl 0964.00020].
- scientific article; zbMATH DE number 559756
- A framework for automated reasoning in multiple-valued logics
- scientific article; zbMATH DE number 1209602
- An application of automated equational reasoning to many-valued logic
- scientific article; zbMATH DE number 1127072
- Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers
- scientific article; zbMATH DE number 1076962
- scientific article; zbMATH DE number 3875236
- scientific article; zbMATH DE number 1678379
- scientific article; zbMATH DE number 2177634
- On the refutational completeness of signed binary resolution and hyperresolution
- A framework for automated reasoning in multiple-valued logics
- Automated deduction with associative-commutative operators
- Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers
- Proof search and co-NP completeness for many-valued logics
- Non-distributive relatives of ETL and NFL
- Analytic tableaux for non-deterministic semantics
- From bi-facial truth to bi-facial proofs
- Automated theorem proving by resolution in non-classical logics
- Complexity of clausal constraints over chains
- Higher-level inferences in the strong-Kleene setting: a proof-theoretic approach
- Partial and paraconsistent three-valued logics
- scientific article; zbMATH DE number 5074301 (Why is no real title available?)
- Fibrational Semantics for Many-Valued Logic Programs: Grounds for Non-Groundness
- Classic-Like Analytic Tableaux for Finite-Valued Logics
- Proof theory for locally finite many-valued logics: semi-projective logics
- Automated proof-searching for strong Kleene logic and its binary extensions via correspondence analysis
- Determination of \(\alpha \)-resolution in lattice-valued first-order logic \(\mathrm{LF}(X)\)
- A first polynomial non-clausal class in many-valued logic
- Axiomatizing non-deterministic many-valued generalized consequence relations
- Bisequent calculus for four-valued quasi-relevant logics: cut elimination and interpolation
- Analytic calculi for logics of indicative conditionals
- Graded relation updates in modal logic
- and in eight-valued non-deterministic semantics for modal logics
- Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics
This page was built for publication: Automated deduction for many-valued logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2751372)
