Lecture Notes in Artificial Intelligence 2309 SubseriesofLectureNotesinComputerScience EditedbyJ.G.CarbonellandJ.Siekmann Lecture Notes in Computer Science EditedbyG.Goos,J.Hartmanis,andJ.vanLeeuwen 3 Berlin Heidelberg NewYork Barcelona HongKong London Milan Paris Tokyo Alessandro Armando (Ed.) Frontiers of Combining Systems 4th International Workshop, FroCoS 2002 Santa Margherita Ligure, Italy, April 8-10, 2002 Proceedings 1 3 SeriesEditors JaimeG.Carbonell,CarnegieMellonUniversity,Pittsburgh,PA,USA Jo¨rgSiekmann,UniversityofSaarland,Saarbru¨cken,Germany VolumeEditor AlessandroArmando DIST–Universita`diGenova VialeCausa13,15145Genova,Italy E-mail:[email protected] Cataloging-in-PublicationDataappliedfor DieDeutscheBibliothek-CIP-Einheitsaufnahme Frontiersofcombiningsystems:4thinternationalworkshop;proceedings/ FroCoS2002,SantaMargheritaLigure,Italy,April8-10,2002.Alessandro Armando(ed.).-Berlin;Heidelberg;NewYork;Barcelona;HongKong; London;Milan;Paris;Tokyo:Springer,2002 (Lecturenotesincomputerscience;Vol.2309:Lecturenotesin artificialintelligence) ISBN3-540-43381-3 CRSubjectClassification(1998):I.2.3,F.4.1,F.4 ISSN0302-9743 ISBN3-540-43381-3Springer-VerlagBerlinHeidelbergNewYork Thisworkissubjecttocopyright.Allrightsarereserved,whetherthewholeorpartofthematerialis concerned,specificallytherightsoftranslation,reprinting,re-useofillustrations,recitation,broadcasting, reproductiononmicrofilmsorinanyotherway,andstorageindatabanks.Duplicationofthispublication orpartsthereofispermittedonlyundertheprovisionsoftheGermanCopyrightLawofSeptember9,1965, initscurrentversion,andpermissionforusemustalwaysbeobtainedfromSpringer-Verlag.Violationsare liableforprosecutionundertheGermanCopyrightLaw. Springer-VerlagBerlinHeidelbergNewYork amemberofBertelsmannSpringerScience+BusinessMediaGmbH http://www.springer.de ©Springer-VerlagBerlinHeidelberg2002 PrintedinGermany Typesetting:Camera-readybyauthor,dataconversionbySteingra¨berSatztechnikGmbH,Heidelberg Printedonacid-freepaper SPIN:10846555 06/3142 543210 Preface This volume contains the proceedings of FroCoS 2002, the 4th International Workshop on Frontiers of Combining Systems, held April 8-10, 2002 in Santa Margherita Ligure (near Genova), Italy. Like its predecessors, organized in Mu- nich (1996), Amsterdam (1998), and Nancy (2000), FroCoS 2002 offered a com- monforumforthepresentationanddiscussionofresearchactivitiesonthecom- bination and integration of systems in various areas of computer science, such as logic, computation, program development and proof, artificial intelligence, mechanical verification, and symbolic computation. There were 35 submissions of high quality, authored by researchers from countries including Australia, Belgium, Brazil, Finland, France, Germany, Italy, Portugal,Spain,Singapore,UnitedKingdom,UnitedStatesofAmerica,andYu- goslavia. All the submissions were thoroughly evaluated on the basis of at least three referee reports, and an electronic program committee meeting was held throughtheInternet.Theprogramcommitteeselected14researchcontributions. The topics covered by the selected papers include: combination of logics, com- bination of constraint solving techniques, combination of decision procedures, combination problems in verification, modular properties of theorem proving, integration of decision procedures and other solving processes into constraint programming and deduction systems. TheworkshopprogramwasenrichedbyfourinvitedtalksbyGregNelsonon “Foundations of a Constraint-Based Illustrator”, Alessandro Cimatti on “Inte- grating BDD-based and SAT-based Symbolic Model Checking”, Deepak Kapur on“ARewriteRulebasedFrameworkforCombiningDecisionProcedures”,and Tom F. Melham on “An Investigation into Software Architecture for Embedded Proof Engines”, and one tutorial by Thom Fruehwirth and Slim Abdennadher on “Reasoning with, about, and for Constraint Handling Rules”. IwouldliketothankthemanypeoplewhomadeFroCoS2002possible.Iam grateful to: the members of the program committee and the additional referees named on the following pages for reviewing the papers in a very short time and maintaining the very high standard of FroCoS workshops; the other members of theFroCoSSteeringCommitteefortheiradviceandencouragement;theinvited speakers;andlast,butbynomeansleast,SilvioRaniseforhandlingthesoftware for our web-based reviewing procedure and Luca Compagna for his help in the local organization of the workshop. January 2002 Alessandro Armando VI Organization Workshop Chair Alessandro Armando (DIST, University of Genova) Program Committee Alessandro Armando (U. Genova) Michael Kohlhase (CMU) David Basin (U. Freiburg) ChristopheRingeissen(LORIANancy) Frederic Benhamou (U. Nantes) Michael Rusinowitch (LORIA Nancy) Jacques Calmet (U. Karlsruhe) Klaus Schulz (LMU Mu¨nchen) Giorgio Delzanno (U. Genova) Roberto Sebastiani (U. Trento) Bernhard Gramlich (T.U. Wien) Cesare Tinelli (U. Iowa) Deepak Kapur (U. New Mexico) Luca Vigano` (U. Freiburg) H´el`ene Kirchner (LORIA Nancy) Frank Wolter (U. Leipzig) Local Organization Alessandro Armando Luca Compagna Silvio Ranise Additional Reviewers Rafael Accorsi Paolo Giorgini Julien Musset Marco Aiello Isabelle Gnaedig Silvio Ranise Alexander Bockmayr Fr´ed´eric Goualard Michel Rueher Chad E. Brown Laurent Granvilliers Luciano Serafini Walter A. Carnielli Timothy J Hickey Frieder Stolzenburg Luca Compagna Dieter Hutter Juergen Stuber Alessandro Coglio Franc¸ois Lamarche Ashish Tiwari Pasquale Delucia Steffen Lange Heinrich Wansing Eric Domenjoud Francisco Lopez-Fraguas Michael Zakharyaschev Hubert Dubois Michael Marte Hantao Zhang Chiara Ghidini Richard Mayr Silvio Ghilardi Eric Monfroy Sponsoring Institutions University of Genova Dipartimento di Informatica, Sistemistica e Telematica (DIST), University of Genova Table of Contents Foundations of a Constraint-Based Illustrator ......................... 1 Greg Nelson Integrating Hol-Casl into the Development Graph Manager Maya...... 2 Serge Autexier, Till Mossakowski Monads and Modularity ............................................ 18 Christoph Lu¨th, Neil Ghani A Modular Approach to Proving Confluence........................... 33 Michael Marte Integrating BDD-Based and SAT-Based Symbolic Model Checking ....... 49 Alessandro Cimatti, Enrico Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella Heuristics for Efficient Manipulation of Composite Constraints........... 57 Tuba Yavuz-Kahveci, Tevfik Bultan Constraint-Based Model Checking for Parameterized Synchronous Systems .............................. 72 Giorgio Delzanno A Rewrite Rule Based Framework for Combining Decision Procedures .... 87 Deepak Kapur Combining Sets with Integers........................................ 103 Calogero G. Zarba Solving Nonlinear Equations by Abstraction, Gaussian Elimination, and Interval Methods ............ 117 Martine Ceberio, Laurent Granvilliers A Generalization of Shostak’s Method for Combining Decision Procedures. 132 Clark W. Barrett, David L. Dill, Aaron Stump Combining Relational Algebra, SQL, and Constraint Programming ...... 147 Marco Cadoli, Toni Mancini Computational Complexity of Propositional Linear Temporal Logics Based on Qualitative Spatial or Temporal Reasoning ................... 162 Philippe Balbiani, Jean-Franc¸ois Condotta Exploiting Constraints for Domain Managing in CLP(FD) .............. 177 Marco Gavanelli, Evelina Lamma, Paola Mello, Michela Milano VIII Table of Contents Tutorial: Reasoning with, about and for Constraint Handling Rules ...... 192 Thom Fruehwirth, Slim Abdennadher Prosper. An Investigation into Software Architecture for Embedded Proof Engines ........................................ 193 T.F. Melham Constraint-Lambda Calculi.......................................... 207 Matthias H¨olzl, John N. Crossley Labelled Deduction over Algebras of Truth-Values...................... 222 Joa˜o Rasga, Am´ılcar Sernadas, Cristina Sernadas, Luca Vigano` A Temporal × Modal Approach to the Definability of Properties of Functions .......................... 239 Alfredo Burrieza, Inma P. de Guzma´n Author Index...................................................... 255 Foundations of a Constraint-Based Illustrator Greg Nelson COMPAQ Systems Research Center 130 Lytton Avenue, Palo Alto, CA 94301 Abstract. The talk describes some of the formal foundations of Juno- 2,aconstraint-basedgraphicalillustratorimplementedbyAllanHeydon and Greg Nelson and available over the web in source form. The first idea underlying Juno-2 is that constraint-based programming isobtainedfromordinaryimperativeprogrammingnotbyaddingafea- turebutbysubtractingarestriction:specificallybydroppingthelawof the excluded miracle from the calculus of guarded commands of Edsger W. Dijkstra. Dropping this law introduces “partial commands” (some- times called “miracles”), which, when combined with conventional local variable introductions (”VAR statements”) creates a highly principled constraintsolvingprimitivethatisbeautifullyorthogonaltotheconven- tional imperative features of the language. The second idea is that the “combination of decision procedures tech- nique”thathasbeenwidelyusedintheautomatictheorem-provingcom- munity for the last two decades can also be used to combine constraint solversfortwologicaltheoriesintoasingleconstraintsolverforthecom- binationofthetheories.Juno-2usesthisideatocombineasimplesolver forthetheoryofapairingfunction(whichamountsonlytoanimplemen- tationofunificationclosure)withasophisticatednumericalsolverforthe theory of the real numbers to produce a powerful constraint solver that is useful for producing accurate technical illustrations and animations. The talk will include a demonstration of Juno-2, weather permitting. References 1. Allan Heydon and Greg Nelson. The Juno-2 Contraint-based Drawing Editor. Re- searchReport131a.DigitalEquipmentCorporationSystemsResearchCenter,Palo Alto, CA 1994. 2. The Juno-2 Home Page. http://research.compaq.com/SRC/juno-2 3. Greg Nelson. Juno, A Constraint-based Graphics System. In Proceedings of the ACM Siggraph conference, pp 235–43, July 1985. 4. GregNelson. AGeneralizationofDijkstra’sCalculus.ACMTOPLAS11(4).Octo- ber 1989, pp 517–61. 5. Greg Nelson. Combining Satisfiability Pocedures by Equality-sharing. In “Au- tomatic Theorem Proving: after 25 years” edited by W. W. Bledsoe and D. W. Loveland. (vol 29 of “Contemporary Mathematics”) American Mathematical Soci- ety 1983. pp 201–11. A.Armando(Ed.):FroCoS2002,LNAI2309,p.1,2002. (cid:1)c Springer-VerlagBerlinHeidelberg2002 Integrating Hol-Casl into the Development Graph Manager Maya Serge Autexier1 and Till Mossakowski2 1 FR 6.2 Informatik, Saarland University, P.O. Box 15 11 50, D 66041 Saarbru¨cken, [email protected], Fax: +49 681 302 2235 2 BISS, University of Bremen, P.O. Box 330 440, D 28334 Bremen, [email protected], Fax: +49 421 218 3054 Abstract. FortherecentlydevelopedspecificationlanguageCasl,there exist two different kinds of proof support: While HOL-Casl has its strength in proofs about specifications in-the-small, Maya has been de- signed for management of proofs in (Casl) specifications in-the-large, within an evolutionary formal software development process involving changesofspecifications.Inthiswork,wediscussourintegrationofHOL- CaslandMayaintoapowerfulsystemprovidingtoolsupportforCasl, whichwillalsoserveasabasisfortheintegrationoffurtherprooftools. 1 Introduction The specification of large software systems is only manageable if specifications are built in a structured manner. Specification languages, like Casl [4], provide various mechanisms to combine basic specifications to structured specifications. Analogously, verification tools must be able to represent the logical content of specifications in a structured way. This needs to be more than the pure logical contentofthespecification,sincethestatus,provenoropen,ofproofobligations must be represented in order to keep the whole development in a consistent state. Attempts to prove some proof obligation may fail, revealing errors in the specification,whichissubsequentlychanged.Hencespecificationandverification of software are intertwined, until we finally obtain a version of the specification, whoseproofobligationscanallbeproved.Inpractice,itisindispensabletodeal in an efficient manner with the effects of correcting flaws in the specification. This is mainly to be able to determine which proofs remain valid, since a lot of proof effort, i.e. development time, has gone into creating those proofs. Industrial strength formal software development systems like VSE [9] have been designed to deal with the evolutionary character of the software develop- ment process. The main differences between those systems and usual theorem proversisontheonehandthattheyaccommodatetheneedtoprovidetoolsup- port to exploit the structure of specifications to ease their verification. On the otherhand,theyprovidetoolsupporttoadministratethestatusofthedevelop- ment. The development graph manager Maya [13,8] has been designed to make A.Armando(Ed.):FroCoS2002,LNAI2309,pp.2–17,2002. (cid:1)c Springer-VerlagBerlinHeidelberg2002