Resolution-based theorem proving for many-valued logics

DOI10.1006/jsco.1995.1021zbMath0839.68091OpenAlexW2076410236MaRDI QIDQ1897558

Matthias Baaz, Christian G. Fermüller

Publication date: 9 October 1995

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/90ed51a3e9520af42dad56317bdc5949f6e9ab34

zbMATH Keywords

automated theorem proving

Mathematics Subject Classification ID

Related Items (19)

Automated theorem proving by resolution in non-classical logics ⋮ Binary resolution over Boolean lattices ⋮ General form of \(\alpha\)-resolution principle for linguistic truth-valued lattice-valued logic ⋮ Filter-based resolution principle for lattice-valued propositional logic LP\((X)\) ⋮ On compatibilities of \(\alpha \)-lock resolution method in linguistic truth-valued lattice-valued logic ⋮ A first polynomial non-clausal class in many-valued logic ⋮ Canonical signed calculi with multi-ary quantifiers ⋮ Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers ⋮ Ideal resolution principle for lattice-valued first-order logic based on lattice implication algebra ⋮ 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 ⋮ The Helly property and satisfiability of Boolean formulas defined on set families ⋮ CWA formalizations in multi-valued logics ⋮ Canonical Signed Calculi, Non-deterministic Matrices and Cut-Elimination ⋮ CWA Extensions to Multi-Valued Logics ⋮ On the refutational completeness of signed binary resolution and hyperresolution ⋮ A categorical critical-pair completion algorithm ⋮ Optimal axiomatizations of finitely valued logics

This page was built for publication: Resolution-based theorem proving for many-valued logics