Automatic Deduction and Logic Programming Extensio

UniversitadegliStudidiTorinoDottoratodiRicercainInformatica(IXciclo)PhDThesis(RevisedversiondatedApril14,1998)NormalMultimodalLogics:AutomaticDeductionandLogicProgrammingExtensionMatteoBaldoniAdvisor:Prof.AlbertoMartelliCo-Advisor:Dr.LauraGiordanoDipartimentodiInformatica|UniversitadegliStudidiTorinoC.soSvizzera,185|I-10149Torino(Italy)rstintroducedbyFari~nasdelCerroandPenttonen,includessomewell-knownnon-homogeneousmultimodalsystemscharacterizedbyinteractionaxiomsoftheform[t1][t2]:::[tn]’[s1][s2]:::[sm]’,thatwecallinclusionaxioms.Thethesisisorganizedintwopart.Intherstparttheclassofinclusionmodallogicsisdeeplystudiedbyintroducingthethesyntax,thepossible-worldssemantics,andtheaxiomatization.Afterwards,wedeneaprooftheorybasedonananalytictableaucalculus.Themainfeatureofthecalculusisthatitcandealinauniformwaywithanymultimodallogicsintheconsideredclass.Inordertoachievethisgoal,weuseaprexedtableaucalculusalaFitting,where,however,weexplicitlyrepresentaccessibilityrelationsbetweenworldsbymeansofagraphandweusethecharacterizingaxiomsofthelogicasrewritingruleswhichcreatenewpathamongworldsinthecounter-modelconstruction.Some(un)decidabilityresultsforthisclassoflogicaregiven.Moreover,thetableaumethodisextendedinordertodealwithawideclassofnormalmultimodallogicsthatincludestheonescharacterizedbyserial,symmetric,andEuclideanaccessibilityrelations.Inthesecondpart,weproposethelogicprogramminglanguageNemoLOG.Thislan-guageextendstheHornclauseslogicallowingfreeoccurrencesofuniversalmodaloperatorsinfrontofgoals,infrontofclauses,andinfrontofclauseheads.Theconsideredmultimodalsystemsaretheonesoftheclassofinclusionmodallogics.Theaimofourproposalisnotonlytoextendlogiclanguagesinordertoperformepistemicreasoningandreasoningaboutactionsbutespeciallytoprovidetoolsforsoftwareengineering(e.g.modularityandin-heritanceamongclasses)retainingadeclarativeinterpretationoftheprograms.AprooftheoryisdevelopedforNemoLOGandthesoundnessandcompletenesswithrespecttothemodeltheoryareshownbyaxedpointconstruction.iiamioPapaivContentsPrefacexiPartOne:InclusionModalLogics3IIntroduction3IISyntaxandSemantics9II.1Syntax::::::::::::::::::::::::::::::::::::9II.2Possible-worldssemantics::::::::::::::::::::::::::10II.3Axiomatization:::::::::::::::::::::::::::::::11Inclusionaxiomschemas::::::::::::::::::::::::11Someexamples:::::::::::::::::::::::::::::12InclusionframesandKripkeA-interpretation:::::::::::::15Soundnessandcompleteness::::::::::::::::::::::17IIIProofTheory21III.1Preliminarynotions:::::::::::::::::::::::::::::21III.2Atableaucalculus::::::::::::::::::::::::::::::23III.3Soundnessandcompleteness::::::::::::::::::::::::28Soundness::::::::::::::::::::::::::::::::28Completeness::::::::::::::::::::::::::::::29IVDecidability33IV.1Grammars,languagesandmodallogics::::::::::::::::::33IV.2Undecidabilityresultsforinclusionmodallogics:::::::::::::36IV.3Adecidabilityresultforinclusionmodallogics::::::::::::::39VFirst-Order45V.1Syntax::::::::::::::::::::::::::::::::::::45V.2Possible-worldssemantics::::::::::::::::::::::::::46V.3Apredicatetableaucalculus::::::::::::::::::::::::49vviContentsVITowardsawiderclassoflogics53VI.1Syntaxandpossible-worldssemantics:::::::::::::::::::53Syntax::::::::::::::::::::::::::::::::::53Possible-worldssemantics::::::::::::::::::::::::54VI.2Incestualmodallogics::::::::::::::::::::::::::::55VI.3Atableaucalculus::::::::::::::::::::::::::::::59Soundnessandcompleteness::::::::::::::::::::::65VIIRelatedwork69VII.1Prexedtableausystems::::::::::::::::::::::::::69VII.2Translationmethods:::::::::::::::::::::::::::::73PartTwo:InclusionModalLogicsforProgramming77VIIIIntroduction77IXAProgrammingLanguage81IX.1Syntax::::::::::::::::::::::::::::::::::::81Someexamplesofmodallogicprograms::::::::::::::::83IX.2Operationalsemantics::::::::::::::::::::::::::::84Derivabilityrelation:::::::::::::::::::::::::::84Agoaldirectedproofprocedure::::::::::::::::::::86IX.3UniformproofsforNemoLOG:::::::::::::::::::::::89Asequentcalculus::::::::::::::::::::::::::::89Uniformproofs:::::::::::::::::::::::::::::91IX.4TranslatingNemoLOGprogramsintoHornclauselogic::::::::::96Thetranslationmethod:::::::::::::::::::::::::97XApplications103X.1Beliefs,knowledge,andactionsrepresentation::::::::::::::103X.2Deningmodules::::::::::::::::::::::::::::::105Flatcollectionofmodules::::::::::::::::::::::::106Compositionofmodules:exportinginformation::::::::::::107Nestedmodules:::::::::::::::::::::::::::::108Parametricmodules:::::::::::::::::::::::::::110X.3Inheritanceandhierarchies:::::::::::::::::::::::::112Evolvingandconservativesystemswithdynamicorstaticcongura-tionofmodules:::::::::::::::::::::::::115XIFixedPointSemantics119XI.1Immediateconsequencetransformation::::::::::::::::::119Interpretationsandweaksatisability:::::::::::::::::119TPoperator:::::::::::::::::::::::::::::::120C