语义网的逻辑基础

1、China 20091语义网的逻辑基础 Logical Foundation of the Semantic Web主讲： 黄智生 Zhisheng HuangVrije University Amsterdam， The Netherlandshuangcs.vu.nl助教： 胡伟 Wei HuSoutheast U China 20092课程时间表ScheduleChina 20093 为什么可判定性是重要的？ 描述逻辑的可判定性 描述逻辑的tableau算法 计算复杂性理论导论 描述逻辑的复杂性 讲座3：描述逻辑的可判定性与复杂性Lecture 3: The Decidability a

2、nd the Complexity of Description LogicsChina 20094逻辑研究的几个步骤 提出一个逻辑系统（句法，语义，与公理系统） 证明其公理系统的正确性（soundness） 证明其公理系统的完备性（completeness） 证明其关问题的可判定性（decidability） 证明其关问题算法的复杂性（complexity）(并说明其是否具有易处理性tractability）China 20095为什么可判定性是重要的？ 可判定性给出了一个计算上的特征指标，来判定是否存在着一个有效的算法来解决特定的问题。 不可判定性则表明寻找解决该类问题的有效算法是徒劳的。

3、China 20096算法与可判定性 Algorithm and Decidability可判定性可判定性(decidability): 一个逻辑系统的一个理论（即一个逻辑封闭一个逻辑系统的一个理论（即一个逻辑封闭的公式集）被称为是可判定的，的公式集）被称为是可判定的， 当且仅当存在着一个有效的方法来当且仅当存在着一个有效的方法来决定任意一个公式是否被包含在这个理论之中决定任意一个公式是否被包含在这个理论之中A theory (set of formulas closed under logical consequence) in a fixed logical system is decid

4、able 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 effe

5、ctively calculable.China 20097逻辑系统和可判定性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 20098一些逻辑系统的判定性 命题逻辑

6、是可判定的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

7、also undecidable.China 20099一些可判定的一阶谓词逻辑Fragment China 200910固定变元的一阶逻辑Fixed Variable FOChina 200911二变元一阶谓词逻辑FO2二变元一阶谓词逻辑FO2具有有限模型性，故是可判定的（Mortmer 1975）China 200912描述逻辑的可判定性 描述逻辑ALC是可判定的。China 200913描述逻辑的不可判定性 现在你应该知道了为什么uncle关系是无法用可判定的描述逻辑来定义的了。China 200914DL Reasoning Algorithms Structural subsumpt

8、ion algorithms Subsumption of concepts can be computed. They are complete 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.Chi

9、na 200915描述逻辑的推理算法 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

10、 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

11、tree is constructedChina 200916DL Reasoning: Decision ProceduresTheorem: 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 n

12、ode) 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 treeChina 200917Structural Subsumption AlgorithmProceed in two phasesn

13、The descriptions to be tested for subsumption are normalized.n 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 formA1 Am R1.C1 Rn.CnWhere A1,., Am are distinct concept names, R1,., Rn are distinct roles names

14、, and C1, Cn are concept descriptions in normal from.China 200918Structural Subsumption 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 i = Aj ji, 1

15、 i l, j, 1 j n:Si i = Rj j and Cj j Di iChina 200919Tableau-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

16、 tree (root node). Repeatedly apply expansion rules until find contradiction or expansion completed. Satisfiable iff a complete and contradiction-free tree is found.China 200920Transformation RulesChina 200921Tableau-based Algorithms - ExampleDetermine the satisfiability of the concept-definition:(

17、( CHILD. Male ) ( CHILD. Male ) )( ( CHILD. Male ) ( CHILD. Male ) ) ( CHILD. Male ) -rule( CHILD. Male ) ruleCHILD -rule Male -ruleMale -ruleChina 200922思考 如何用Tableau方法来证明一个subsumption断言，或者是instance断言？China 200923More Transformation RulesChina 200924Reasoning: Decidability vs. Expressivity KR syste

18、m 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 sufficie

19、ntly expressive to represent the important concepts of an application. Quest for a highly expressive DL with decidable/ practical inference problems.China 200925计算复杂性理论导论Introduction to Computational complexity theory 计算复杂性理论是计算机理论科学的一部分，它研究计算问题是所需要的资源。时间复杂性是指在完成一個算法所需要的时间开销，空间复杂性是指在完成一個算法所需要的存储空间上的

20、开销。China 200926大O标记法Big O notation 与输入数据长度相关的时间复杂性度量 O（x） 对数复杂性O(log(n) 线性复杂性O(n) 平方复杂性O(n2) 多项式复杂性O(ni) 指数复杂性O(2n)China 200927复杂性类Complexity class 复杂性类是指一类具有相同复杂性的问题集合a complexity class is a set of problems of related complexity. 一个典型的复杂性类可定义成一个基于某种抽象计算机的大O标记类 A typical complexity class has a defin

21、ition 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 200928图灵机： Turing MachineChina 200929Turing Machine: Formal DefinitionChina 200930典型复杂性类 NP类： 不确定的图灵机在多项式时间内可完成。The class NP is the set of decision problems t

22、hat 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 200931NP完全的（NP-complete）一个NP 完全的问题 是指它是NP的（即用一个NP算法是可以解决的，它指

23、出了复杂性的上界）它是NP难度的（NP-hard）（指任何NP问题都可以在多项式时间内转成它，即它起码要用NP算法才能解决的，它指出了复杂性的下界）any problem in NP can be reduced in polynomial time.同样定义可以类推到其他计算复杂完全类China 200932NL类 NL ：非常简单的复杂性类（不确定的图灵机在对数空间里可解决）(Nondeterministic Logarithmic-space) is the complexity class containing decision problems which can be solved

24、 by a nondeterministic Turing machine using a logarithmic amount of memory space.China 200933复杂类之间的关系Relation among complexity classes著名的NP问题China 200934复杂类之间的关系Relation among complexity classesPSPACE = NPSPACE （Savitchs theorem）（space hierarchy theorem）China 200935复杂类之间的关系Relation among complexity classesChina 200936描述逻辑