Â¥Ö÷

¶¥Ò»Ï ÎÒÒ²ÊÇѧÂß¼­³ÌÐòÉè¼Æ ÂÛÎÄÌâÄ¿£ºÂß¼­³ÌÐòÏàÈÝÐÔÓë»·¹«Ê½Ñо¿ Ŀ¼ Table of Contents Table of Contents v Abstract i 1 Introduction 1 1.1 Motivations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.3 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2 An Overview of Normal Logic Programming 8 2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.2.1 Least model . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.2.2 Stable model . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.2.3 Well-founded model . . . . . . . . . . . . . . . . . . . . . . . . 15 2.3 Computation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 2.3.1 Complexity . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.3.2 Smodels . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 2.3.3 ASSAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2.4 Syntactic extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2.4.1 Constraints and classical negation . . . . . . . . . . . . . . . . 31 2.4.2 Disjunctions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 2.4.3 Nested expressions . . . . . . . . . . . . . . . . . . . . . . . . 36 2.5 Applications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 2.5.1 Planning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 2.5.2 CSP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 2.5.3 Combinational graph problems . . . . . . . . . . . . . . . . . 41 3 Weakly Auto-compatible Logic Programs 43 3.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 3.2 Weakly auto-compatibility . . . . . . . . . . . . . . . . . . . . . . . . 44 3.2.1 Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 3.2.2 Algorithms . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 v 3.2.3 Reasoning complexities . . . . . . . . . . . . . . . . . . . . . . 56 3.3 Comparison . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 3.3.1 FC-normality . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 3.3.2 Call-consistency . . . . . . . . . . . . . . . . . . . . . . . . . . 66 3.3.3 WF-irreducible . . . . . . . . . . . . . . . . . . . . . . . . . . 71 3.4 Concluding remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 4 First-order Loop formulas 74 4.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 4.2 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 4.3 First-order loops and loop formulas . . . . . . . . . . . . . . . . . . . 80 4.4 Some properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 4.5 Concluding remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98 5 Conclusion and Future Work 100 Acknowledgements 102 Bibliography 104 A The encodings of various problems 111 A.1 Planning domain . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111 A.1.1 The block world panning, Niemel¡§a¡¯s version . . . . . . . . . . 111 A.1.2 The block world planning, Lifschitz¡¯s version . . . . . . . . . . 112 A.1.3 Hanoi tower planning . . . . . . . . . . . . . . . . . . . . . . . 113 A.2 Combinatorial graph domain . . . . . . . . . . . . . . . . . . . . . . . 114 A.2.1 Independent set . . . . . . . . . . . . . . . . . . . . . . . . . . 114 A.2.2 Maximal matching . . . . . . . . . . . . . . . . . . . . . . . . 114 A.2.3 Graph matching . . . . . . . . . . . . . . . . . . . . . . . . . . 114 ¶à½»Á÷ ys_wang168@sina.com