QED Workshop II Warsaw, July 20 - 22, 1995 Here are some of the statements of interest that I asked for a while back. I hope this will help us to introduce ourselves to one another. Roman Matuszewski ___________________________________________________________________________ Bob Boyer (boyer@cli.com) --- ----- For over 20 years, Robert S. Boyer has worked on Nqthm, also known as the Boyer-Moore Prover, which has been described in a number of books and articles. See for example the book "A Computational Logic Handbook", Boyer and Moore, Academic Press, 1988. At least 10 megabytes of machine checker user input to this system are available. Nqthm may be obtained by anonymous ftp from ftp.cli.com in /pub/nqthm/nqthm-1992/. The most recent release was in January, 1994. It is Boyer's view that while a sufficient number of mathematicians and computer scientists are sufficiently in favor of the QED project to build it in the next century or two, hopes for much progress on it at the current time are currently dim because of sociological and political problems. There is currently at least some funding, and certainly reasonable opportunities for publication (which leads to scientific status, including tenure) for work on new ways of trying to do automated reasoning and, of course, for new mathematics. But he fears that there is very little funding or publication opportunity for the cooperative building of up an extremely large proof-checked edifice. Thus, Boyer's highest personal hope for the QED workshop is some insight into how to overcome these sociological and political problems, to establish practical, personal motivation for large scale cooperation on this endeavor. ___________________________________________________________________________ Bill McCune (mccune@mcs.anl.gov) ---- ------ My background is computer science, and my main interest is automated discovery of proofs. My recent work has been in first-order logic (with equality) with Otter, a resolution/paramodulation theorem prover, applying it to problems in mathematics and logic. I have also been working with programs that search for small models of first-order statements. Since the first QED workshop at Argonne, we have given Otter the capability of building detailed "proof objects" representing the proofs it finds, and we have written a simple, independent program (in the Boyer-Moore logic) that checks the proof objects. (The proof checker has not been formally verified.) ___________________________________________________________________________ Bernd,Ingo Dahn (dahn@mathematik.hu-berlin.de) ----- ---- ---- The Special Interest of the ILF Group in the QED Project My group is a group of 3 mathematicians - especially trained in Mathematical Logic - working at the Institute of Pure Mathematics at the Humboldt University at Berlin in a Project "Integration of Logical Functions" supported by the Deutsche Forschungsgemeinschaft within the so-called "Schwerpunktprogramm Deduktion". The main objective of the group is to make the possibilities of theorem provers available to specialists working in other fields We have concentrated on integrating - automated theorem provers - interactive theorem provers - proof tactics - models in a system named ILF (Integrating Logical Functions) running on SUN Sparc stations. Currently, we are working with a configuration of the system - named ProofPad - that integrates the automated provers OTTER, (Argonne Nat. Lab.), SETHEO (TU Munich), DISCOUNT (Univ. Kaiserslautern) KoMeT (TU Darmstadt) and domain specific methods within a graphical user interface. The automated systems work as background processes (similar to an online spell checker) without requiring knowledge of automated theorem proving techniques from the user. Experiments have been made with proofs in the fields of lattice ordered groups and of verification of communication protocols. The group is preparing a mail server that takes block structured and model elimination proofs as input and returns natural language proof presentations as LaTeX source. ___________________________________________________________________________ Rajeev Gore (rpg@cisr.anu.edu.au) ------ ---- I am attending as a representative of the Automated Reasoning Project based at the Australian National University in Canberra Australia. Our early work was in the formalisation and implementation of theorem provers for relevant logics resulting in the propositional relevant logic prover called KRIPKE. Our current research is aimed at using problem specific semantic information to guide theorem provers as espoused in the prover SCOTT (Semantically Constrained Otter). SCOTT has been used to discover new theorems about finite groups. Although both of these provers are fully automatic, their domain of applicability is limited. We are therefore very keen to broaden our horizons by joining the QED community and keeping abreast of the international developments in this field. My personal interest in the QED project stems from the belief that currently available systems for formal mathematics are too arcane to be of general use to mathematicians or engineers. One should not need a PhD in this field to be able to use such systems. ___________________________________________________________________________ John Harrison (John.Harrison@cl.cam.ac.uk) ---- -------- I'm a final-year PhD student at the University of Cambridge Computer Laboratory, supervised by Mike Gordon. My research topic is computer-aided verification (floating-point hardware etc.) but my work on formalizing real analysis in HOL, which started as a mere theoretical adjunct, has led me to have some experience of, and considerable interest in, computer-checked mathematics. The proposals for using proof theory to link systems together is interesting, and worth pursuing. However in the short term, it seems to me that a more useful goal is to actually do formalized mathematics, picking areas which will reveal the strengths and weaknesses of different foundational systems, methods of proof support etc. We could also investigate quite direct interpretations of one logic in another (e.g. I'm sure HOL's logic has a straightforward interpretation in MIZAR's set theory), without worrying too much about proof theory. Linking in automated provers an/or computer algebra systems to help make proofs easier is another interesting topic. ______________________________________________________________________ Randall Holmes (holmes@math.idbsu.edu) ------- ------ I (Randall Holmes) have been developing an equational theorem prover for several years. This explains my interest in QED, I think; I view this kind of work as both an application of the prover and an opportunity to test its applicability to more "practical" problems. Attendance at the first QED workshop convinced me of the importance of work on interfaces between theorem proving systems; I think that the development and use of standards supporting such interfaces might be almost enough to cause QED to come about on its own (?). ___________________________________________________________________________ Paul Jackson (jackson@cs.cornell.edu) ---- ------- My interest in the QED project stems from my work over the last four years in creating tactics and theories for the Nuprl proof development system. This work includes: 1. implementing tactics for rewriting, chaining, induction, arithmetic reasoning and type checking. 2. Developing abstract algebra. Most recently, I developed some factorization theory for abelian cancellation monoids and am currently working on multivariate polynomials. ___________________________________________________________________________ Deepak Kapur (kapur@cs.albany.edu) ------ ----- I have been interested in constructive aspects of commutative algebra and automated theorem proving over the last 10 years. I got interested in algorithmic aspects of commutative algebra because of my interest in understanding rewrite-based approach to automated reasoning when I stumbled into the Groebner basis algorithm. I started investigating relationship between the Knuth-Bendix completion procedure and the Groebner basis algorithm, and have extended the Groebner basis algorithm to work on other structures. I also developed an algebraic approach for automated theorem proving in first-order predicate calculus. My current interest is in elimination algorithms for solving nonlinear polynomial equations. I have also been working on developing heuristics for automating proofs by induction. I have also been interested in understanding the interplay between algorithmic techniques used in commutative algebra and automated reasoning, in particular studying how to design an environment which facilitates algebraic reasoning, inductive reasoning and logical reasoning. I think such an environment would be useful for supporting mathematical reasoning and the QED project. ___________________________________________________________________________ Roman Matuszewski (romat@plearn.edu.pl) ----- ----------- My background is in aircraft and energy engineering. I am employed at the Department of Logic, Warsaw University in Bialystok. My main interest is how to cope with a large body of mechanically proof- checked encyclopedia of mathematics. I have been working in the Mizar Project since its beginning in 1973. My present work consists in editing the journal "Formalized Mathematics - a computer assisted approach" which is a report of mizared and formally checked mathematics. I am also working in mechanical translation from Mizar into natural language. English version is realized now in ,,Forma- lized Mathematics". I perceive the QED Project as a beginning of a wide international effort to construct mechanically proof-checked mathematical encyclopedia. ___________________________________________________________________________ Bill Pase (bill@ora.on.ca) ---- ---- I have been involved in the design and development of the NEVER theorem prover and the EVES verification system for over a decade. My interests have centered upon the formalization of specifications and the development of automated support for the proofs of properties about those specifications. Most specifications of interesting properties, are written in terms of an underlying mathematical theory. Example theories are those for integers, arrays, sets, sequences, and graphs. Whenever a specification requires such a theory, it must be studied and developed for EVES with heuristics for the NEVER theorem prover. To do this requires finding a formalization of the mathematical theory upon which to build. The QED project presents the possibility of there existing a standardized library of formalized mathematics. These theories could be used as a basis for the specialized theories required. Furthermore, the existence of the QED libraries would result in a common framework for the discussion of mathematical concepts. Thus, when set theory is required as part of a specification, the reference would be to the QED formalization of set theory. This will greatly reduce the difficulty of general dialog on mathematics and the attack upon mathematical problems by multiple theorem provers. ______________________________________________________________________ Rein Prank (prank@cs.ut.ee) ---- ----- Since 1987 I have worked on the use of computers by teaching Mathematical Logic. We have written our own software for the exercises of the main course of ML: truth-tables, formula manipulation, Turing Machines, proofs in Propositional Calculus, Predicate Calculus, Formal Arithmetic, First Order Theories. The next question after teaching the students understand the proofs is: how far stands this formal game from the proofs in real mathematics. I hope that the project like QED helps to understand it better but also to understand how to formulate formal systems and design the computer programs for easier real work. ___________________________________________________________________________ Piotr Rudnicki (piotr@cs.ualberta.ca) ----- -------- I have been in the Mizar project since its beginning. The goals of the Mizar project overlap with the goals of QED. I believe that the QED project is feasible, what more I am convined it is inevitable. Most of my recent work is in contributing to the Mizar data base by formalizing various fragments of mathematics and computing science. At this stage of developing Mizar it is most important to formalize a substantial amount of mathematics in it. Mizar's evolution is driven by such formalizations. ______________________________________________________________________ Herbert Stoyan (Herbert.Stoyan@informatik.uni-erlangen.de) ------- ------ Wolfgang Jaksch (Wolfgang.Jaksch@informatik.uni-erlangen.de) -------- ------ Claus Zinn (Claus.Zinn@informatik.uni-erlangen.de) ----- ---- To facilitate the application of AI in mathematics H.Stoyan founded the FERMAT project. The FERMAT project is concerned in the specification and implementation of a system which supports mathematicians in their activities (and its content is thus very close to QED aims). Our project is still in its very early steps. Actually, we are interested in identifying mathematical activities, analyzing and describing them and the possibilities to support them mechanically. An application area for AI has to have a firm conceptual basis formulated in a scientific language. Application areas without such an area (f.ex. common sense) are doomed to fail. To prove the feasibility of AI mathematics with its excellent system of concepts is a outstanding example. Our research team (Prof. Stoyan, 2 full-time researchers and a PhD-Student with partial funding) approach FERMAT in mainly three directions: o Mathematical Proving (by humans) (basically, C.Zinn) o Discovering mathematical entities (basically, S.Jacob) o Hypertexting mathematical texts (basically, W.Jaksch) We're interested in the following issues: - Identify major mathematical activities - Identify which of these activities may be subject to mechanization or supported by computer - Identify how such mechanization/support can be done We argue, that: - Current theorem proving systems are not usable for mathematicians. - Current Hypertext systems lack important characteristic. - Current (i.e. old) Discovery systems are too bad, too. Current theorem proving systems are not usable for mathematicians. Current user interfaces for TP systems will not be accepted by mathematicians. The underlying logic (resolution-typed, gentzen-typed, hilbert-typed, or whatever) is too low-level for mathematicians. Translating text-book proofs of mathematical theorems into these calculi is difficult and hard to do for non-logicians. Generated proofs are unreadable for mathematicians (even if there is a graphical representation of proof trees). Current hypertext systems lack important characteristic. Some mathematicians learned TeX; they will not learn HTML to present their articles by hypertext because of poor setting of mathematical symbols. Moreover, static nodes and links do not suffice. Hypertext (the nodes) needs to be automatically generated. The links too. Reading and writing is a mayor mathematical activity. We think about a 'living book', helping the reader in understanding mathematical concepts. Current discovery systems are too bad, too. The old systems AM and EURISKO are often quoted in the AI literature. However, their major deficiencies are: too much heuristics, unsufficient structure; lacking correspondence between theory and program, lacking a theorem prover for proving hypotheses. A fundamental part of discovery system is the implementation of interestingness. D.Lenat did not develop a theory of interestingness. Instead, he used a set of heuristic rules which define interestingness implicitly. We believe that the role of interestingness (esp. for agenda mechanisms) has not yet been understood. We'll try. First subprojects have been done/started: a) Standardization of the natural language texts used in proofs, b) Parsing of mathematical proofs, c) A theory of interestingness, d) A hypertext for a number theory text book (Hasse). ______________________________________________________________________ Martin Strecker (strecker@informatik.uni-ulm.de) ------ -------- Our group at the AI department of the University of Ulm (headed by F. von Henke) is developing methods and tools for system specification and computer-aided verification. Whereas currently most work is carried out with the PVS system, a type-theoretic approach based on an extension of the Calculus of Constructions is being examined, and a specification and verification environment is under development. Expressive type theories are promising because they permit, in one logical framework, a unified treatment of mathematical entities such as predicates, proofs, theories and theory morphisms. One of our interests in the QED project is to investigate questions of: - how to represent and organize a large corpus of mathematical or computer science knowledge - how to add or retrieve specific knowledge ``Knowledge'' is here supposed to mean mathematical terminology, theorems and proofs thereof. At first sight, a solution of these questions depends very much on the logical formalism. In the frame of the QED project, we are interested in finding means of abstracting away from the particular formalism, of translating results from one formalism to another and thus making results transferable between formalisms. ______________________________________________________________________ Javier Thayer (jt@linus.mitre.org) ------ ------ 1. My View of QED The QED project is an attempt to build a coherent cooperative effort in the area of automated mathematical reasoning. Nevertheless, exactly what QED should do is currently very much undecided. In my opinion, many ideas have been expressed about what these goals should be without careful consideration of what it would cost to achieve these goals or whether a broad group of individuals could really benefit from reaching these goals. A common element in most of the suggested goals is the construction of a rigorous mathematics database. By rigorous I mean that each entry in the database is a valid, but not necessarily machine-checked, theorem stated in some formal theory. Taking this as a departure, without refining goals any further, I would suggest that the QED project should first determine who might benefit from project and in what way. Having a clear idea on this issue will make it a lot easier for us to decide exactly what has to be done and to get the necessary support from government and industry Issues that have to be decided include: o Do the entries in the mathematical database have to be machine checked? o Should QED develop a mathematical inference engine? - Will the inference engine be used to facilitate machine checking of the entries in the database? - Will the inference engine be used to facilitate using the mathematical database in inference and calculation? o How will this database be accessible to users? - Should the database be thought of as a lending library easily accessible to the public or as archive accessible only to motivated researchers? - How much user interface, if any, should we develop? 2. Personal Interest in QED. Issues that interest me personally are developing rigorous (possibly machine-checked) formal theories of parts of analysis (including Fourier Analysis and Partial Differential Equations.) I am also very much interested in relating the QED project to symbolic computation. Providing user support facilities to help and encourage less experienced users is also an important area in which I would like to participate. ______________________________________________________________________ Yozo Toda (yozo@aohakobe.ipc.chiba-u.ac.jp) ---- ---- My interest in QED: coordination of mathematical libraries of proof-checkers/assistants. ______________________________________________________________________ Andrzej Trybulec (trybulec@cksr.ac.bialystok.pl) ------- -------- I have been working on the Mizar project for more than 20 years. I am leading the implementation efforts, development of the Mizar data base. I am the designer of the Mizar language, which still evolves. In my opinion, one of the fundamental tasks of the QED effort should focus on reconstruction of the language and technology of mathematics. During last 2500 years mathematicians have developed techniques of deductive reasoning which seem to be optimal in many respects. It is an astonishing phenomenon that the same techniques led to biggest achievements of human mind while at the same time they are used for teaching children. I fully appreciate the efforts to clarify the logical basis of the QED project but I would like to stress the need for systems that allow us to write texts as close as possible to regular mathematical papers. I would like to have such systems as soon as possible even if at the cost of sacrificing their reliability and clarity. I am affraid that current experience with formalized mathematics is too narrow and can hardly be used to foresee the future problems of implementing the QED program. I see an urgent need to collect a sizeable corpus of formalized texts, idealy written by working mathematicians. At times, I think that all of us underestimate both the difficulties of building QED and the potential gains from it. ______________________________________________________________________