Resolution-based theorem proving for many-valued logics
From MaRDI portal
Cited in
(51)- On the refutational completeness of signed binary resolution and hyperresolution
- A resolution framework for finitely-valued first-order logics
- A categorical critical-pair completion algorithm
- TMPR: A tree-structured modified problem reduction proof procedure and its extension to three-valued logic
- Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers
- Proof search and co-NP completeness for many-valued logics
- Optimal axiomatizations of finitely valued logics
- On compatibilities of -lock resolution method in linguistic truth-valued lattice-valued logic
- Automated theorem proving by resolution in non-classical logics
- General form of \(\alpha\)-resolution principle for linguistic truth-valued lattice-valued logic
- Ideal resolution principle for lattice-valued first-order logic based on lattice implication algebra
- scientific article; zbMATH DE number 1696719 (Why is no real title available?)
- Towards a unified theorem of soundness and completeness for resolution in different 2-valued logics
- scientific article; zbMATH DE number 4164174 (Why is no real title available?)
- Resolution-Like Theorem Proving for High-Level Conditions
- Canonical Signed Calculi, Non-deterministic Matrices and Cut-Elimination
- CWA extensions to multi-valued logics
- scientific article; zbMATH DE number 3902617 (Why is no real title available?)
- scientific article; zbMATH DE number 3957059 (Why is no real title available?)
- scientific article; zbMATH DE number 19150 (Why is no real title available?)
- On the completeness theorem for many-valued lattices
- Canonical signed calculi with multi-ary quantifiers
- scientific article; zbMATH DE number 1292291 (Why is no real title available?)
- scientific article; zbMATH DE number 1301752 (Why is no real title available?)
- scientific article; zbMATH DE number 1324434 (Why is no real title available?)
- scientific article; zbMATH DE number 517011 (Why is no real title available?)
- scientific article; zbMATH DE number 559756 (Why is no real title available?)
- Short Conjunctive Normal Forms in Finitely Valued Logics
- scientific article; zbMATH DE number 1076963 (Why is no real title available?)
- scientific article; zbMATH DE number 1127072 (Why is no real title available?)
- Higher-Order Multi-Valued Resolution
- scientific article; zbMATH DE number 2042613 (Why is no real title available?)
- scientific article; zbMATH DE number 2072502 (Why is no real title available?)
- scientific article; zbMATH DE number 1507196 (Why is no real title available?)
- scientific article; zbMATH DE number 1775515 (Why is no real title available?)
- SAT and SMT technology for many-valued logics
- A resolution theorem prover for intuitionistic logic
- MUltlog 1.0: towards an expert system for many-valued logics
- Semantic trees revisited: some new completeness results
- Optimal axiomatizations for multiple-valued operators and quantifiers based on semi-lattices
- Exploiting data dependencies in many-valued logics
- scientific article; zbMATH DE number 1420874 (Why is no real title available?)
- Multi-valued extension of Putnam-Davis procedure
- scientific article; zbMATH DE number 7267153 (Why is no real title available?)
- scientific article; zbMATH DE number 4193644 (Why is no real title available?)
- An application of automated equational reasoning to many-valued logic
- CWA formalizations in multi-valued logics
- A first polynomial non-clausal class in many-valued logic
- Binary resolution over Boolean lattices
- Filter-based resolution principle for lattice-valued propositional logic LP(X)
- The Helly property and satisfiability of Boolean formulas defined on set families
This page was built for publication: Resolution-based theorem proving for many-valued logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1897558)
