Abstract | ||
---|---|---|
Key issues for resolution-based automated reasoning in lattice-valued first-order logic LF(X) are investigated with truth-values in a lattice-valued logical algebraic structure-lattice implication algebra (LIA). The determination of resolution at a certain truth-value level (called @a-resolution) in LF(X) is proved to be equivalently transformed into the determination of @a-resolution in lattice-valued propositional logic LP(X) based on LIA. The determination of @a-resolution of any quasi-regular generalized literals and constants under various cases in LP(X) is further analyzed, specified, and subsequently verified. Hence the determination of @a-resolution in LF(X) can be accordingly solved to a very broad extent, which not only lays a foundation for the practical implementation of automated reasoning algorithms in LF(X), but also provides a key support for @a-resolution-based automated reasoning approaches and algorithms in LIA based linguistic truth-valued logics. |
Year | DOI | Venue |
---|---|---|
2011 | 10.1016/j.ins.2010.03.024 | Inf. Sci. |
Keywords | Field | DocType |
linguistic truth-valued logic,resolution-based automated reasoning,lattice-valued first-order logic,lattice-valued propositional logic,key support,automated reasoning algorithm,a-resolution-based automated reasoning approach,broad extent,lattice-valued logical algebraic structure-lattice,key issue,many valued logic,automated reasoning,first order logic,propositional logic | Automated reasoning,Discrete mathematics,Algebraic number,Lattice (order),Inference,Fuzzy logic,Propositional calculus,First-order logic,Many-valued logic,Mathematics | Journal |
Volume | Issue | ISSN |
181 | 10 | 0020-0255 |
Citations | PageRank | References |
21 | 1.04 | 43 |
Authors | ||
4 |
Name | Order | Citations | PageRank |
---|---|---|---|
Yang Xu | 1 | 711 | 83.57 |
Jun Liu | 2 | 419 | 23.08 |
Da Ruan | 3 | 2008 | 112.05 |
Xiaobing Li | 4 | 47 | 2.76 |