Short Conjunctive Normal Forms in Finitely Valued Logics
From MaRDI portal
Publication:4323008
DOI10.1093/logcom/4.6.905zbMath0818.03003OpenAlexW1978050007MaRDI QIDQ4323008
Publication date: 10 August 1995
Published in: Journal of Logic and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1093/logcom/4.6.905
many-valued logicŁukasiewicz logicresolution theorem provingsatisfiability preserving CNF reduction of formulas in finite-valued calculi
Mechanization of proofs and logical operations (03B35) Many-valued logic (03B50) Logical aspects of ?ukasiewicz and Post algebras (03G20)
Related Items
Binary resolution over complete residuated Stone lattices, Automated theorem proving by resolution in non-classical logics, Binary resolution over Boolean lattices, Regular-SAT: A many-valued approach to solving combinatorial problems, MaxSAT resolution for regular propositional logic, A first polynomial non-clausal class in many-valued logic, Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers, A Generalisation of the Hyperresolution Principle to First Order Gödel Logic, New complexity results for Łukasiewicz logic, On the refutational completeness of signed binary resolution and hyperresolution, Hyperresolution for Gödel logic with truth constants, Optimal axiomatizations of finitely valued logics
Uses Software
