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）.展开更多
Many reduction systems have been presented for implementing functional programming languages. We propose here an extension of a reduction architecture to realize a kind of logic programming——pure Horn clause logic p...Many reduction systems have been presented for implementing functional programming languages. We propose here an extension of a reduction architecture to realize a kind of logic programming——pure Horn clause logic programming.This is an attempt to approach amalgama- tion of the two important programming paradigms.展开更多
A series of Petri net-based definitions were formulated for describing four types of structural errors in a rule-based system(RBS),including inconsistency,incompleteness,redundancy and circularity.A marked v-Petri net...A series of Petri net-based definitions were formulated for describing four types of structural errors in a rule-based system(RBS),including inconsistency,incompleteness,redundancy and circularity.A marked v-Petri net model of acyclic RBS was constructed.Then,its reachability tree was generated to record all reachable relations between propositions in RBS.Moreover,a backward reasoning forest of a reachable marking was generated for explicitly representing reachable paths in RBS.Finally,a set of theorems and algorithms were provided to analyze and check structural errors.The usability of the research results presented in this paper was illustrated by an example.展开更多
基金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）.
基金This work was done by the author when he was a visiting researcher in the research group of Prof.Dr.Werner Kluge at Kiel University,supported by the grant of Federal M ster of Science and Technology of Germany.
文摘Many reduction systems have been presented for implementing functional programming languages. We propose here an extension of a reduction architecture to realize a kind of logic programming——pure Horn clause logic programming.This is an attempt to approach amalgama- tion of the two important programming paradigms.
基金supported by the National Basic Research Program of China (Nos.2003CB317002 and 2007CB316502)the National Natural Science Foundation of China (Grant Nos.60534060 and 90718012).
文摘A series of Petri net-based definitions were formulated for describing four types of structural errors in a rule-based system(RBS),including inconsistency,incompleteness,redundancy and circularity.A marked v-Petri net model of acyclic RBS was constructed.Then,its reachability tree was generated to record all reachable relations between propositions in RBS.Moreover,a backward reasoning forest of a reachable marking was generated for explicitly representing reachable paths in RBS.Finally,a set of theorems and algorithms were provided to analyze and check structural errors.The usability of the research results presented in this paper was illustrated by an example.
