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.

Secretary of AAR

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:

- Ready-built executables for Sun Sparc, DEC Alpha, PC under NetBSD, PC under MS-DOS/Windows
- C source for UNIX
- C source for MS-DOS/Windows
- Scheme source

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

- describes new syntax, including COND, CASE, LET, LIST*, and backquote;
- describes some higher-order inference procedures, including constrained functions and functional instantiation;
- documents more sophisticated control machinery for manipulating very large theories;
- introduces a secure proof-checking environment;
- presents example input dealing with difficult questions in formal methods and mathematics;
- provides a formal parser for the syntax;
- compares the proof complexity of many interesting checked examples;
- includes tutorial help; and
- contains a thorough bibliography of Nqthm applications.

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

Laboratory Leibniz-Imag, Grenoble, France

Stephane.Fevre@imag.fr, Nicolas.Peltier@imag.fr

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 :

*dipt*(*x*,*y*):*x*and*y*are two distinct points.*diln*(*x*,*y*):*x*and*y*are two distinct lines.*apt*(*x*,*y*): point*x*is apart from line*y*.*con*(*x*,*y*): lines*x*and*y*are convergent.*ln*(*x*,*y*) is a connecting line of points*x*and*y*.*pt*(*x*,*y*) is the intersection point of*x*and*y*(if*x*and*y*are distinct and convergent; if*x*and*y*are not convergent*pt*(*x*,*y*) has no intuitive meaning).

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* (**R**efutation **A**nd **
M**odel **C**onstruction) 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 lemma does 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**

**1**-
C. Bourely, R. Caferra, and N. Peltier.
A method for building models automatically. Experiments with
an extension of Otter.
In
*Proceedings of CADE-12, LNAI 814*, pages 72-86. Springer, 1994. **2**-
R. Caferra and N. Zabel.
A method for simultaneous search for refutations and models by
equational constraint solving.
*J. Symbolic Computation*, 13:613-641, 1992. **3**-
L. Dafa.
Is von Plato's axiomatization complete for elementary geometry?
*AAR Newsletter*, 37, 1997. **4**-
L. Dafa.
Three axioms of von Plato's axiomatization of constructive
projective geometry are not independent.
*AAR Newsletter*, 37, 1997. **5**-
W. McCune.
A Davis-Putnam program and its application to finite
first-order
model search: Quasigroup existence problems.
Technical report MCS-TM-19, Argonne National Laboratory, 1994.
**6**-
N. Peltier.
A new method for automated finite model building exploiting
failures
and symmetries.
To appear in the
*J. Logic and Computation,*1997. **7**-
J. Slaney.
Finder (finite domain enumerator): Notes and guides.
Technical report, The Australian National University Automated
Reasoning
Project, Canberra, 1992.
**8**-
J. von Plato.
The axiomas of constructive geometry.
*Annals of Pure and Applied Logic*, 2:169-200, 1995. **9**-
J. Zhang and H. Zhang.
SEM: A system for enumerating models.
In
*Proc. IJCAI-95*, volume 1, pages 298-303. Morgan Kaufmann, 1995.

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.