当前位置:文档下载 > 所有分类 > The semantic clause graph procedure
侵权投诉

The semantic clause graph procedure

Abstract. In this contribution we propose a variant of a resolution theorem prover which selects resolution steps based on the proportion of models a newly generated clause satisfies compared to all models given in a reference class, which is generated fro

TheSemanticClauseGraphProcedure

ManfredKerber

SeungyeobChoi

SchoolofComputerScienceTheUniversityofBirminghamBirminghamB152TT,England

e-mail:M.Kerber@cs.bham.ac.uk,S.Choi@cs.bham.ac.uk

URL:http://www.cs.bham.ac.uk/

Abstract.Inthiscontributionweproposeavariantofaresolutionthe-oremproverwhichselectsresolutionstepsbasedontheproportionofmodelsanewlygeneratedclausesatis escomparedtoallmodelsgiveninareferenceclass,whichisgeneratedfromasubsetoftheinitialclauseset.Sincetheemptyclausedoesnotsatisfyanymodelspreferenceisgiventosuchclauseswhichsatisfyfewmodelsonly.Inordertoavoidprema-tureconvergence,model-guidedstepsareinterleavedwithrandomsteps.Sincecomputingthenumberofmodelsiscomputationallyexpensiveontheonehand,butwillremainalmostunchangedaftertheapplicationofonesingleresolutionstepontheotherhand,weadaptKowalski’scon-nectiongraphmethodtostorethenumberofmodelsateachlink.Wereportonworkinprogressandarenotyetabletopresentexperimentalresults.

1Introduction

Theconnectiongraphproofprocedurewas rstintroducedbyKowalski[5].Themainideaistoexplicitlyrepresentallresolutionpossibilitiesaslinksinagraphbetweenliterals,wherethelinksstorenotonlytheapplicabilitybutadditionallythemostgeneraluni erfortheapplication.Independentlyofopentheoreticalquestions(likecompleteness,see[3])themethodhasnotattractedmuchatten-tioninup-to-dateresolutiontheoremproverssincethecomputationaloverheadtoexplicitlyrepresenttheuni ersinagraphdoesnotpayo comparedtoothertechniqueslikeindexing.Inotherwordsthegraphisusedtostoreinformationwhichcanbemorecheaplycomputedfrom rstprinciples.Inparticular,theheuristicchoice,onwhichlinktoresolvemakesonlymarginallyuseofthelinks.Someworkhasbeendonetointegratesemanticinformationintoresolu-tiontheoremproving.Slaney,Lusk,andMcCune[8]developedtheScott-systemwhichcombinesthemodelgeneratorFinderandtheresolutiontheoremproverOtter.Tospeakinasimpli edway,Scottextendstheset-of-supportstrategybytheintroductionofasemanticsatis abilitycheck,whichisbasedoniter-atedmodelgeneration.Itcouldbeshownthatthisapproachmakesasigni cantimprovementforsomeexamples.ChuandPlaisted[2]implementedatheoremproverusinghyper-linkingtechniques[6]withtheconceptofthesemanticguid-ance.

第1页

猜你喜欢

返回顶部