Maria Paola Bonacina Mark E. Stickel (Eds.) t f i r h c s t s e F 8 8 Automated Reasoning 7 7 I A and Mathematics N L Essays in Memory of William W. McCune 123 Lecture Notes in Artificial Intelligence 7788 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 Maria Paola Bonacina Mark E. Stickel (Eds.) Automated Reasoning and Mathematics Essays in Memory of William W. McCune 1 3 SeriesEditors RandyGoebel,UniversityofAlberta,Edmonton,Canada JörgSiekmann,UniversityofSaarland,Saarbrücken,Germany WolfgangWahlster,DFKIandUniversityofSaarland,Saarbrücken,Germany VolumeEditors MariaPaolaBonacina UniversitàdegliStudidiVerona,DipartimentodiInformatica StradaLeGrazie15,37134Verona,Italy E-mail:[email protected] MarkE.Stickel SRIInternational,ArtificialIntelligenceCenter 333RavenswoodAvenue,MenloPark,CA94025,USA E-mail:[email protected] ThepictureofWilliamW.McCuneonpageVwastakenfromthewebsite http://www.cs.unm.edu/mccune/photo.html. The cover illustration is licensed under the Creative Commons Attribution-Share Alike3.0UnitedStateslicense.Attribution:http://www.ForestWander.com ISSN0302-9743 e-ISSN1611-3349 ISBN978-3-642-36674-1 e-ISBN978-3-642-36675-8 DOI10.1007/978-3-642-36675-8 SpringerHeidelbergDordrechtLondonNewYork LibraryofCongressControlNumber:2013932090 CRSubjectClassification(1998):I.2.3,F.4.1-2,F.3.1 LNCSSublibrary:SL7–ArtificialIntelligence ©Springer-VerlagBerlinHeidelberg2013 Thisworkissubjecttocopyright.Allrightsarereserved,whetherthewholeorpartofthematerialis concerned,specificallytherightsoftranslation,reprinting,re-useofillustrations,recitation,broadcasting, reproductiononmicrofilmsorinanyotherway,andstorageindatabanks.Duplicationofthispublication orpartsthereofispermittedonlyundertheprovisionsoftheGermanCopyrightLawofSeptember9,1965, inistcurrentversion,andpermissionforusemustalwaysbeobtainedfromSpringer.Violationsareliable toprosecutionundertheGermanCopyrightLaw. Theuseofgeneraldescriptivenames,registerednames,trademarks,etc.inthispublicationdoesnotimply, evenintheabsenceofaspecificstatement,thatsuchnamesareexemptfromtherelevantprotectivelaws andregulationsandthereforefreeforgeneraluse. Typesetting:Camera-readybyauthor,dataconversionbyScientificPublishingServices,Chennai,India Printedonacid-freepaper SpringerispartofSpringerScience+BusinessMedia(www.springer.com) William W. McCune (1953–2011) Preface In Memory of William W. McCune (1953–2011) ThisvolumeisatributetothememoryofWilliam(Bill)McCune,whosesudden death on May 4, 2011, left the field of automated reasoning deprived of one of the founders of practical theorem proving and model building. While he was an accomplished computer scientist all around, Bill McCune was especially a fan- tastic system builder and software engineer. He developed a series of systems of astoundingpower,robustness,useability,andportability,including the theorem proversOtter,EQP,andProver9,theparallelproverROO,theproofcheckerIvy, the prototype SAT-solver ANL-DP, and the model builders Mace2 and Mace4. Bill McCune’s Scientific and Professional Contributions Originary of New Hampshire, Bill did his undergraduate studies in mathemat- ics at the University of Vermont, and completed his education with an MS and a PhD in computer science from Northwestern University, with adviser Larry Henschen. After the PhD, he started his career as Assistant Computer Scien- tist at the Mathematics and Computer Science (MCS) Division of the Argonne National Laboratory (ANL), at Argonne, near Chicago. He was soon promoted to Computer Scientist, and later became Senior Computer Scientist. Bill spent most of his professional life in the red-brick building hosting the MCS Division onthevastandquietANLcampus.Hestayedthereuntiltheunexpecteddemise ofthe automatedreasoningprogramin2006,whenhe joinedthe Departmentof Computer Science of the University of New Mexico as Research Professor. ANLisaresearchlaboratorymostlyfundedbythefederalgovernmentofthe United States throughits Department ofEnergy.A primarymissionof its MCS Division is to advance research in computing and mathematics to enable the solving of the mathematical and computational challenges posed by research in physics and other natural sciences. Perhaps surprisingly, and due in part to the lack of specialization in the early days of computer science, Argonne, was, and still remains from a historic point of view, the cradle of automated reasoning. J.AlanRobinsonworkedonresolutionandunificationduringsummerjobsatAr- gonne during 1962–1964,writing the milestone article on “A Machine-Oriented Logic” in the summer of 1963. Approximately in the same years, Larry Wos started at ANL a research program in automated reasoning, where paramod- ulation, or resolution with equality built-in, demodulation, or the ad hoc use of equations for rewriting, and the set of support strategy were invented in the years 1965–1969. Work on automated reasoning at Argonne continued during the1970sandearly1980s.WhenBillMcCunestartedatANLin1984,hejoined Larry Wos, Ewing L. (Rusty) Lusk, and Ross Overbeek. The Argonne theorem proversinthatperiodwereITP,LMA/ITP,andAURA,whichalreadyfeatured an early version of the given-clause algorithm later popularized by Otter. VIII Preface A positive consequence of Argonne’s great inventions was the persuasion that time was ripe to focus on implementation and system building. A less pos- itive one was the notion that research in theory was almost over. In reality, in the mid-1980s the quest for building equality into resolution was not over. The Wos–Robinson conjecture,namely,whetherparamodulationiscompletewithout paramodulatingintovariablesandaddinginstancesofreflexivity–thefunction- ally reflexive axioms – was not settled. Also, it was not known how to control the termination of demodulation, that was called k-demodulation, because it depended on an ad hoc bound k on the number of allowed rewriting steps. In the same years when Larry Wos and G. Robinson invented paramodula- tion, Don Knuth and his student Peter B. Bendix devised a completion proce- dure, featuring superposition, or paramodulation between the left sides of two rewrite rules, and simplification of a rewrite rule by another. A key idea was that equations were oriented into rewrite rules by a well-founded ordering on terms. In 1981, G´erard Huet proved that Knuth–Bendix completion is correct: if it does not fail by generating an equation that cannot be oriented, it gener- ates in the limit a confluent rewriting system, and it semi-decides the validity of equationaltheorems,as suggestedindependently also by Dallas Lankford. At the IEEE Symposium on Logic in Computer Science (LICS) of 1986,Leo Bach- mair, Nachum Dershowitz, and Jieh Hsiang reobtained these results in a more general framework based on well-founded proof orderings. At the 8th Interna- tional Conference on Automated Deduction (CADE-8), held at Oxford in July 1986, Jieh Hsiang and Micha¨el Rusinowitch showed that ordered resolution and ordered paramodulation, restrictedbyawell-foundedordering,arerefutationally complete without functionally reflexive axioms. During 1987–1989, Jieh Hsiang andMicha¨elRusinowitch,ononehand,andLeoBachmair,NachumDershowitz, and David A. Plaisted, on the other, came up independently with unfailing, or ordered, completion, which works for equations with no need of orienting them once and for all into rewrite rules. Throughout the 1980s, Nachum Dershowitz, David A. Plaisted, and others workedsystematically on well-founded orderings, their properties, and termination of rewriting for theorem proving. Bill McCune’s greatness at that time was that he deeply understood the rewriting and completion research developed elsewhere, and united it with the best results of the Argonne tradition in a new theorem prover named Otter. Otterstandsfororganized techniques for theorem-proving and effective research, and it is also the name of a rare semiaquatic mammal, that inhabits rivers and unites a playful, shy nature with the determination of a skilled hunter. The release of Otter at CADE-9 in 1988 was a turning point in the history of automatedreasoning.Never before had the computer science community seena theoremproverofsuchawesomepower.Otterprovedtheoremsinfullfirst-order logic with equality with amazing speed, relative to the technology of the day. It was almost surely sound,1 and endowed with both complete and incomplete 1 Though Bill used to joke that he would not jump off a bridge if a soundness bug were exposed in Otter or any otherof his systems. Preface IX strategies, with the latter often most useful in practice. Otter quickly became the touchstone for an entire field. Alreadyintheearly1990s,Ottermaturedintoarobust,reliable,andportable prover, with options and parameters that the experimenter could set to define the adoptedstrategy.Overtime,Billaddedfeaturessuchasthepick-given ratio to mix clause evaluation functions, hints and a hot list to guide the search, and an auto(matic) mode enabling the prover to choose by itself the strategy based on the input’s syntax. Several of these enhancements came from Bill’s readinesstolearnfromexperiments,includingthosecarriedoutbyothers,andto integrateusers’suggestionsorrequestswithhisownapparentlyinfalliblesenseof what was practical to implement. Notwithstanding its wealth of features, Otter was remarkably easy to use, and therefore a significant user community grew world-wide, including scientists not working in theorem proving, and especially mathematicians and logicians. Indeed, Larry Wos and Bill McCune shared a keen interest in applying theorem proving to mathematics, especially algebra, geometry,andlogic,alsobuildingonhistorictiesthattheMCSDivisionofANL had with the Department of Mathematics of the University of Chicago. However, perhaps Otter’s greatest impact was due to Bill’s generous and far-looking decision to make its source code publicly available. It is impossible to describe completely a reasoning programin research papers. There is always some amount of knowledge, often a surprising amount, that is written only in thecode,andthereforeremainshidden,ifthecodeisnotpublicoristoohardto read. Bill’s code was admirably readable and well organized. Other researchers, including those whose systems eventually overtook Otter in speed or in variety of inference rules, also learnt from Bill’s code data structures, algorithms, and indexing schemes, which are fundamental for implementing theorem provers. Although Bill developed Otter for several years, he had a clear sense that it maynotbe wise to try to puttoo many featuresin onesystem.For instance,he refused to implement in Otter reasoning modulo associativity and commutativ- ity (AC). Rather, he built another theorem prover, called EQP, for equational prover, that had AC-matching and AC-unification, but worked only for equa- tionaltheories.BillalwaysconsideredEQPasaprototypetobe usedbyhimself andafewothers,ratherthanasystemforalllikeOtter.EQPwaswrittenwitha specific goalinmind: provingtheRobbins conjecture,anopenprobleminmath- ematics whose existence Larry Wos had discovered in his continuous quest for challenges for theorem provers. The Robbins conjecture dated back to 1933, when a mathematician, named E. V. Huntington, demonstrated by hand that a certain equation, later called Huntingtonaxiom,wassufficient,togetherwithassociativityandcommutativity of addition, to axiomatize Boolean algebra. In the same year, another math- ematician, Herbert Robbins, conjectured that the same was true of another equation, later called Robbins axiom. A proof was not found, and algebras pre- sented by Robbins axiom, together with associativity and commutativity of ad- dition, became known as Robbins algebras. In 1990-1992, S. Winker proposed two equations, later called first Winker condition and second Winker condition, X Preface and proved by hand that if each of them is added to the Robbins axiom, the Huntington axiom follows. This led to decomposing the problem into proving that Robbins axiom implies the second Winker condition, the second Winker condition implies the first, and the first implies Huntington axiom. While the first step was relatively easy, the other two remained beyond the possibilities of theorem provers. In 1996, EQP proved them both, thereby solving a problem that had chal- lengedmathematiciansforover60years.Thefirstsuccessfulrunforthe hardest lemma, the one showing that the second Winker condition implies the first, in February 1996, took an impressive 12.5 days of computation on a 486DX2/66. The experimentwas repeatedon anRS/6000taking 7.2days.In the same year, BillalsosucceededinhavingEQPprovethatRobbinsaxiomimpliesHuntington axiominonerun,inordertohaveasinglemechanicalproof.Ahumanversionof the proofwasextractedfromthe mechanicalone forreadabilityandpersuasion. The field reacted with awe, and this momentous achievement brought unprece- dented visibility to automated deduction, artificial intelligence, and the whole of computer science. Bill McCune and EQP made it onto the pages of the New York Times. One of the very early dreams of artificial intelligence, namely, ma- chines capableofprovingmathematicaltheoremsthat humanexperts couldnot prove, was no longer only a dream: it was a reality. The Robbins algebra proof is an ideal example of a successful blending of multiple strands of research in automated reasoning: the extensive experimentation characteristic of Argonne, new theory about equality reasoning, and associative-commutative unification. While obtaining these outstanding results in theorem proving, Bill was also among the first to understand the importance of the dual problem of model building, or theorem disproving. A precipitating event was the solution of open problems of quasigroup existence in 1992. The problems were posed by mathe- matician Frank Bennett, and solved initially by Masayuki Fujita, with ICOT’s Model Generation Theorem Prover (MGTP), and by John Slaney, with his model builder FINDER. The opportunity and excitement of solving open prob- lems stimulated a lot of activity by researchers, including the second editor of this volume, Hantao Zhang, and Bill McCune, on new, advanced implemen- tations of the Davis–Putnam–Loveland–Logemann (DPLL) procedure, known since 1960-1962, to decide propositional satisfiability (SAT), and find models. A Japanese–AmericanWorkshop on Automated Theorem Proving that focused on finite domain theorem proving was held at Duke University in March 1994. Frank Bennett, Masayuki Fujita, Bill McCune, Hantao Zhang, and the second editor of this volume, were among the attendees. A few months later, in June 1994,Bill McCune announced his DPLL-based SAT-solver ANL-DP, which was already being applied to solving quasigroup existence problems. Billwastoo involvedwith first-orderreasoningto delve into SAT, andANL- DP remained a prototype. Since DPLL works by trying to build a model, and reportsunsatisfiabilitywhenithasfoundthatnoneexists,ANL-DPwasprepara- tory work for Bill’s next great system, the SAT-based finite model finder Mace, whose most successful version was Mace2. The mathematical community that Preface XI Bill supported benefited enormously from his providing a model builder as well as a theorem prover. As we shall see, several chapters of this volume report results that depend on both. For all these achievements, in 2000 Bill McCune receivedthe HerbrandAward,thehighesthonorinautomatedreasoningandone of the highest in computer science. Bill McCune was not the kind who would rest on his laurels. Although he maintained Otter through August 2003,which is the date of that glorioustheo- rem prover’s last manual, Bill knew that Otter had become too old to continue developing it. Thus, he embarked in designing a brand new theorem prover for first-order logic with equality, called Prover9, and with the ever-optimistic, forward-looking subtitle “the future of theorem proving.” The years 2005–2010 were devoted to Prover9 and Mace4, a new Mace, no longer SAT-based, but using a more general constraint solving approach.Prover9and Mace4 inherited all the great qualities of their predecessors Otter and Mace2, as witnessed by the fact that they are still very much in use today. Not only was Bill McCune a marvelous system builder, he also wanted to make it easy for others to build reasoning programs. In addition to making his owncode available,alreadyin1992–1993,he hadthe ideaofbuilding a software library to assemble theorem provers. The version dating from those years was named OPS, for Otter parts store. Later it evolved into a new library, called LADR, or Library for Automated Deduction Research. Bill was probably also the first to think ofa web-basedinterface to let anyoneplay with anautomated reasoner:SonofBirdBraingaveaccesstoOtterandMace2,andSonofBirdBrain II gave access to Prover9 and Mace4. Since he worked for most of his career in a research laboratory, Bill did not have PhD students. However, he mentored through cooperation several junior colleagues. Also, he served the scientific community as the first Secretary of the Association for Automated Reasoning (AAR) in 1986–1993,as co-organizer of CADE-9 at Argonne in 1988, as Program Chair of CADE-14 in Townsville, Australia, in 1997, and as Trustee of CADE Inc. in 1997–2000. Bill McCune was remembered with heart-felt speeches by several colleagues at CADE-23 in Wroc(cid:3)law, Poland, in August 2011, and at the 8th International Workshop on First-Order Theorem Proving (FTP) in Bern, Switzerland, in July 2011. Some Recollections of Bill McCune by Maria Paola Bonacina It is likely that my first interaction with Bill was by e-mail, when he was AAR Secretary, I was a graduate student, and I wanted to become a member of the AAR. As part of my PhD work at SUNY Stony Brook, I implemented a dis- tributed version of Otter, called Aquarius, later presented at the Third Inter- national Symposium on Design and Implementation of Symbolic Computation Systems (DISCO),inGmunden, Austria,inSeptember 1993.The availabilityof Bill’s code helped the implementation part of my thesis enormously. It meant that I could focus on implementing the methodology for distributed deduction that I was proposing in the thesis, called clause diffusion, reusing Bill’s code for everything else. It was my first opportunity to appreciate the clarity and robustness of his code. Also, Bill’s turn-around time by e-mail was fantastic.