and RAMC), developed in our inference laboratory (ATINF).
NEWSLETTER
Last year I was delighted to report in the December issue of the AAR newsletter that William McCune had solved the Robbins algebra problem. This year I am equally pleased to note that AI Magazine has cited this achievement as one of five major accomplishments in artificial intelligence.
Problem solving is, of course, the real test of a new strategy or a new theorem prover. In this regard, I encourage you to read the article by Stéphane Fèvre and N. Peltier on the solution of two problems in geometry. I've also included a challenge problem in Tarskian geometry.
For the new year, I hope that AAR members will send in additional challenging problems or reports on new solutions.
The first elections of CADE trustees were held by electronic mail in August 1997, following CADE-14. The elections were organized according to the bylaws of CADE Inc. to fill two positions in the board of trustees: one left vacant by Mark Stickel, whose term in office had just expired, and one temporarily occupied by William McCune as program chair of CADE-14. Ulrich Furbach, William McCune, and Dale Miller were nominated and accepted the nominations. Ulrich Furbach and William McCune were elected, after a vote in which all three candidates received strong support. The Association of Automated Reasoning thanks Mark Stickel for his years in office and offers congratulations and best wishes to Ulrich Furbach and William McCune as new trustees of CADE Inc.
OSHL
The University of North Carolina theorem-proving group announces the availability of the OSHL (ordered semantic hyper-linking) theorem prover on the Web.
OSHL combines natural semantics, equality (term rewriting and narrowing), efficient propositional techniques, and goal-sensitivity. This prover also has special techniques for AC operators (but not AC unification).
This site has an interface to the OSHL prover that permits the user to run one of a selection of predefined examples or to input one's own problem and semantics. OSHL may also be downloaded from the Web site.
A runtime limit of 300 seconds has been imposed for problems submitted over the Web. Of course, if many people are running this prover at the same time, the response will be very slow.
Please send any reports of problems to Yunshan Zhu at zhu@cs.unc.edu, with a cc to David Plaisted at plaisted@cs.unc.edu.
Gandalf Release c-1.0c
Gandalf is a theorem prover for classical first-order logic. The prover, developed by Tanel Tammet, won the MIX class of the last ATP competition CASC-14, held this summer during CADE in Townsville.
Gandalf and related materials can be obtained from the newly created Gandalf home page on the Web.
Gandalf comes in several different forms:
Gandalf is also used as a name for a whole family of code-sharing theorem provers, currently including versions for classical first-order logic, intuitionistic first-order logic, propositional linear logic, and a subset of Martin Lof's constructive type theory.
Formal Methods Specifications and Analysis Guidebook
The NASA guidebook Formal Methods Specification and Analysis Guidebook for the Verification of Software and Computer Systems, Volume II: A Practitioner's Companion (NASA-GB-001-97, 245 pp., 1997) is available via the Web.
This guidebook is a product of the NASA Software Program and was cooperatively developed by three NASA centers (Jet Propulsion Laboratory, Johnson Space Center, and Langley Research Center) with support from SRI International, ViGYAN, and Lockheed Martin. The guidebook reflects experience in pilot testing formal methods on several of NASA's software subsystems.
The book is designed to help transition formal methods from experimental use into practical application for critical software requirements and design. It discusses technical issues involved in applying these techniques to aerospace and avionics software systems and provides an overview of the current status of formal methods techniques.
A Computational Logic Handbook
The second edition of the book A Computational Logic Handbook, by Robert S. Boyer and J Strother Moore, has recently been published by Academic Press (1997, ISBN 0121229556. 518+xxv pp., $69.95). To order the book, contact Academic Press at 1-800-321-5068.
The second edition is the authoritative documentation for Nqthm-1992, the most recent edition of the Boyer-Moore prover, which may be obtained with sources and without fee at the FTP site. In addition to a very large number of minor corrections and improvements to the first edition, the second edition
CADE-15
The 15th International Conference on Automated Deduction will take place July 5-10, 1998, in Lindau, Germany. CADE is the major forum for the presentation of new research in all aspects of automated deduction.
Papers: Original research papers, descriptions of systems, and problem sets are solicited. Research papers can be up to 15 proceedings pages, and system descriptions up to 4 pages. The proceedings of CADE-15 will be published by Springer-Verlag in the LNAI series. All submissions must be received by January 5, 1998.
Workshops and Tutorials: Proposals for workshops and tutorials, which are to be held July 5-6, are solicited for CADE-15. Workshops will run the whole day, and tutorials for half a day. Tutorials may be introductory, intermediate, or advanced. Anyone wishing to organize a workshop or tutorial in conjunction with CADE-14 should send (e-mail preferred) a proposal no longer than two pages to the program chair by February 15, 1998.
Special Symposium: A special symposium entitled ``Deduction as a Cross-Sectional Technology'' will be held on Friday, July 10.
Details on Submission: Further information is available on the CADE-15 Web site.
Program Chair: Claude and Helene Kirchner, LORIA, INRIA & CNRS, 615 Rue du Jardin Botanique, BP 101, F-54602 Villers-les-Nancy CEDEX, FRANCE, Phone: +33 3 83 59 30 11 or 12; FAX: +33 3 83 27 83 19; E-mail: cade-15@loria.fr.
CAV'98
The conference on Computer-aided Verification will take place June 28-July 2, 1998, in Vancouver, British Columbia, Canada.
Topics of interest include modeling and specification formalisms, algorithms and tools, verification techniques, applications and case studies, and verification in practice. Submission are invited in two categories: (1) regular papers (abstract not exceeding ten pages) and (2) tool presentations (abstract not exceeding four pages). The deadline for submissions is January 9, 1998.
For further information, see the Web site.
33 Years of Gröbner Bases
The international conference ``33 Years of Gröbner Bases" will be held in Hagenberg, Austria, on February 2-4, 1998. The first day of the conference will be devoted to tutorials on various connections and applications of Gröbner bases to other mathematical fields. Papers on new research in Gröbner bases theory will be presented on the second and third days of the conference. Additional activities such as minisymposia, software demonstrations, and poster sessions are planned. More information about the conference is provided on the Web.
Papers presenting original contributions in any area of first-order theorem proving are being sought for a special issue on ``Advances in first-order theorem proving'' of the Journal of Symbolic Computation. Topics of interest include resolution and tableau methods; equational reasoning and term-rewriting systems; constraint-based reasoning; unification algorithms for first-order theories; specialized decision procedures; propositional logic; abstraction; first-order constraints; complexity of theorem proving procedures; and applications of first-order theorem provers to problems in artificial intelligence, verification, and formal mathematics.
Manuscripts should be unpublished works and not submitted elsewhere. Revised and enhanced versions of papers published in conference proceedings that have not appeared in archival journals are eligible for submission. The participants of the workship on First-order Theorem Proving (FTP'97) are invited to submit papers, but the special issue is open for every body. All submissions will be subject to the standard review procedure. Submission deadline is June 1, 1998.
Authors are invited to submit manuscripts by e-mail to one of the guest editors as a PostScript file, preferably gzipped and uuencoded.
Guest editor addresses: Maria Paola Bonacina (University of Iowa) bonacina@cs.uiowa.edu; and Ulrich Furbach (Universitat Koblenz) uli@mailhost.uni-koblenz.de.
For further information, see the Web site.
We show how to use automated model building techniques to solve automatically
two problems introduced
by Li Dafa concerning von Plato's axiomatization
of constructive apartness geometry.
First, we give an automated proof of the incompleteness of von Plato's
axiomatization for elementary geometry (proved by hand by Li Dafa).
Second, we prove automatically the independence of axioms for
projective geometry (which was stated as a conjecture by Li Dafa
in a recent AAR newsletter.
Both problems are solved very easily by using automated model builders (FMC
and RAMC), developed in our inference laboratory (ATINF).
Jan von Plato introduced in 1995 an axiomatization of constructive apartness geometry [8]. The intent of von Plato was to propose a constructive axiomatization of elementary geometry. That is why theorems have to be proved in intuitionistic logic.
His axiomatization uses four predicates and two function symbols :
We give below the translation of the axioms in clausal logic.
Von Plato also gave an axiomatization of constructive projective
geometry. It is obtained by adding the following axiom to the previous ones:
In [3], Li Dafa proved that von Plato's axiomatization is not complete for elementary geometry. In his proof, Li Dafa considered the following statement (noted (R) in [3]): ``If x and y are different lines, then either x and y are convergent or for any point z, z is apart from x or y''. (R) is obviously valid in elementary geometry. However, Li Dafa showed that (R) is not a theorem of von Plato's geometry, by proving by hand that it cannot be derived from the axioms. In this work, we give a purely automated proof of this assertion, by constructing automatically a model of von Plato's axioms that contradicts (R). The existence of a counterexample implies that the formula is not provable in classical logic and hence not provable in intuitionistic logic.
The statement (R) can be formalized as follows:
We use our model builder FMC for building a model
of the axioms that is not a model of (R).
FMC is a finite model builder based on enumeration of the set of
interpretation. It uses some strategies, taking into account the failures of
the previously tested interpretations and the isomorphism on interpretations,
in order to reduce the
number of candidates to be considered (see [6] for details).
We obtain the following 2-elements model in 0.01 second.
We also build a 3-elements model where there exist at least three distinct points and two distinct lines (see the Appendix).
The following Herbrand model (which is very similar to the finite one) can
also be generated by using the system RAMC (Refutation And
Model Construction) denoted to the simultaneous search for refutations
and models (see, for example, [2, 1]).
In [4], Li Dafa showed (using the theorem prover ANDP) that the axioms 1.2, 1.5, and 1.6 are in fact redundant for constructive projective geometry. Li Dafa also contended that the axioms 1.3, 1.6, and 4.3 are not redundant. More precisely, he argued that the equivalence of the predicate con and dipt, which is clearly valid in constructive geometry, does not hold if axioms 1.3, 1.6, and 4.3 are deleted. But no proof of this assertion is presented:
Our prover ANPD fails to find a proof of the lemma from the remaining 12 axioms. We believe that the lemmadoes not hold. Thus the convergence and distinctness of two lines cannot become equivalent after Axioms 1.3, 1.6, 4.3 are deleted. ([4], page 3)
We used our model builder FMC to get a purely automated proof of this
assertion, by building a model of von Plato's axiomatization of projective
geometry without axioms 1.3, 1.6, and 4.3 in which con(x,y) and
diln(x,y) are not equivalent.
We obtain the following 2-elements model (in 0.01 seconds).
We note that
other model
builders, such as SEM,
[9],
FINDER,
[7],
and MACE
[5],
could be used also.
Theorem provers are, in general, unable to detect the satisfiability (resp. nonvalidity) of a formula, even if the formula admits a very simple model (resp. counterexample). The examples treated in this paper--though rather simple from a model building point of view--show once more the usefulness of model builders in studying mathematical theories. In the near future, we shall continue our investigation of von Plato's axiomatization of geometry, using the model building systems developed into the framework of the ATINF project.
References
In an article in AI Magazine (Fall 1997, pp. 49-52) entitled ``Artificial Intelligence: Realizing the Ultimate Promises of Computing,'' author David L. Waltz cited the 1996 solution of the Robbins algebra problem as one of five key applications of AI in recent years.
The Robbins algebra problem was solved by William McCune of Argonne National Laboratory using his automated reasoning system EQP. We reported on this achievement in the December 1996 issue of the AAR Newsletter. For a detailed discussion of the problem and solution, see the latest issue of the Journal of Automated Reasoning 19, no. 3 (December 1997) 263-276.
The other four accomplishments cited by AI Magazine were an autonomous vehicle controlled by an onboard computer system, the Deep Blue chess computer, a system that classifies very faint signals as stars or galaxies, and a spoken language interface for flight information.
Waltz emphasized that each of the five cited accomplishments was the result of "decades of federally-sponsored fundamental research.'' The work at Argonne that led to the solution of the Robbins problem was funded by the U.S. Department of Energy.
With the inclusion of the lemma on the symmetry of betweenness, the five-point theorem in Tarskian geometry is true--but most difficult to prove with an automated reasoning program. (The symmetry lemma itself is, on the other hand, easy to prove with a reasoning program.)
The challenge problem, then, is to use the following input clauses--but without using the commented out (with a %) lemma on the symmetry of betweenness--to prove this theorem with an automated reasoning program without giving substantial guidance. To date, without the symmetry lemma, we have not obtained a proof.
list(usable).
% Axioms for Tarskian Geometry
% identity axiom for betweenness
-B(x,y,x) | EQ(x,y).
% transitivity axiom for betweenness
-B(x,y,u) | -B(y,z,u) | B(x,y,z).
% connectivity axiom for betweenness
-B(x,y,z) | -B(x,y,u) | EQ(x,y) | B(x,z,u) | B(x,u,z).
% reflexivity axiom for equidistance
L(x,y,y,x).
% identity axiom for equidistance
-L(x,y,z,z) | EQ(x,y).
% transitivity axiom for equidistance
-L(x,y,z,u) | -L(x,y,v,w) | L(z,u,v,w).
% Pasch's axiom (two clauses)
-B(x,v,u) | -B(y,u,z) | B(x,op(v,x,y,z,u),y).
-B(x,v,u) | -B(y,u,z) | B(z,v,op(v,x,y,z,u)).
% Euclid's axiom (three clauses)
-B(x,u,v) | -B(y,u,z) | EQ(x,u) | B(x,z,euc1(v,x,y,z,u)).
-B(x,u,v) | -B(y,u,z) | EQ(x,u) | B(x,y,euc2(v,x,y,z,u)).
-B(x,u,v) | -B(y,u,z) | EQ(x,u) | B(euc1(v,x,y,z,u),v,euc2(v,x,y,z,u)).
% five-ext axiom
-L(x1,y1,x2,y2) | -L(y1,z1,y2,z2) | -L(x1,u1,x2,u2) | -L(y1,u1,y2,u2)
| -B(x1,y1,z1) | -B(x2,y2,z2) | EQ(x1,y1) | L(z1,u1,z2,u2).
% axiom of ext construction (two clauses)
B(x,y,ext(x,y,u,v)).
L(y,ext(x,y,u,v),u,v).
% lower dimension axiom (three clauses)
-B(c1,c2,c3).
-B(c2,c3,c1).
-B(c3,c1,c2).
% upper dimension axiom
-L(x,u,x,v) | -L(y,u,y,v) | -L(z,u,z,v)
| EQ(u,v) | B(x,y,z) | B(y,z,x) | B(z,x,y).
% weakened continuity axiom (two clauses)
-L(u1,x1,u1,x2) | -L(u1,z1,u1,z2) | -B(u1,x1,z1) | -B(x1,y1,z1)
| L(u1,y1,u1,cont(x1,y1,z1,x2,z2,u1)).
-L(u1,x1,u1,x2) | -L(u1,z1,u1,z2) | -B(u1,x1,z1) | -B(x1,y1,z1)
| B(x2,cont(x1,y1,z1,x2,z2,u1),z2).
% ---------------
% Equality Axioms
% ---------------
% define equality
EQ(x,x).
-EQ(x,y) | EQ(y,x).
-EQ(x,y) | -EQ(y,z) | EQ(x,z).
% equality substitution axioms for B
-EQ(u,v) | -B(u,x2,x3) | B(v,x2,x3).
-EQ(u,v) | -B(x1,u,x3) | B(x1,v,x3).
-EQ(u,v) | -B(x1,x2,u) | B(x1,x2,v).
% equality substitution axioms for L
-EQ(u,v) | -L(u,x2,x3,x4) | L(v,x2,x3,x4).
-EQ(u,v) | -L(x1,u,x3,x4) | L(x1,v,x3,x4).
-EQ(u,v) | -L(x1,x2,u,x4) | L(x1,x2,v,x4).
-EQ(u,v) | -L(x1,x2,x3,u) | L(x1,x2,x3,v).
% equality substitution axioms for op
-EQ(u,v) | EQ(op(u,x2,x3,x4,x5),op(v,x2,x3,x4,x5)).
-EQ(u,v) | EQ(op(x1,u,x3,x4,x5),op(x1,v,x3,x4,x5)).
-EQ(u,v) | EQ(op(x1,x2,u,x4,x5),op(x1,x2,v,x4,x5)).
-EQ(u,v) | EQ(op(x1,x2,x3,u,x5),op(x1,x2,x3,v,x5)).
-EQ(u,v) | EQ(op(x1,x2,x3,x4,u),op(x1,x2,x3,x4,v)).
% equality substitution axioms for euc1
-EQ(u,v) | EQ(euc1(u,x2,x3,x4,x5),euc1(v,x2,x3,x4,x5)).
-EQ(u,v) | EQ(euc1(x1,u,x3,x4,x5),euc1(x1,v,x3,x4,x5)).
-EQ(u,v) | EQ(euc1(x1,x2,u,x4,x5),euc1(x1,x2,v,x4,x5)).
-EQ(u,v) | EQ(euc1(x1,x2,x3,u,x5),euc1(x1,x2,x3,v,x5)).
-EQ(u,v) | EQ(euc1(x1,x2,x3,x4,u),euc1(x1,x2,x3,x4,v)).
% equality substitution axioms for euc2
-EQ(u,v) | EQ(euc2(u,x2,x3,x4,x5),euc2(v,x2,x3,x4,x5)).
-EQ(u,v) | EQ(euc2(x1,u,x3,x4,x5),euc2(x1,v,x3,x4,x5)).
-EQ(u,v) | EQ(euc2(x1,x2,u,x4,x5),euc2(x1,x2,v,x4,x5)).
-EQ(u,v) | EQ(euc2(x1,x2,x3,u,x5),euc2(x1,x2,x3,v,x5)).
-EQ(u,v) | EQ(euc2(x1,x2,x3,x4,u),euc2(x1,x2,x3,x4,v)).
% equality substitution axioms for ext
-EQ(u,v) | EQ(ext(u,x2,x3,x4),ext(v,x2,x3,x4)).
-EQ(u,v) | EQ(ext(x1,u,x3,x4),ext(x1,v,x3,x4)).
-EQ(u,v) | EQ(ext(x1,x2,u,x4),ext(x1,x2,v,x4)).
-EQ(u,v) | EQ(ext(x1,x2,x3,u),ext(x1,x2,x3,v)).
% equality substitution axioms for cont
-EQ(u,v) | EQ(cont(u,x2,x3,x4,x5,x6),cont(v,x2,x3,x4,x5,x6)).
-EQ(u,v) | EQ(cont(x1,u,x3,x4,x5,x6),cont(x1,v,x3,x4,x5,x6)).
-EQ(u,v) | EQ(cont(x1,x2,u,x4,x5,x6),cont(x1,x2,v,x4,x5,x6)).
-EQ(u,v) | EQ(cont(x1,x2,x3,u,x5,x6),cont(x1,x2,x3,v,x5,x6)).
-EQ(u,v) | EQ(cont(x1,x2,x3,x4,u,x6),cont(x1,x2,x3,x4,v,x6)).
-EQ(u,v) | EQ(cont(x1,x2,x3,x4,x5,u),cont(x1,x2,x3,x4,x5,v)).
% ---------------------------------
% Additional Axioms for Colinearity
% ---------------------------------
% definition
-C(x,y,z) | B(x,y,z) | B(y,x,z) | B(x,z,y).
-B(x,y,z) | C(x,y,z).
-B(y,x,z) | C(x,y,z).
-B(x,z,y) | C(x,y,z).
% equality substitution for C
-EQ(x,y) | -C(x,w,z) | C(y,w,z).
-EQ(x,y) | -C(w,x,z) | C(w,y,z).
-EQ(x,y) | -C(w,z,x) | C(w,z,y).
end_of_list.
list(sos).
B(a,c,e).
B(a,d,e).
B(c,b,d).
-B(a,b,e).
% -B(x,y,z) | B(z,y,x).
end_of_list.