A Formal Semantics and Axiomatization for Specifyi

AFormalSemanticsandAxiomatizationforSpecifyingtheDynamicsofKnowledge-basedSystemsDieterFenselRixGroenboom†AbstractWestudytheKADSspecificationlanguagesKARLand(ML)2inastatesasalgebrassetting.Theessenceoftheselanguagesisthattheyintegrateadeclarativespecificationofinferencestogetherwithcontrolinformation.Therefore,theselanguagescanbeusedtospecifythedynamicreasoningprocessofknowledge-basedsystemsbesidestheirpureinput/outputbehavior.ThedepartureofourdiscussionisthelogicMLCM(ModalLogicofCreationandModification)whichisdevelopedtoreasonaboutdynamicpropertiesofthespecificationlanguageCOLDstemmingfromsoftwareengineering.WeproposenecessaryextensionstoMLCMleadingtothedefinitionofMLCM++,andshowthatitissufficienttoexpresstheinferencestepsofKADS-models.Thethreemaincontributionsofthepaperare:definingasemanticsforthespecificationofthedynamicreasoningbehaviorofaknowledge-basedsystemwithinthestatesasalgebrasetting;proposinganextensionofMLCMforintegratingthespecificationofstaticanddynamicaspectsofasystem;andprovidingforthefirsttimeanaxiomatizationofspecificationlanguagesforknowledge-basedsystems.1IntroductionThemodelofexpertiseasdevelopedintheKADS-I[WSB92]andCommonKADSprojects[SWH+94]hasbecomeawidelyusedframeworkfordevelopinganddescribingknowledge-basedsystems(kbs).Suchamodelofexpertisecanbeusedtodescribethereasoningprocessandtheknowledgerequiredbythisreasoningprocessinanimplementation-independentman-ner.Themodeldistinguishesthreedifferenttypesofknowledge:Thedomainlayerprovidesthedomain-specificknowledgenecessaryfordefiningthetaskandforrealizingthedifferentinferencestepsoftheproblem-solvingprocess.Theinferencelayerdefinesthereasoningprocessofthekbs.Itconsistsofinferenceactions,(staticanddynamic)knowledgeroles,andaninferencestructure.Theinferenceactionsdefinetheelementaryinferencestepsofthereasoningprocess.Thestaticrolesdefinetheroleofthedomainknowledgeforthereasoningprocess.Thedynamicrolesareusedtorefertointermediateresultsoftheproblem-solvingprocess.Theinferencestructureconnectsinferenceactionsandrolesanddefinesthedata-flowdependenciesbetweentheseelements.UniversityofAmsterdam,DepartmentofSocialScienceInformatics,Roetersstraat15,1018WBAmsterdam,theNetherlands.E-mail:[e-mail]†UniversityofGroningen,DepartmentofComputingScience,P.O.Box800,9700AVGroningen,theNether-lands.E-mail:[e-mail]1Thetasklayerdefinesthegoalsofthereasoningprocessandthewaytoachievethegoals.Forthelatter,controlovertheexecutionofinferenceactionsisdefined.Duringthelastyearsacoupleofformalorexecutablespecificationlanguageshavebeende-velopedfordescribingkbs.MostofthemarebasedontheKADSmodelofexpertiseordefinetheirconceptualmodelasamodificationofthismodel.Asurveyon(mostof)theselanguagescanbefoundin[TW93,FvH94,Fen95b].SupplementingconceptualmodelingtechniquesliketheKADSmodelbyformalspecificationlanguageshasthreewellknownadvantages:Formalspecificationlanguagescanbeusedtoresolveambiguityandlackingdetailsofspecificationsstatedinnaturallanguage.Executablespecificationlanguagesenabletheevaluationofthespecificationbyproto-typing(i.e.testing).Proofcalculibasedonformalsemanticsofthelanguagescanbeusedtocheckrelevantpropertiesofaspecification.Duringthepaper,wewilldiscussanewsemanticalframeworkfortheinferenceandtask-layerinKADSwhichexpressthedynamicreasoningprocessofakbs.Infact,westudytwoKADS-languages(KARL[Fen95a]and(ML)2[vHB92])andincorporatetheideasforinfer-encesinthemulti-modallogicMLCM[GR94].Thelanguage(ML)2wasdevelopedaspartoftheKADSprojectsandprovidesaformalspecificationlanguagefortheKADSmodelofexpertisebycombiningthreetypesoflogic:order-sortedfirst-orderlogicextendedbymod-ularizationforspecifyingthedomainlayer,first-ordermeta-logicforspecifyingtheinferencelayer,andquantifieddynamiclogic[Har84],whichwasoriginallydevelopedfortheverifica-tionofproceduralprograms,forspecifyingthetasklayer.ThelanguageKARLwasdevelopedaspartoftheMIKEproject[AFL+93]andprovidesaformalandexecutablespecificationlan-guagefortheKADSmodelofexpertisebycombiningtwotypesoflogic:AvariantofFrameLogic[KLW93]isusedtospecifydomainandinferencelayers.Itcombinesfirst-orderlogicwithsemanticaldatamodelingprimitives.Arestrictedversionofdynamiclogicisprovidedtospecifyatasklayer.ExecutabilityisachievedbyrestrictingFramelogictoHornlogicwithstratifiednegationandbyrestrictingdynamiclogictoregularanddeterministicprograms.WehavechosenKARLand(ML)2forourexerciseasbothlanguages(likeMLCM)relyondynamiclogictorepresentthedynamicsofthereasoningprocess.AsthetechnicalcoreofthesemanticsofKBSSF[SP94]isclosetothatofKARL,mostoftheresultsofthepapercanalsoappliedtoit.Theotherspecificationlanguagesforkbsusedifferentmeansforspecifyingthedynamicsofakbs:Petrinets(MoMo[VV93]),abstractdatatypes(TASK[PGT95]),orlineartemporallogic(DESIRE[Tre94]).Commonforallapproachesisthataformalsemanticshastocoverthreeaspects:thespecificationofstaticaspectsofakbs,thespecificationofthedynamicsofakbs(i.e.,itsreasoning),andthecombinationofbothi.e.itsoverallsemantics.Forourstudywerestrictourattentiontothesecondandthirdpartaswethinkthatthemainimprovementhastobedoneforthedynamic