Lecture Notes in Artificial Intelligence 7362 Subseries of Lecture Notes in Computer Science LNAISeriesEditors RandyGoebel UniversityofAlberta,Edmonton,Canada YuzuruTanaka HokkaidoUniversity,Sapporo,Japan WolfgangWahlster DFKIandSaarlandUniversity,Saarbrücken,Germany LNAIFoundingSeriesEditor JoergSiekmann DFKIandSaarlandUniversity,Saarbrücken,Germany Johan Jeuring John A. Campbell Jacques Carette Gabriel Dos Reis Petr Sojka Makarius Wenzel Volker Sorge (Eds.) Intelligent Computer Mathematics 11th International Conference,AISC 2012 19th Symposium, Calculemus 2012 5th International Workshop, DML 2012 11th International Conference, MKM 2012 Systems and Projects, Held as Part of CICM 2012 Bremen, Germany, July 8-13, 2012, Proceedings 1 3 SeriesEditors RandyGoebel,UniversityofAlberta,Edmonton,Canada JörgSiekmann,UniversityofSaarland,Saarbrücken,Germany WolfgangWahlster,DFKIandUniversityofSaarland,Saarbrücken,Germany VolumeEditors JohanJeuring UtrechtUniversity,TheNetherlands,E-mail:[email protected] JohnA.Campbell UniversityCollegeLondon,UK,E-mail:[email protected] JacquesCarette McMasterUniversity,Hamilton,ON,Canada,E-mail:[email protected] GabrielDosReis TexasA&MUniversity,CollegeStation,TX,USA,E-mail:[email protected] PetrSojka MasarykUniversity,Brno,CzechRepublic,E-mail:sojka@fi.muni.cz MakariusWenzel UniversitédeParis-Sud,OrsayCedex,France,E-mail:[email protected] VolkerSorge TheUniversityofBirmingham,UK,E-mail:[email protected] ISSN0302-9743 e-ISSN1611-3349 ISBN978-3-642-31373-8 e-ISBN978-3-642-31374-5 DOI10.1007/978-3-642-31374-5 SpringerHeidelbergDordrechtLondonNewYork LibraryofCongressControlNumber:2012940388 CRSubjectClassification(1998):I.1,F.4.1,I.2.2-3,I.2.6,I.2,F.3.1,D.2.4,F.3,H.3.7, H.3,G.4,H.2.8 LNCSSublibrary:SL7–ArtificialIntelligence ©Springer-VerlagBerlinHeidelberg2012 Thisworkissubjecttocopyright.Allrightsarereserved,whetherthewholeorpartofthematerialis concerned,specificallytherightsoftranslation,reprinting,re-useofillustrations,recitation,broadcasting, reproductiononmicrofilmsorinanyotherway,andstorageindatabanks.Duplicationofthispublication orpartsthereofispermittedonlyundertheprovisionsoftheGermanCopyrightLawofSeptember9,1965, initscurrentversion,andpermissionforusemustalwaysbeobtainedfromSpringer.Violationsareliable toprosecutionundertheGermanCopyrightLaw. Theuseofgeneraldescriptivenames,registerednames,trademarks,etc.inthispublicationdoesnotimply, evenintheabsenceofaspecificstatement,thatsuchnamesareexemptfromtherelevantprotectivelaws andregulationsandthereforefreeforgeneraluse. Typesetting:Camera-readybyauthor,dataconversionbyScientificPublishingServices,Chennai,India Printedonacid-freepaper SpringerispartofSpringerScience+BusinessMedia(www.springer.com) Preface As computers and communications technology advance, greater opportunities arise for intelligent mathematical computation. While computer algebra, auto- mateddeduction,mathematicalpublishingandnoveluserinterfacesindividually have long and successful histories, we are now seeing increasing opportunities for synergy among these areas. The series of Conferences on Intelligent Com- puter Mathematics (CICM) hosts collections of co-located meetings, allowing researchersandpractitionersactiveinthese relatedareastosharerecentresults and identify the next challenges. The fifth in this series of Conferences on Intelligent Computer Mathematics was held in Bremen, Germany, in 2012. Previous conferences, all also published in Springer’s Lecture Notes in Artificial Intelligence series, were held in the UK (Birmingham, 2008: LNAI 5144), Canada (Grand Bend, Ontario, 2009: LNAI 5625),France(Paris,2010:LNAI6167)andItaly(Bertinoro,2011:LNAI6824). CICM 2012 included four long-standing international meetings: – 11th International Conference on Mathematical Knowledge Management (MKM 2012) – 19th Symposium on the Integration of Symbolic Computation and Mecha- nized Reasoning (Calculemus 2012) – 11th International Conference on Artificial Intelligence and Symbolic Com- putation (AISC 2012) – 5th Workshop/Conference on Digital Mathematics Libraries (DML 2012) Since2011,CICMalsooffersatrackforbriefdescriptionsofsystemsandprojects that span the MKM, Calculemus, AISC, and DML topics, the “Systems and Projects” track. The proceedings of the four international meetings and the Systems and Projects track are collected in this volume. CICM 2012 also contained the following activities: – Demonstrations of the systems presented in the Systems and Projects track – Less formal “work in progress” sessions We used the “multi-track” features of the EasyChair system, and our thanks are due to Andrei Voronkov and his team for this and many other features. Themulti-trackfeaturealsoallowedtransparenthandlingofconflictsofinterest between the Track Chairs and submissions: these submissions were moved to a separatetrackoverseenbytheGeneralChair.Therewere60submissions,eightof whichwerewithdrawn.Eachofthe remaining52submissionwasreviewedbyat least two, and on average three, ProgramCommittee members. The committee decidedtoaccept38papers.However,thisisaconflationoftrackswithdifferent acceptance characteristics.The track-basedacceptance rates were: VI Preface MKM 13 acceptances out of 19 submissions Calculemus6 acceptances out of 9 submissions AISC 6 acceptances out of 8 submissions DML 2 acceptances out of 3 submissions S & P 11 acceptances out of 12 submissions One paper was not submitted to a particular track, and was rejected. Threeinvitedtalksweregiven.ThefirstonewasbyConorMcBridefromthe Department of Computer and Information Sciences, University of Strathclyde, and was entitled “A Prospection for Reflection”: Go¨del’s incompleteness theorems tell us that there are effective limita- tions on the capacity of logicalsystems to admit reasoning about them- selves.However,therearesolidpragmaticreasonsforwantingtotry:we can benefit considerably by demonstrating that systematic patterns of reasoning (and programming,of course) are admissible. It is very useful to treatgoalsas data inorderto attackthem with computation,adding certified automation to interactive proof tools, delivering the efficiency required to solve compute-intensive problems with no loss of trust. Dependent type theory provides a ready means of reflection: goals be- come types, and types may be computed from data. This technique has proven highly successful when tightly targeted on specific problem do- mains. But we may yet ask the bold question of how large a universe of problems we can effectively reflect: how much of our type theory can we encode within its own notion of data? To what extent can our type theory capture its own typing discipline? Might we construct a hierar- chy of type theories where the whole of each lower levelcan be reflected at higher levels? In this talk, I shall outline grounds for modest opti- mism and propose a plan of campaign. The obstacles may turn out to be as fascinating as the objective. The reward, if we can reach it, is a flexible technologyfor certified automationin problem-solving,honestly articulating what at least computers can do. The second invited talk was by Cezar Ionescu from the Potsdam Institute for Climate Impact Research, on “Increasingly Correct Scientific Programming”: Dependently typed languages promise an elegant environment for pro- grammingfromspecifications:the propertiesthataprogramshouldsat- isfyareexpressedaslogicalformulasandencodedviatheCurry–Howard isomorphismasatype,acandidateimplementationshouldbeamember ofthistype,andthetypecheckerverifieswhetherthisisindeedthecase. But sometimes the type checker demands “too much”: in particular, in scientificprogramming,itoftenseemsthatonemustformalizeallofreal analysis before writing a single line of useful code. Alternatively, one can use mechanisms provided by the language in order to circumvent the type checker,andconfirmthat“realprogrammerscanwriteFortran in any language.” We present an example of navigating between these Preface VII extremes in the case of economic modeling. First, we use postulates in ordertobe abletoreusecode,andachieveakindofconditionalcorrect- ness (for example, we can find a Walrasianequilibrium if we are able to solve a convex optimization problem). We then remove more and more of the postulates, replacing them with proofs of correctness, by using interval arithmetic methods. Finally, Yannis Haralambous, D´epartement Informatique, T´el´ecom Bretagne, gave a talk on “Text Mining Methods Applied to Mathematical Texts.” April 2012 Johan Jeuring John A. Campbell Jacques Carette Gabriel Dos Reis Petr Sojka Makarius Wenzel Volker Sorge Organization CICM 2012 was organized by the Conference on Intelligent Computer Mathe- maticsSteeringCommittee,whichwasformedatCICM2010asaparentbodyto the long-standing Calculemus and Mathematical Knowledge Management spe- cialinterestgroups.Theconferencesorganizedbytheseinterestgroupscontinue as special tracks in the CICM conference. The AISC conference, which is only organized every other year, and DML workshop were organized in 2012 too. Thesetracksandthe Systems andProjectstrackhadindependent TrackChairs andProgramCommittees.Localarrangements,the life-bloodofanyconference, were handled by the Department of Computer Science of the Jacobs University Bremen, Germany, and DFKI, Bremen, Germany. CICM Steering Committee Secretary Michael Kohlhase Jacobs University Bremen, Germany Calculemus Delegate Renaud Rioboo ENSIIE, France Treasurer William Farmer McMaster University, Canada DML Delegate Thierry Bouche Universit´e Joseph Fourier Grenoble, France CICM PC Chair 2011 James Davenport University of Bath, UK CICM PC Chair 2012 Johan Jeuring Utrecht University and Open University, The Netherlands MKM Trustees Serge Autexier Florian Rabe Alan Sexton James Davenport Claudio Sacerdoti Coen Makarius Wenzel Patrick Ion (Treasurer) X Organization Calculemus Trustees David Delahaye Paul Jackson Stephen Watt Gabriel Dos Reis Renaud Rioboo Makarius Wenzel William Farmer Volker Sorge AISC Steering Committee Serge Autexier John Campbell Eugenio Roanes-Lozano Jacques Calmet Jacques Carette Volker Sorge CICM 2012 Officers General Program Chair Johan Jeuring Utrecht University and Open University, The Netherlands Local Arrangements Michael Kohlhase Jacobs University Bremen, Germany Serge Autexier DFKI, Germany MKM Track Chair Makarius Wenzel LRI, Paris Sud, France Calculemus Track Chair Gabriel Dos Reis Texas A&M University, USA AISC Track CoChairs John A. Campbell University College London, UK Jacques Carette McMaster University, Canada DML Track Chair Petr Sojka Masaryk University Brno, Czech Republic S & P Track Chair Volker Sorge University of Birmingham, UK Organization XI Program Committee Mathematical Knowledge Management David Aspinall University of Edinburgh, UK Jeremy Avigad Carnegie Mellon University, USA Mateja Jamnik University of Cambridge, UK Cezary Kaliszyk University of Tsukuba, Japan Manfred Kerber University of Birmingham, UK Christoph Lu¨th DFKI, Germany Adam Naumowicz University of Bia(cid:4)lystok, Poland Jim Pitman University of California at Berkeley, USA Pedro Quaresma University of Coimbra, Portugal Florian Rabe Jacobs University Bremen, Germany Claudio Sacerdoti Coen University of Bologna, Italy Enrico Tassi INRIA Saclay, France Makarius Wenzel LRI, Paris Sud, France Freek Wiedijk Radboud University Nijmegen, The Netherlands Program Committee Calculemus Andrea Asperti University of Bologna, Italy Laurent Bernardin Maplesoft, Canada James H. Davenport University of Bath, UK Gabriel Dos Reis Texas A&M University, USA Ruben Gamboa University of Wyoming, USA Mark Giesbrecht University of Waterloo, Canada Sumit Gulwani Microsoft Research, USA John Harrison Intel Corporation,USA Joris van der Hoeven CNRS, Ecole Polytechnique, France Hoon Hong North Carolina State University, USA Lo¨ıc Pottier INRIA Sophia-Antipolis, France Wolfgang Windsteiger RISC Linz, Johannes Kepler University, Austria Program Committee Artificial Intelligence and Symbolic Computation Serge Autexier DFKI, Germany Jacques Calmet Karlsruhe Institute of Technology, Germany John Campbell University College London, UK Jacques Carette McMaster University, Canada Simon Colton Imperial College London, UK Jacques Fleuriot University of Edinburgh, UK