Author Description

ThisvolumecontainsthepaperspresentedattheNinthInternationalC- ferenceonLogicforProgramming,Arti?cialIntelligence,andReasoning(LPAR 2002),heldonOctober14–18,2002,attheUniversityofTbilisi(Georgia),- getherwiththeThirdInternationalWorkshoponImplementationofLogics. Therewere68submissions,ofwhicheightbelongedtothespecialsubmission categoryofexperimentalpapers,intendedtodescribeimplementationsorc- parisonsofsystems,orexperimentswithsystems. Eachsubmissionwasreviewed byatleastthreeprogramcommitteemembersandanelectronicprogramc- mitteemeetingwasheldviatheInternet. Thenumberofsubmissionsandshort reviewingperiodcausedalargeamountofwork,andweareverygratefultothe other22PCmembersfortheire?ciencyandforthequalityoftheirreviewsand discussions. Finally,thecommitteedecidedtoaccept30papers. Theprogramme alsoincludesthreeinvitedlecturesandapostersession.^ Apartfromtheprogrammecomittee,wewouldalsoliketothanktheother people who made LPAR 2002 possible: the additional referees, and the local arrangementschairsKhimuriRhukia,KotePhakadze,GelaChankvetadze,and JemalAntidze. TheInternet-basedsubmissionsoftwareandtheprogramcommitteedisc- sionsoftwarewereprovidedbythesecondco-chair.^ August2002 MatthiasBaaz AndreiVoronkov ConferenceOrganization ProgramChairs MatthiasBaaz(TechnischeUniversit¨atWien) AndreiVoronkov(UniversityofManchester) ProgramCommittee ElviraAlbert(UniversidadPolitecnicadeValencia) FranzBaader(TechnischeUniversit¨atDresden) MauriceBruynooghe(KatholiekeUniversiteitLeuven) PatrickCousot(ENSParis) MaartendeRijke(UniversityofAmsterdam) HaraldGanzinger(Max-PlanckInstitut,Saarbruc ¨ken) JeanGoubault-Larrecq(ENSdeCachan) MikiHermann(EcolePolytechnique) MatejaJamnik(UniversityofCambridge) NeilJones(KøbenhavnsUniversitet) DeepakKapur(UniversityofNewMexico) MaurizioLenzerini(Universit`adiRoma“LaSapienza”) GiorgioLevi(Universit`adiPisa) LeonidLibkin(UniversityofToronto) RobertNieuwenhuis(TechnicalUniversityofCatalonia) LeszekPacholski(WroclawskiUniwersytet) MichelParigot(Universit´eParis7) PavelPudlak(MathematicalInstitute,Prague) CarstenSchuermann(YaleUniversity) J¨orgSiekmann(DFKISaarbruc ¨ken) WolfgangThomas(RWTHAachen)^ MichaelZakharyaschev(King’sCollege) LocalOrganization KhimuriRhukia KotePhakadze GelaChankvetadze JemalAntidze VIII ConferenceOrganization ListofReferees GianlucaAmato CarlosAreces M. Arenas OferArieli RobertoBarbuti ChristophBenzmueller MartaBilkova BrunoBlanchet AlexandreBoisseau AhmedBouajjani DmitriChubarov PabloCordero VeroniqueCortier AgostinoDovier RachidEchahed MorenoFalaschi C`esarFerri OlivierGasquet BernhardGramlich Jos´eManuelG´omez PhilippedeGroote RainerHaehnle JiriHanika JuanHeguiabehere JoseHernandez-Orallo ThomasHillenbrand JoeHurd EmilJerabek ValentinJijkoun KonstantinKorovin G.^ Lakemeyer DominiqueLarchey-Wendling OlivierLaurent StefanLeue LuigiLiquori ChristofLoeding CarstenLutz ChristopherLynch PatrickMaier PaoloMancarella FlorenceMaraninchi MaartenMarx Jesus ´ Medina EricaMelis AntoineMin´e RalfM¨oller PaulinDeNaurois HansdeNivelle MichaelNorrish ManuelOjeda-Aciego NikolayPelov GuyPerrier ReinhardPichler ChristopherPollett Germ´anPuebla Jean-PierreRessayre ChristianRetor´e AlexandreRiazanov MichalRossler PaulRozi`ere NikitaSakhanenko UlrikeSattler StefanSchlobach ManfredSchmidt-Schauß KonradSlind Anni-YasminTurhan ChristianUrban WimVanhoof YdeVenema So?eVerbaeten UweWaldmann KlausWeich ClausPeterWirth StefanWoehrle ConferenceOrganization IX ConferencesprecedingLPAR2001 RCLP’90,Irkutsk,SovietUnion RCLP’91,Leningrad,SovietUnion,aboardtheship“MichailLomonosov” LPAR’92,St. Petersburg,Russia,aboardtheship“MichailLomonosov” LPAR’93,St.^ Petersburg,Russia LPAR’94,Kiev,Ukraine,aboardtheship“MarshalKoshevoi” LPAR’99,Tbilisi,RepublicofGeorgia LPAR2000,ReunionIsland,France LPAR2001,Havana,Cuba TableofContents ImprovingOn-DemandStrategyAnnotations......................... 1 M. Alpuente,S. Escobar,B. Gramlich,S. Lucas First-OrderLogicasaConstraintProgrammingLanguage.............. 19 K. R. Apt,C. F. M. Vermeulen MaintenanceofFormalSoftwareDevelopmentsby Strati?edVeri?cation............................................... 36 SergeAutexier,DieterHutter ANoteonUniversalMeasuresforWeakImplicit ComputationalComplexity......................................... 53 ArnoldBeckmann ExtendingCompositionalMessageSequenceGraphs.................... 68 BenediktBollig,MartinLeucker,PhilippLucas SearchingforInvariantsUsingTemporalResolution...................^ 86 JamesBrotherston,AnatoliDegtyarev,MichaelFisher, AlexeiLisitsa ProofPlanningforFeatureInteractions:APreliminaryReport.......... 102 ClaudioCastellini,AlanSmaill AnExtensionofBDI withFunctional CTL DependenciesandComponents...................................... 115 MehdiDastani,LeendertvanderTorre BindingLogic:ProofsandModels................................... 130 GillesDowek,Th´er`eseHardin,ClaudeKirchner DirectedAutomatedTheoremProving................................ 145 StefanEdelkamp,PeterLeven AFrameworkforSplittingBDIAgents............................... 160 XiaocongFan,JohnYen OntheComplexityofDisjunctionandExplicitDe?nability PropertiesinSomeIntermediateLogics............................... 175 MauroFerrari,CamilloFiorentini,GuidoFiorino UsingBDDswithCombinationsofTheories................^.......... 190 PascalFontaine,E. PascalGribomont XII TableofContents OnExpressiveDescriptionLogicswithCompositionofRolesin NumberRestrictions............................................... 202 FabioGrandi QueryOptimizationofDisjunctiveDatabaseswithConstraints throughBindingPropagation....................................... 216 GianluigiGreco,SergioGreco,IrinaTrubtsyna,EsterZumpano ANon-commutativeExtensionofMELL.............................. 231 AlessioGuglielmi,LutzStraßburger ProceduralSemanticsforFuzzyDisjunctivePrograms.................. 247 Du?sanGuller PushdownSpeci?cations............................................ 262 OrnaKupferman,NirPiterman,MosheY. Vardi TheoremProvingwithSequenceVariablesandFlexible AritySymbols.........................................^............