On the refutational completeness of signed binary resolution and hyperresolution
From MaRDI portal
Publication:1037933
DOI10.1016/j.fss.2008.05.011zbMath1191.03009OpenAlexW2021448969MaRDI QIDQ1037933
Publication date: 17 November 2009
Published in: Fuzzy Sets and Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.fss.2008.05.011
Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07) Many-valued logic (03B50)
Related Items (2)
Unsatisfiable Formulae of Gödel Logic with Truth Constants and $$\varDelta $$ Are Recursively Enumerable ⋮ Hyperresolution for Gödel logic with truth constants
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Binary resolution over complete residuated Stone lattices
- Binary resolution over Boolean lattices
- Satisfiability in many-valued sentential logic is NP-complete
- A framework for automated reasoning in multiple-valued logics
- Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators
- Resolution-based theorem proving for many-valued logics
- Many-valued logic and mixed integer programming
- Finiteness in infinite-valued Łukasiewicz logic
- Automated theorem proving by resolution in non-classical logics
- The state of SAT
- Herbrand’s Theorem for Prenex Gödel Logic and Its Consequences for Theorem Proving
- Ordered chaining calculi for first-order theories of transitive relations
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Short Conjunctive Normal Forms in Finitely Valued Logics
- Exploiting data dependencies in many-valued logics
- A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
This page was built for publication: On the refutational completeness of signed binary resolution and hyperresolution
