Name
Title | ||
|---|---|---|
Non-clausal Multi-ary alpha-Generalized Resolution Principle for a Lattice-Valued First-Order Logic |
Abstract | ||
|---|---|---|
The present paper focuses on a resolution-based automated reasoning theory in a lattice-valued logic system with truth-values defined in a lattice-valued algebraic structure - lattice implication algebras (LIA) in order to handle automated deduction under an uncertain environment. Particularly, as a continuation and extension of the established work on binary resolution at a certain truth-value level a (called a-resolution), a non-clausal multi-ary a-generalized resolution principle and deduction are introduced in this paper for a lattice-valued first-order logic LF(X) based on LIA, which is essentially non-clausal generalized resolution avoiding the reduction to normal clausal form. Non-clausal multi-ary a-generalized resolution deduction in LF(X) is then proved to be sound and complete. The present work is expected to provide a theoretical foundation of more efficient resolution based automated reasoning in lattice-valued logic. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1109/ISKE.2015.88 | 2015 10th International Conference on Intelligent Systems and Knowledge Engineering (ISKE) |
Keywords | DocType | ISSN |
Automated reasoning,Resolution principle,Latticevalued logic,Lattice implication algebra,Non-clausal multi-ary - generalized resolution | Conference | 2164-2508 |
Citations | PageRank | References |
0 | 0.34 | 14 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yang Xu | 1 | 711 | 83.57 |
| Jun Liu | 2 | 644 | 56.21 |
| Xingxing He | 3 | 84 | 13.90 |
| xiaomei zhong | 4 | 0 | 0.34 |
| Shuwei Chen | 5 | 121 | 12.14 |