Exploiting data dependencies in many-valued logics

DOI10.1080/11663081.1996.10510866zbMath0836.03013OpenAlexW2035493071MaRDI QIDQ4868234

Reiner Hähnle

Publication date: 6 March 1996

Published in: Journal of Applied Non-Classical Logics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1080/11663081.1996.10510866

zbMATH Keywords

resolutionpolaritymany-valued logicsautomated theorem provingHorn formulasDavis-Putnam proceduredirect products of structuresmany-valued first-order clauses

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Many-valued logic (03B50)

Related Items

Systems of ordinal fuzzy logic with application to preference modelling, Automated theorem proving by resolution in non-classical logics, Regular-SAT: A many-valued approach to solving combinatorial problems, A first polynomial non-clausal class in many-valued logic, Resolution and model building in the infinite-valued calculus of Łukasiewicz, On the refutational completeness of signed binary resolution and hyperresolution

Cites Work

• Unnamed Item
• Why Horn formulas matter in computer science: initial structures and generic examples
• Completely non-clausal theorem proving
• Solving propositional satisfiability problems
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Algorithms for testing the satisfiability of propositional formulae
• A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
• A machine program for theorem-proving