China09SummerSchool4講座3：描述邏輯可判定性與復(fù)雜性

語義網(wǎng)的邏輯基礎(chǔ)

LogicalFoundationoftheSemanticWeb主講：黃智生ZhishengHuangVrijeUniversityAmsterdam，TheNetherlandshuang@cs.vu.nl助教：胡偉WeiHuSoutheastUniversitywhu@seu.edu.cnChina20091課程時(shí)間表Schedule

China20092為什么可判定性是重要的？描述邏輯的可判定性描述邏輯的tableau算法計(jì)算復(fù)雜性理論導(dǎo)論描述邏輯的復(fù)雜性

講座3：描述邏輯的可判定性

與復(fù)雜性

Lecture3:TheDecidabilityandtheComplexityofDescriptionLogicsChina20093邏輯研究的幾個(gè)步驟提出一個(gè)邏輯系統(tǒng)（句法，語義，與公理系統(tǒng)）證明其公理系統(tǒng)的正確性（soundness）證明其公理系統(tǒng)的完備性（completeness）證明其關(guān)問題的可判定性（decidability）證明其關(guān)問題算法的復(fù)雜性（complexity）(并說明其是否具有易處理性tractability）China20094為什么可判定性是重要的？

可判定性給出了一個(gè)計(jì)算上的特征指標(biāo)，來判定是否存在著一個(gè)有效的算法來解決特定的問題。不可判定性則表明尋找解決該類問題的有效算法是徒勞的。China20095算法與可判定性

AlgorithmandDecidability可判定性(decidability):一個(gè)邏輯系統(tǒng)的一個(gè)理論（即一個(gè)邏輯封閉的公式集）被稱為是可判定的，當(dāng)且僅當(dāng)存在著一個(gè)有效的方法來決定任意一個(gè)公式是否被包含在這個(gè)理論之中Atheory(setofformulasclosedunderlogicalconsequence)inafixedlogicalsystemisdecidableifthereisaneffectivemethodfordeterminingwhetherarbitraryformulasareincludedinthetheory.計(jì)算一個(gè)函數(shù)值的有效的方法被稱為一個(gè)算法（algorithm）。Aneffectivemethodforcalculatingthevaluesofafunctionisanalgorithm;functionswithaneffectivemethodaresometimescalledeffectivelycalculable.China20096邏輯系統(tǒng)和可判定性Logicsanddecidability一個(gè)邏輯系統(tǒng)是可判定的當(dāng)且僅當(dāng)存在著一個(gè)有效的方法來決定任意一個(gè)公式是否是該邏輯系統(tǒng)的一個(gè)定理Alogicalsystemisdecidableifthereisaneffectivemethodfordeterminingwhetherarbitraryformulasaretheoremsofthelogicalsystem.思考：這個(gè)定義同上頁中的定義有什么不同？China20097一些邏輯系統(tǒng)的判定性命題邏輯是可判定的Propositionallogicisdecidable一般來說，一階謂詞邏輯是不可判定的。First-orderlogicisnotdecidableingeneral;inparticular,thesetoflogicalvaliditiesinanysignaturethatincludesequalityandatleastoneotherpredicatewithtwoormoreargumentsisnotdecidable.二階邏輯也是不可判定的second-orderlogic,isalsoundecidable.China20098一些可判定的一階謂詞邏輯Fragment?China20099固定變?cè)囊浑A邏輯

FixedVariableFOChina200910二變?cè)浑A謂詞邏輯FO2二變?cè)浑A謂詞邏輯FO2具有有限模型性，故是可判定的（Mortmer1975）China200911描述邏輯的可判定性描述邏輯ALC是可判定的。China200912描述邏輯的不可判定性現(xiàn)在你應(yīng)該知道了為什么uncle關(guān)系是無法用可判定的描述邏輯來定義的了。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方法來證明一個(gè)subsumption斷言，或者是instance斷言？China200922MoreTransformationRulesChina200923Reasoning:Decidabilityvs.ExpressivityKRsystemshouldanswerqueriesinareasonabletime.Thereasoningproceduresshouldterminate.Trade-offbetweenthe

expressivityofDLsandthecomplexityoftheirreasoning.VeryexpressiveDLscanhaveinferenceproblemsofhighcomplexity,theymayevenbeundecidable.VeryWeakDLsmynotbesufficientlyexpressivetorepresenttheimportantconceptsofanapplication.QuestforahighlyexpressiveDLwithdecidable/practicalinferenceproblems.China200924計(jì)算復(fù)雜性理論導(dǎo)論

IntroductiontoComputationalcomplexitytheory計(jì)算復(fù)雜性理論是計(jì)算機(jī)理論科學(xué)的一部分，它研究計(jì)算問題是所需要的資源。時(shí)間復(fù)雜性是指在完成一個(gè)算法所需要的時(shí)間開銷，空間復(fù)雜性是指在完成一個(gè)算法所需要的存儲(chǔ)空間上的開銷。China200925大O標(biāo)記法

BigOnotation與輸入數(shù)據(jù)長(zhǎng)度相關(guān)的時(shí)間復(fù)雜性度量

O（x）對(duì)數(shù)復(fù)雜性O(shè)(log(n))線性復(fù)雜性O(shè)(n)平方復(fù)雜性O(shè)(n2)多項(xiàng)式復(fù)雜性O(shè)(ni)指數(shù)復(fù)雜性O(shè)(2n)China200926復(fù)雜性類

Complexityclass復(fù)雜性類是指一類具有相同復(fù)雜性的問題集合acomplexityclassisasetofproblemsofrelatedcomplexity.一個(gè)典型的復(fù)雜性類可定義成一個(gè)基于某種抽象計(jì)算機(jī)的大O標(biāo)記類Atypicalcomplexityclasshasadefinitionoftheform:thesetofproblemsthatcanbesolvedbyabstractmachineMusingO(f(n))ofresourceR(nisthesizeoftheinput)China200927圖靈機(jī)：TuringMachine

China200928TuringMachine:FormalDefinitionChina200929典型復(fù)雜性類NP類：不確定的圖靈機(jī)在多項(xiàng)式時(shí)間內(nèi)可完成。TheclassNPisthesetofdecisionproblemsthatcanbesolvedbyanon-deterministicTuringmachineinpolynomialtimeP類：確定的圖靈機(jī)在多項(xiàng)式時(shí)間內(nèi)可完成。

PSPACE類：確定的圖靈機(jī)在多項(xiàng)式空間內(nèi)可完成。PSPACEisthesetofdecisionproblemsthatcanbesolvedbyadeterministicTuringmachineinpolynomialspace.China200930NP完全的（NP-complete）一個(gè)NP

完全的問題是指它是NP的（即用一個(gè)NP算法是可以解決的，它指出了復(fù)雜性的上界）它是NP難度的（NP-hard）（指任何NP問題都可以在多項(xiàng)式時(shí)間內(nèi)轉(zhuǎn)成它，即它起碼要用NP算法才能解決的，它指出了復(fù)雜性的下界）anyprobleminNPcanbereducedinpolynomialtime.同樣定義可以類推到其他計(jì)算復(fù)雜完全類China200931NL類NL：非常簡(jiǎn)單的復(fù)雜性類（不確定的圖靈機(jī)在對(duì)數(shù)空間里可解決）(NondeterministicLogarithmic-space)isthecomplexityclasscontainingdecisionproblemswhichcanbesolvedbyanondeterministicTuringmachineusingalogarithmicamountofmemoryspace.China200932復(fù)雜類之間的關(guān)系

Relationamongcomplexityclasses著名的NP問題China200933復(fù)雜類之間的關(guān)系

RelationamongcomplexityclassesPSPACE=NPSPACE

（Savitch'stheorem）（spacehierarchytheorem）China200934復(fù)雜類之間的關(guān)系

RelationamongcomplexityclassesChina200935描述邏輯復(fù)雜性一覽ALCN的可滿足性問題是PSPACE完全的SatisfiabilityofALCN-conceptdescriptionsisPSpace-complete.ALCN-