Short Conjunctive Normal Forms in Finitely Valued Logics
From MaRDI portal
Publication:4323008
DOI10.1093/logcom/4.6.905zbMath0818.03003MaRDI 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 logic; resolution theorem proving; satisfiability preserving CNF reduction of formulas in finite-valued calculi
03B35: Mechanization of proofs and logical operations
03B50: Many-valued logic
03G20: Logical aspects of ?ukasiewicz and Post algebras
Related Items
A first polynomial non-clausal class in many-valued logic, Binary resolution over complete residuated Stone lattices, Binary resolution over Boolean lattices, On the refutational completeness of signed binary resolution and hyperresolution, Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers, Optimal axiomatizations of finitely valued logics, New complexity results for Łukasiewicz logic, Hyperresolution for Gödel logic with truth constants, Automated theorem proving by resolution in non-classical logics, Regular-SAT: A many-valued approach to solving combinatorial problems, A Generalisation of the Hyperresolution Principle to First Order Gödel Logic
Uses Software
