Binary resolution over Boolean lattices

DOI10.1016/J.FSS.2006.02.010MaRDI QIDQ853473zbMATH OpenOpenAlexFDO

Authors Dušan Guller

Publication date 15 November 2006

Published in Fuzzy Sets and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.fss.2006.02.010

zbMATH Keywords

automated deductionknowledge representationmany-valued logicsresolution proof systems

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Many-valued logic (03B50) Knowledge representation (68T30)

Review text

The author presents a binary resolution system over complete Boolean lattices with the condition that their supremum operators are infinitely distributive over the infimum ones. He utilizes inference techniques developed in classical two-valued logic for many-valued ones. He considers many-valued logics \({\mathbf L}\) whose truth values form a Boolean algebra. He avoids any limitation to the finite case where the set of truth values or a given set of clauses are finite. The refutational soundness and completeness of binary \({\mathbf L}\)-resolution is proved.

Recommendations

• Binary resolution over complete residuated Stone lattices
• On the refutational completeness of signed binary resolution and hyperresolution
• scientific article; zbMATH DE number 1324434
• \(\alpha\)-resolution principle based on lattice-valued propositional logic \(\text{LP} (X)\)
• Graded many-valued resolution with aggregation.

Cites work

• A framework for automated reasoning in multiple-valued logics
• A lattice-theoretical fixpoint theorem and its applications
• A logic for reasoning with inconsistency
• Commodious axiomatization of quantifiers in multiple-valued logic
• Fuzzy logic and approximate reasoning
• scientific article; zbMATH DE number 2089453 (Why is no real title available?)
• scientific article; zbMATH DE number 420884 (Why is no real title available?)
• scientific article; zbMATH DE number 3987347 (Why is no real title available?)
• scientific article; zbMATH DE number 48957 (Why is no real title available?)
• scientific article; zbMATH DE number 53302 (Why is no real title available?)
• scientific article; zbMATH DE number 4128792 (Why is no real title available?)
• scientific article; zbMATH DE number 695097 (Why is no real title available?)
• scientific article; zbMATH DE number 1076962 (Why is no real title available?)
• scientific article; zbMATH DE number 2042611 (Why is no real title available?)
• scientific article; zbMATH DE number 1775515 (Why is no real title available?)
• scientific article; zbMATH DE number 1852927 (Why is no real title available?)
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• Innovations in intelligent systems.
• Metamathematics of fuzzy logic
• On Fuzzy Logic I Many‐valued rules of inference
• Optimal axiomatizations for multiple-valued operators and quantifiers based on semi-lattices
• Optimal axiomatizations of finitely valued logics
• Paraconsistent logic programming
• Resolution theorem proving
• Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators
• Resolution-based theorem proving for many-valued logics
• Short Conjunctive Normal Forms in Finitely Valued Logics
• The SAT problem of signed CNF formulas

Cited in

(4)

• On the refutational completeness of signed binary resolution and hyperresolution
• Sparse Boolean equations and circuit lattices
• Determination of \(\alpha \)-resolution in lattice-valued first-order logic \(\mathrm{LF}(X)\)
• Binary resolution over complete residuated Stone lattices

This page was built for publication: Binary resolution over Boolean lattices

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q853473)