A new method of solving Horn logic with equality,the goal-type driven method,is presented, which considers explicitly the unification operator as a goal and merged it into the resolution process. The method has the fo...A new method of solving Horn logic with equality,the goal-type driven method,is presented, which considers explicitly the unification operator as a goal and merged it into the resolution process. The method has the following advantages.The resolution and the unification have been integrated in a uniform way.The architectures of the inference engines based on Horn logic with equality are simplified. Any techniques of exploiting AND/ OR parallelism to solve goals can also be applied to unification at the same time.The method can be used to integrate the styles of functional language and logic lan- guage by a uniform framework.It can also deal with infinite data structures.展开更多
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）.展开更多
文摘A new method of solving Horn logic with equality,the goal-type driven method,is presented, which considers explicitly the unification operator as a goal and merged it into the resolution process. The method has the following advantages.The resolution and the unification have been integrated in a uniform way.The architectures of the inference engines based on Horn logic with equality are simplified. Any techniques of exploiting AND/ OR parallelism to solve goals can also be applied to unification at the same time.The method can be used to integrate the styles of functional language and logic lan- guage by a uniform framework.It can also deal with infinite data structures.
基金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）.
