China09SummerSchool4讲座3：描述逻辑可判定性与复杂性

语义网的逻辑基础

LogicalFoundationoftheSemanticWeb主讲：黄智生ZhishengHuangVrijeUniversityAmsterdam，TheNetherlandshuang@cs.vu.nl助教：胡伟WeiHuSoutheastUniversitywhu@seu.edu.cnChina20091课程时间表Schedule

China20092为什么可判定性是重要的？描述逻辑的可判定性描述逻辑的tableau算法计算复杂性理论导论描述逻辑的复杂性

讲座3：描述逻辑的可判定性

与复杂性

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

可判定性给出了一个计算上的特征指标，来判定是否存在着一个有效的算法来解决特定的问题。不可判定性则表明寻找解决该类问题的有效算法是徒劳的。China20095算法与可判定性

AlgorithmandDecidability可判定性(decidability):一个逻辑系统的一个理论（即一个逻辑封闭的公式集）被称为是可判定的，当且仅当存在着一个有效的方法来决定任意一个公式是否被包含在这个理论之中Atheory(setofformulasclosedunderlogicalconsequence)inafixedlogicalsystemisdecidableifthereisaneffectivemethodfordeterminingwhetherarbitraryformulasareincludedinthetheory.计算一个函数值的有效的方法被称为一个算法（algorithm）。Aneffectivemethodforcalculatingthevaluesofafunctionisanalgorithm;functionswithaneffectivemethodaresometimescalledeffectivelycalculable.China20096逻辑系统和可判定性Logicsanddecidability一个逻辑系统是可判定的当且仅当存在着一个有效的方法来决定任意一个公式是否是该逻辑系统的一个定理Alogicalsystemisdecidableifthereisaneffectivemethodfordeterminingwhetherarbitraryformulasaretheoremsofthelogicalsystem.思考：这个定义同上页中的定义有什么不同？China20097一些逻辑系统的判定性命题逻辑是可判定的Propositionallogicisdecidable一般来说，一阶谓词逻辑是不可判定的。First-orderlogicisnotdecidableingeneral;inparticular,thesetoflogicalvaliditiesinanysignaturethatincludesequalityandatleastoneotherpredicatewithtwoormoreargumentsisnotdecidable.二阶逻辑也是不可判定的second-orderlogic,isalsoundecidable.China20098一些可判定的一阶谓词逻辑Fragment◮China20099固定变元的一阶逻辑

FixedVariableFOChina200910二变元一阶谓词逻辑FO2二变元一阶谓词逻辑FO2具有有限模型性，故是可判定的（Mortmer1975）China200911描述逻辑的可判定性描述逻辑ALC是可判定的。China200912描述逻辑的不可判定性现在你应该知道了为什么uncle关系是无法用可判定的描述逻辑来定义的了。China200913DLReasoningAlgorithmsStructuralsubsumptionalgorithmsSubsumptionofconceptscanbecomputed.Theyarecompleteforsimplelanguageswithlittleexpressivity.UsedbyKL-ONE,LOOMandothersystems.Tableau–basedalgorithms(推演表算法)Turnedouttobeveryefficientreasoningalgorithms.Sound,completeanddecidable.Usede.g.inRACER.China200914描述逻辑的推理算法Tableaualgorithmsusedtotestsatisfiability

(consistency)Trytobuildatree-likemodeloftheinputconceptCDecomposeCsyntacticallyApplytableau

expansionrulesInferconstraintsonelementsofmodelTableaurulescorrespondtoconstructorsinlogic(u,tetc)Somerulesarenondeterministic(e.g.,t,6)Inpractice,thismeanssearchStopwhennomorerulesapplicableorclashoccursClashisanobviouscontradiction,e.g.,A(x),:A(x)Cyclecheck(blocking)maybeneededforterminationCsatisfiableiff

rulescanbeappliedsuchthatafullyexpandedclashfreetreeisconstructedChina200915DLReasoning:

DecisionProcedures Theorem:Tableauxalgorithmsaredecisionproceduresforconceptsatisfiability(&subsumption&w.r.t.anontology) i.e.,algorithmsreturn“SAT”iff

inputconceptissatisfiableTerminatingBoundsonout-degree(ruleapplicationspernode)anddepth(blocking)oftreeSoundCanconstructatableau,andhenceamodel,fromafullyexpandedandclash-freetreeCompleteCanuseamodeltoguideapplicationofnon-deterministicrulesandsoconstructaclash-freetreeChina200916StructuralSubsumptionAlgorithmProceedintwophasesThedescriptionstobetestedforsubsumptionarenormalized.Thenthesyntacticstructureofthenormalformsiscomparedwitheachother.AnFLo-conceptdescriptionisinnormalform

iffitisoftheformA1

П…ПAm

П

R1.C1

П…П

Rn.CnWhereA1,..,Amaredistinctconceptnames,R1,...,Rn

aredistinctrolesnames,andC1,…,Cn

areconceptdescriptionsinnormalfrom.China200917StructuralSubsumptionAlgorithm

(contd.)GivenisthenormalformoftheconceptdescriptionCA1

П…ПAm

П

R1.C1

П…П

Rn.CnandthenormalformoftheconceptdescriptionD B1

П…ПBk

П

S1.D1

П…П

Sl.DlDsubsumesC:CDiff

i,1≤i≤k,

j,1≤j≤m: Bi=Aj

i,

1≤i≤l,

j,1≤j≤n: Si

=RjandCj

DiChina200918Tableau-basedAlgorithmsConstructamodelfortheinputconceptdescriptionC0.Modelisrepresentedbytreeform.TheformulahasbeentranslatedintoNegationNormalForm(NNM).TodecidesatisfiabilityoftheconceptC0,startwiththeinitialtree(rootnode).Repeatedlyapplyexpansionrulesuntilfindcontradictionorexpansioncompleted.Satisfiable

iff

acompleteandcontradiction-freetreeisfound.China200919TransformationRulesChina200920Tableau-basedAlgorithms-ExampleDeterminethesatisfiabilityoftheconcept-definition:((

CHILD.Male)П(

CHILD.

Male))((

CHILD.Male)П(

CHILD.

Male))<x>(

CHILD.Male)<x> П-rule(

CHILD.

Male)<x> П–ruleCHILD<x,y>

-rule

Male<y>

-ruleMale<y>

-rule<CLASH>China200921思考如何用Tableau方法来证明一个subsumption断言，或者是instance断言？China200922MoreTransformationRulesChina200923Reasoning:Decidabilityvs.ExpressivityKRsystemshouldanswerqueriesinareasonabletime.Thereasoningproceduresshouldterminate.Trade-offbetweenthe

expressivityofDLsandthecomplexityoftheirreasoning.VeryexpressiveDLscanhaveinferenceproblemsofhighcomplexity,theymayevenbeundecidable.VeryWeakDLsmynotbesufficientlyexpressivetorepresenttheimportantconceptsofanapplication.QuestforahighlyexpressiveDLwithdecidable/practicalinferenceproblems.China200924计算复杂性理论导论

IntroductiontoComputationalcomplexitytheory计算复杂性理论是计算机理论科学的一部分，它研究计算问题是所需要的资源。时间复杂性是指在完成一個算法所需要的时间开销，空间复杂性是指在完成一個算法所需要的存储空间上的开销。China200925大O标记法

BigOnotation与输入数据长度相关的时间复杂性度量

O（x）对数复杂性O(log(n))线性复杂性O(n)平方复杂性O(n2)多项式复杂性O(ni)指数复杂性O(2n)China200926复杂性类

Complexityclass复杂性类是指一类具有相同复杂性的问题集合acomplexityclassisasetofproblemsofrelatedcomplexity.一个典型的复杂性类可定义成一个基于某种抽象计算机的大O标记类Atypicalcomplexityclasshasadefinitionoftheform:thesetofproblemsthatcanbesolvedbyabstractmachineMusingO(f(n))ofresourceR(nisthesizeoftheinput)China200927图灵机：TuringMachine

China200928TuringMachine:FormalDefinitionChina200929典型复杂性类NP类：不确定的图灵机在多项式时间内可完成。TheclassNPisthesetofdecisionproblemsthatcanbesolvedbyanon-deterministicTuringmachineinpolynomialtimeP类：确定的图灵机在多项式时间内可完成。

PSPACE类：确定的图灵机在多项式空间内可完成。PSPACEisthesetofdecisionproblemsthatcanbesolvedbyadeterministicTuringmachineinpolynomialspace.China200930NP完全的（NP-complete）一个NP

完全的问题是指它是NP的（即用一个NP算法是可以解决的，它指出了复杂性的上界）它是NP难度的（NP-hard）（指任何NP问题都可以在多项式时间内转成它，即它起码要用NP算法才能解决的，它指出了复杂性的下界）anyprobleminNPcanbereducedinpolynomialtime.同样定义可以类推到其他计算复杂完全类China200931NL类NL：非常简单的复杂性类（不确定的图灵机在对数空间里可解决）(NondeterministicLogarithmic-space)isthecomplexityclasscontainingdecisionproblemswhichcanbesolvedbyanondeterministicTuringmachineusingalogarithmicamountofmemoryspace.China200932复杂类之间的关系

Relationamongcomplexityclasses著名的NP问题China200933复杂类之间的关系

RelationamongcomplexityclassesPSPACE=NPSPACE

（Savitch'stheorem）（spacehierarchytheorem）China200934复杂类之间的关系

RelationamongcomplexityclassesChina200935描述逻辑复杂性一览ALCN的可满足性问题是PSPACE完全的SatisfiabilityofALCN-conceptdescriptionsisPSpace-complete.ALCN-