语义网的逻辑基础 Logical Foundation of the Semantic Web

Presentation on theme: "语义网的逻辑基础 Logical Foundation of the Semantic Web"— Presentation transcript:

1 语义网的逻辑基础 Logical Foundation of the Semantic Web
主讲： 黄智生 Zhisheng Huang Vrije University Amsterdam， The Netherlands 助教： 胡伟 Wei Hu Southeast University 系列讲座 China 2009

2 课程时间表Schedule China 2009

3 讲座3：描述逻辑的可判定性 与复杂性 Lecture 3: The Decidability and the Complexity of Description Logics
为什么可判定性是重要的？ 描述逻辑的可判定性 描述逻辑的tableau算法 计算复杂性理论导论 描述逻辑的复杂性 China 2009

4 逻辑研究的几个步骤 提出一个逻辑系统（句法，语义，与公理系统） 证明其公理系统的正确性（soundness）
证明其公理系统的完备性（completeness） 证明其关问题的可判定性（decidability） 证明其关问题算法的复杂性（complexity） (并说明其是否具有易处理性tractability） China 2009

5 为什么可判定性是重要的？ 可判定性给出了一个计算上的特征指标，来判定是否存在着一个有效的算法来解决特定的问题。
不可判定性则表明寻找解决该类问题的有效算法是徒劳的。 China 2009

6 Algorithm and Decidability
算法与可判定性 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 arbitrary 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
逻辑系统和可判定性 Logics and decidability 一个逻辑系统是可判定的 当且仅当存在着一个有效的方法来决定任意一个公式是否是该逻辑系统的一个定理 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 decidable 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 Variable FO
China 2009

11 二变元一阶谓词逻辑FO2 二变元一阶谓词逻辑FO2具有有限模型性，故是可判定的（Mortmer 1975） China 2009

12 描述逻辑的可判定性 描述逻辑ALC是可判定的。 China 2009

13 描述逻辑的不可判定性 现在你应该知道了为什么uncle关系是无法用可判定的描述逻辑来定义的了。 China 2009

14 DL Reasoning Algorithms
Structural subsumption algorithms Subsumption of concepts can be computed. They are complete for simple languages with little expressivity. Used by KL-ONE, LOOM and other systems. Tableau–based 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 (consistency)
Try to build a tree-like model of the input concept C Decompose C syntactically Apply tableau expansion rules Infer constraints on elements of model Tableau rules correspond to constructors in logic (u, t etc) Some rules are nondeterministic (e.g., t, 6) In practice, this means search Stop when no more rules applicable or clash occurs Clash is an obvious contradiction, e.g., A(x), :A(x) Cycle check (blocking) may be needed for termination C satisfiable iff rules can be applied such that a fully expanded clash free tree is constructed China 2009

16 DL Reasoning: Decision Procedures
Theorem: Tableaux algorithms are decision procedures for concept satisfiability (& subsumption & w.r.t. an ontology) i.e., algorithms return “SAT” iff input concept is satisfiable Terminating Bounds on out-degree (rule applications per node) and depth (blocking) of tree Sound Can construct a tableau, and hence a model, from a fully expanded and clash-free tree Complete Can 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 phases The descriptions to be tested for subsumption are normalized. Then the syntactic structure of the normal forms is compared with each other. An FLo- concept description is in normal form iff it is of the form A1 П… ПAm П R1.C1 П… П Rn.Cn Where 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 Subsumption Algorithm (contd.)
Given is the normal form of the concept description C A1 П… ПAm П R1.C1 П… П Rn. Cn and the normal form of the concept description D B1 П… ПBk П S1.D1 П… П Sl. Dl D subsumes C: C  D iff i, 1≤ i ≤k,  j, 1 ≤j ≤m: Bi = Aj i, 1≤ i ≤l,  j, 1 ≤j ≤n: Si = Rj and Cj  Di China 2009

19 Tableau-based Algorithms
Construct 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 completed. 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 ) ) <x> ( CHILD. Male ) <x> П -rule ( CHILD.  Male ) <x> П –rule CHILD <x, y >  -rule  Male < y>  -rule Male <y >  -rule <CLASH > 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 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 for 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)) 线性复杂性O(n)
多项式复杂性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 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 time P类： 确定的图灵机在多项式时间内可完成。 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算法才能解决的，它指出了复杂性的下界）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 amount of memory space. China 2009

33 复杂类之间的关系 Relation among complexity classes
著名的NP问题 China 2009

34 复杂类之间的关系 Relation among complexity classes
PSPACE = NPSPACE （Savitch's theorem） （space hierarchy theorem） China 2009

35 复杂类之间的关系 Relation among complexity classes
China 2009

36 描述逻辑复杂性一览 ALCN的可满足性问题是PSPACE完全的
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 练习题 证明下列断言： （i）Mary:Human （ii) John: Female
T-Box A-Box Female  Male  Human Mary: Mother Mother  Female John: Father Father  Male Mary: parent.Child Child  has.Mother П has.Father John: parent.Child Disjoint（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
China 2009