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.
______________________________________________________________________