Anytime Reasoning in First-Order Logic

  • 格式:pdf
  • 大小:65.67 KB
  • 文档页数:7

AnytimeReasoninginFirst-OrderLogicKeithB.VanderveenandC.V.Ramamoorthy

AbstractWeproposeaclassofalgorithmswhichgivesbest-effortsanswerstoproblemsinfirst-orderlogicgivenaboundontheresourcesavailableforreasoning.Thealgorithmsinthisclassgenerateandattempttosolveandapproximationstotheinputproblem,thenusetheresultstodeterminethemostlikelysolutiontotheinputproblem.Weshowthatanalgorithminthisclassoutperformstheoremproverswhichattempttosolvetheproblemdirectly.

1IntroductionFirst-orderlogicisusedtodayinavarietyofappli-cationssuchasverificationofhardwareandsoftware,solvingresourceallocationandschedulingproblems[1],andansweringqueriesposedtoknowledgebases.However,theuseoffirst-orderlogicalreasoninginapplicationsrequiringreal-timedecisionmakinghasbeeninhibitedbecauseoftheinabilitytogiveboundsontheresourcesneededtosolveevenverysmallprob-lems.Formanyreal-timedecision-makingapplications,itisnecessarytomakethebestdecisionpossiblewithlimitedresourcesforreasoning(usuallythelimitedre-sourceistime).Forexample,incontent-basedroutingofmessagesbetweendistributedintelligentagents,itisimportanttoroutethemessagesquickly,evenifthismeansthatsomemessagesaremisdelivered.Someer-rorscanbetoleratedincontent-basedrouting,sinceitiscommonlyassumedthattheroutingprocessisunre-liableanywayduetonetworkproblems[6].expressioninwhichallofthevariablesarequantifiedover.Foramorethoroughexplanationoffirst-orderlogic,see[8].Throughouttherestofthepaper,wewillregardallvariablesappearinginsentencesasbeingim-plicitlyuniversallyquantifiedandomitthequantifierstoimprovereadability.Givenasentenceinfirst-orderlogic,ouralgorithmattemptstodeterminewhetherornotthesentenceissatisfiable.Bysatisfiable,wemeanthatthereexistsamodelinwhichthesentenceistrueundersomeassign-mentofvariablestoobjectsinthemodel.Allreason-inginfirst-orderlogiccanbereducedtodeterminingthesatisfiabilityofsentences,sincewecanprovethatasetofsentencesentailsasentence()byshowingthatisunsatisfiable,whereistheconjunctionofthesentencesin[8].Thismethodofproofisknownasproofbyrefutation,andisthebasisofmostautomatedtheoremprovingtechniquesincludingresolution[8].Wesaythatsentenceisweakerthanifissatisfiableonlyifis,i.e.allmodelsforarealsomodelsfor.Wesaythatsentenceisstrongerthanifandonlyifisweakerthan,i.e.allmodelsforarealsomodelsfor.3andApproximationsSchaerfandCadoliintroducedsimpletechniquesofgeneratingweakerandstrongerapproximationsofsentencesinpropositionallogic,modallogic,andfrag-mentsoffirst-orderlogic[9].Theweakerapprox-imationsareknownasapproximations,andthestrongerapproximationsasapproximations.Wehaveextendedandapproximationstoallsen-tencesinfirst-orderlogic.Tounderstandandapproximationsforsen-tencesinfirst-orderlogic,itishelpfultofirstconsidertheseapproximationsforpropositionalsentences.Theprocessofcomputingandapproximationsisparticularlyeasytodescribeforsentenceswhichareinnegatednormalform(NNF),whichmeansthatallnegationsoccuratthelevelofliterals(propositionsforpropositionallogicandoccurrencesofpredicatesforfirst-orderlogic).AnysentencecanbeconvertedtoNNFinsteps,whereisthenumberofliter-alsandisthemaximumdepthofnestedconjunc-tions,disjunctions,orimplications,byapplyingDeMorgan’sLaws[9].AnapproximationisformedforapropositionalsentenceinNNFbyreplacingallpositiveandnega-tiveoccurrencesofsomesetofpropositionallettersbythetruthvalue‘true’.Forexample,ifisthesen-tence,thenthereisonepositiveandonenegativeoccurrenceofin.If,thentheapproximationofforthesetwouldbe,sincebothandwouldbesetto’true’.approxima-tionsareformedsimilarly,exceptthattheoccurrencesofpropositionallettersinthesetarereplacedbythetruthvalue‘false’insteadof‘true’.Thus,theap-proximationofforthesetwouldbe‘false’(sincewereplacebothandwith‘false’,whichrendersthewholeconjunction‘false’).Determiningorapproximationsforasen-tenceinfirst-orderlogicisgreatlysimplifiedif,inad-ditiontobeinginNNF,thesentencehasonlyuniver-salquantifierswhichhavetheentiresentenceastheirscope.Anysentencecanbeputinthisform,see[8]fordetails.andapproximationsforfirst-ordersentencesarecomputedinafashionsimilartothatforpropositionalsentences,exceptthatinsteadofreplac-ingoccurrencesofpropositionalletterswith‘true’or‘false’,wereplaceoccurrencesofpredicates.Forex-ample,considerthefollowingsentenceinwhichandarevariables(implicitlyuniversallyquantified)andandareconstants:

If,thentheapproximationofthesentencewouldbe‘true’andtheapproximationwouldbe‘false’.Acomplicationwithwhichwemustdealinthecaseofapproximationstofirst-ordersentencescon-cernsvariants,whichareoccurrencesofpredicateswhichhavethesameargumentsexceptforachangeofvariables.andintheabovesen-tencearevariants;andarenot.Sinceallofthevariablesareuniversallyquantified,variantsofaliteralmusthaveexactlythesametruthvalueastheliteral.Therefore,wemusttreatallvariantsthesamewhenwedoorapproximation.Forexam-ple,if,thentheapproximationfortheabovesentencebecomes