a-Input resolution and a-unit resolution for generalized Horn clause set are discussed in linguistic truth-valued lattice-valued first-order logic （ Lv（ n × 2） F（X） ）, which can represent and handle uncerta...a-Input resolution and a-unit resolution for generalized Horn clause set are discussed in linguistic truth-valued lattice-valued first-order logic （ Lv（ n × 2） F（X） ）, which can represent and handle uncertain linguistic values-based information. Firstly the concepts of a-input resolution and a.unit resolution are presented, and the equivalence of them is shown. Then α-input （a-unit） resolution is equivalently transformed from Lv（ n × 2） F（X） into that of LnP（X）, and their soundness and completeness are also established. Finally an algorithm for a-unit resolution is contrived in LnP（ X）.展开更多
基金National Natural Science Foundations of China (No. 60875034,No. 61175055)
文摘a-Input resolution and a-unit resolution for generalized Horn clause set are discussed in linguistic truth-valued lattice-valued first-order logic （ Lv（ n × 2） F（X） ）, which can represent and handle uncertain linguistic values-based information. Firstly the concepts of a-input resolution and a.unit resolution are presented, and the equivalence of them is shown. Then α-input （a-unit） resolution is equivalently transformed from Lv（ n × 2） F（X） into that of LnP（X）, and their soundness and completeness are also established. Finally an algorithm for a-unit resolution is contrived in LnP（ X）.
