1、China 2009,1,语义网的逻辑基础 Logical Foundation of the Semantic Web,主讲： 黄智生 Zhisheng HuangVrije University Amsterdam， The Netherlandshuangcs.vu.nl助教： 胡伟 Wei HuSoutheast U,China 2009,2,课程时间表Schedule,China 2009,3,为什么可判定性是重要的？描述逻辑的可判定性描述逻辑的tableau算法计算复杂性理论导论描述逻辑的复杂性,讲座3：描述逻辑的可判定性与复杂性Lecture 3: The Decidabilit
2、y and the Complexity of Description Logics,China 2009,4,逻辑研究的几个步骤,提出一个逻辑系统（句法，语义，与公理系统）证明其公理系统的正确性（soundness）证明其公理系统的完备性（completeness）证明其关问题的可判定性（decidability）证明其关问题算法的复杂性（complexity）(并说明其是否具有易处理性tractability）,China 2009,5,为什么可判定性是重要的？,可判定性给出了一个计算上的特征指标，来判定是否存在着一个有效的算法来解决特定的问题。不可判定性则表明寻找解决该类问题的有效算法是
3、徒劳的。,China 2009,6,算法与可判定性 Algorithm and Decidability,可判定性(decidability): 一个逻辑系统的一个理论（即一个逻辑封闭的公式集）被称为是可判定的， 当且仅当存在着一个有效的方法来决定任意一个公式是否被包含在这个理论之中A theory (set of formulas closed under logical consequence) in a fixed logical system is decidable if there is an effective method for determining whether arb
4、itrary formulas are included in the theory.计算一个函数值的有效的方法被称为一个算法（algorithm）。An effective method for calculating the values of a function is an algorithm; functions with an effective method are sometimes called effectively calculable.,China 2009,7,逻辑系统和可判定性Logics and decidability,一个逻辑系统是可判定的 当且仅当存在着一个
5、有效的方法来决定任意一个公式是否是该逻辑系统的一个定理A logical system is decidable if there is an effective method for determining whether arbitrary formulas are theorems of the logical system.思考： 这个定义同上页中的定义有什么不同？,China 2009,8,一些逻辑系统的判定性,命题逻辑是可判定的Propositional logic is decidable一般来说，一阶谓词逻辑是不可判定的。First-order logic is not dec
6、idable in general; in particular, the set of logical validities in any signature that includes equality and at least one other predicate with two or more arguments is not decidable. 二阶逻辑也是不可判定的second-order logic, is also undecidable.,China 2009,9,一些可判定的一阶谓词逻辑Fragment,China 2009,10,固定变元的一阶逻辑Fixed Var
7、iable FO,China 2009,11,二变元一阶谓词逻辑FO2,二变元一阶谓词逻辑FO2具有有限模型性，故是可判定的（Mortmer 1975）,China 2009,12,描述逻辑的可判定性,描述逻辑ALC是可判定的。,China 2009,13,描述逻辑的不可判定性,现在你应该知道了为什么uncle关系是无法用可判定的描述逻辑来定义的了。,China 2009,14,DL Reasoning Algorithms,Structural subsumption algorithmsSubsumption of concepts can be computed.They are com
8、plete for simple languages with little expressivity.Used by KL-ONE, LOOM and other systems.Tableaubased algorithms (推演表算法)Turned out to be very efficient reasoning algorithms.Sound, complete and decidable.Used e.g. in RACER.,China 2009,15,描述逻辑的推理算法,Tableau algorithms used to test satisfiability (con
9、sistency)Try to build a tree-like model of the input concept CDecompose C syntacticallyApply tableau expansion rulesInfer constraints on elements of modelTableau rules correspond to constructors in logic (u, t etc)Some rules are nondeterministic (e.g., t, 6)In practice, this means searchStop when no
10、 more rules applicable or clash occurs Clash is an obvious contradiction, e.g., A(x), :A(x)Cycle check (blocking) may be needed for terminationC satisfiable iff rules can be applied such that a fully expanded clash free tree is constructed,China 2009,16,DL Reasoning: Decision Procedures,Theorem: Tab
11、leaux algorithms are decision procedures for concept satisfiability (& subsumption & w.r.t. an ontology)i.e., algorithms return “SAT” iff input concept is satisfiableTerminatingBounds on out-degree (rule applications per node) and depth (blocking) of treeSoundCan construct a tableau, and hence a mod
12、el, from a fully expanded and clash-free treeCompleteCan use a model to guide application of non-deterministic rules and so construct a clash-free tree,China 2009,17,Structural Subsumption Algorithm,Proceed in two phasesThe descriptions to be tested for subsumption are normalized.Then the syntactic
13、structure of the normal forms is compared with each other.An FLo- concept description is in normal form iff it is of the formA1 Am R1.C1 Rn.CnWhere A1,., Am are distinct concept names, R1,., Rn are distinct roles names, and C1, Cn are concept descriptions in normal from.,China 2009,18,Structural Sub
14、sumption Algorithm (contd.),Given is the normal form of the concept description CA1 Am R1.C1 Rn. Cnand the normal form of the concept description DB1 Bk S1.D1 Sl. DlD subsumes C: C D iff i, 1 i k, j, 1 j m: Bi = Aji, 1 i l, j, 1 j n:Si = Rj and Cj Di,China 2009,19,Tableau-based Algorithms,Construct
15、a model for the input concept description C0.Model is represented by tree form.The formula has been translated into Negation Normal Form (NNM).To decide satisfiability of the concept C0 , start with the initial tree (root node).Repeatedly apply expansion rules until find contradiction or expansion c
16、ompleted.Satisfiable iff a complete and contradiction-free tree is found.,China 2009,20,Transformation Rules,China 2009,21,Tableau-based Algorithms - Example,Determine the satisfiability of the concept-definition:( ( CHILD. Male ) ( CHILD. Male ) )( ( CHILD. Male ) ( CHILD. Male ) ) ( CHILD. Male )
17、-rule( CHILD. Male ) ruleCHILD -rule Male -ruleMale -rule,China 2009,22,思考,如何用Tableau方法来证明一个subsumption断言，或者是instance断言？,China 2009,23,More Transformation Rules,China 2009,24,Reasoning: Decidability vs. Expressivity,KR system should answer queries in a reasonable time.The reasoning procedures should
18、 terminate.Trade-off between the expressivity of DLs and the complexity of their reasoning.Very expressive DLs can have inference problems of high complexity, they may even be undecidable. Very Weak DLs my not be sufficiently expressive to represent the important concepts of an application. Quest fo
19、r a highly expressive DL with decidable/ practical inference problems.,China 2009,25,计算复杂性理论导论Introduction to Computational complexity theory,计算复杂性理论是计算机理论科学的一部分，它研究计算问题是所需要的资源。时间复杂性是指在完成一個算法所需要的时间开销，空间复杂性是指在完成一個算法所需要的存储空间上的开销。,China 2009,26,大O标记法Big O notation,与输入数据长度相关的时间复杂性度量 O（x）对数复杂性O(log(n)线性复
20、杂性O(n)平方复杂性O(n2)多项式复杂性O(ni)指数复杂性O(2n),China 2009,27,复杂性类Complexity class,复杂性类是指一类具有相同复杂性的问题集合a complexity class is a set of problems of related complexity.一个典型的复杂性类可定义成一个基于某种抽象计算机的大O标记类A typical complexity class has a definition of the form: the set of problems that can be solved by abstract machine
21、 M using O(f(n) of resource R (n is the size of the input),China 2009,28,图灵机： Turing Machine,China 2009,29,Turing Machine: Formal Definition,China 2009,30,典型复杂性类,NP类： 不确定的图灵机在多项式时间内可完成。The class NP is the set of decision problems that can be solved by a non-deterministic Turing machine in polynomial
22、 timeP类： 确定的图灵机在多项式时间内可完成。 PSPACE类：确定的图灵机在多项式空间内可完成。PSPACE is the set of decision problems that can be solved by a deterministic Turing machine in polynomial space.,China 2009,31,NP完全的（NP-complete）,一个NP 完全的问题 是指它是NP的（即用一个NP算法是可以解决的，它指出了复杂性的上界）它是NP难度的（NP-hard）（指任何NP问题都可以在多项式时间内转成它，即它起码要用NP算法才能解决的，它指出
23、了复杂性的下界）any problem in NP can be reduced in polynomial time.同样定义可以类推到其他计算复杂完全类,China 2009,32,NL类,NL ：非常简单的复杂性类（不确定的图灵机在对数空间里可解决）(Nondeterministic Logarithmic-space) is the complexity class containing decision problems which can be solved by a nondeterministic Turing machine using a logarithmic amoun
24、t of memory space.,China 2009,33,复杂类之间的关系Relation among complexity classes,著名的NP问题,China 2009,34,复杂类之间的关系Relation among complexity classes,PSPACE = NPSPACE （Savitchs theorem）,（space hierarchy theorem）,China 2009,35,复杂类之间的关系Relation among complexity classes,China 2009,36,描述逻辑复杂性一览,ALCN的可满足性问题是PSPACE完
25、全的Satisfiability of ALCN-concept descriptions is PSpace-complete.ALCN-Aboxes的一致性问题是PSPACE完全的Consistency of ALCN-ABoxes is PSpace-complete.,China 2009,37,P类,China 2009,38,NP类与Co-NP类,China 2009,39,PSPACE,China 2009,40,EXPTime,China 2009,41,NEXPTime,China 2009,42,不可判定的DL问题,China 2009,43,练习题,T-Box A-Box
26、Female Male Human Mary: MotherMother Female John: FatherFather Male Mary: parent.ChildChild has.Mother has.Father John: parent.ChildDisjoint（Female,Male）,证明下列断言：（i）Mary:Human（ii) John: Female(iii) disjoint(Mother,Father).,China 2009,44,练习题,用Tableau方法判断下列subsumption是否成立？分析为什么KL-one是不可判定的语言？,China 2009,45,通知,今天下午郊游活动改成自由活动。今天下午另外增加一次座谈，自由决定是否参加（已有40名学员报名参加并准备发言），地点：计算机学院301室，下午2时开始。欢迎旁听。,China 2009,46,China 2009,47,语义网逻辑基础演义,第四回：问题求解寻算法判定性为先 逻辑推理说论证复杂性作本 欲知后事如何，请听下回分解。,China 2009,48,Questions and Discussions,
