| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 391408 | Fuzzy Sets and Systems | 2006 | 28 Pages |
Abstract
We propose a binary resolution system over Boolean lattices. We shall assume that truth values form a complete Boolean lattice L where its supremum operator is infinitely distributive over the infimum one. Binary L-resolution will operate on graded clauses. A graded clause is a pair of the form (l1∨⋯∨ln,c) where li are literals and c is a truth degree in L. The refutational soundness and completeness of the proposed resolution proof method will be proved.
Related Topics
Physical Sciences and Engineering
Computer Science
Artificial Intelligence
