von Plato's axiomatization constructively.
NEWSLETTER
"If I rest, I rust,"' claimed Mendelsohn. I have the same feeling about the field of automated reasoning. If we are not to rust, we need to increase the power of our reasoning systems, to add capabilities such as self-analysis and meta-level reasoning, to attack open questions, and to find real applications not currently being studied -- all increasing the likelihood of substantial visibility.
One step toward this is participation in the CADE competitions. Such competitions can, for example, reveal areas where our automated reasoning programs need strengthening. Another step is the TPTP library, which provides test problems for automated theorem-proving programs.
My favorite approach is to attempt to answer challenging questions. But to do so, I need your help: I would like to accumulate a database of such questions, from diverse areas such as universal algebra, quantum computing, logic, puzzles, circuit design, and the like.
The future of automated reasoning is bright--but I strongly believe that advances in the field require experimentation, and experimentation requires challenging problems. I hope that you will start flooding my e-mail with such problems.
The CADE-15 ATP System Competition
Download Postscript file
Download DVI file
In order to stimulate automated theorem-proving (ATP) system development, and to expose ATP systems to interested researchers, a competition for first-order ATP systems will be held at CADE-15 on Tuesday, July 7, 1998. The CADE-15 ATP System Competition (CASC-15) will evaluate the performance of sound, fully automatic, first-order ATP systems. The evaluation will be in terms of the number of problems solved and the average runtime for successful solutions. The evaluation will be done in the context of a bounded number of eligible problems, chosen from the TPTP Problem Library (see article below), and specified time limit for each solution attempt.
Divisions
CASC-15 is divided into divisions according to problem and system characteristics. There are four competition divisions in which the systems are explicitly ranked, and one demonstration division in which systems can demonstrate their abilities without being formally ranked. The competition divisions run on locally provided standard UNIX workstation (the general hardware). Prizes will be awarded in the competition divisions.
Registration
Registration for CASC-15 closes on June 8, 1998, and no registrations will be accepted after this deadline. System registration is via the CASC-15 WWW page. For each system entered, a person has to be nominated to handle all issues (including execution difficulties) arising before and during the competition. It is not necessary for entrants to physically attend the competition, but at least the nominated person has to register for CASC-15 via the CADE-15 registration form.
Registration deadline: June 8, 1998
Installation starts: June 15, 1998
Installation deadline: June 26, 1998
Competition date: July 7, 1998
Organizers
| Geoff Sutcliffe | Christian Suttner |
| Dept of Computer Science | Institut fur Informatik |
| James Cook University | TU Munchen |
| Townsville | D-80290 Munich |
| Australia 4811 | Germany |
| geoff@cs.jcu.edu.au | suttner@informatik.tu-muenchen.de |
For further information
| CASC-15 WWW Site | http://www.cs.jcu.edu.au/~tptp/CASC-15/ | CADE-15 WWW Site | http://www.th-darmstadt.de/cade-15 |
The TPTP Problem Library, Release v2.1.0
Geoff Sutcliffe
Dept. of Computer Science, James Cook University, Australia
geoff@cs.jcu.edu.au
Christian Suttner
Institut für Informatik, TU München, Germany
suttner@informatik.tu-muenchen.de
Download Postscript file
Download DVI file
The TPTP (Thousands of Problems for Theorem Provers) Problem Library is a library of test problems for automated theorem-proving (ATP) systems. The TPTP supplies the ATP community with
The principal motivation for this project is to move the testing and evaluation of ATP systems from the previously ad hoc situation onto a firm footing. This became necessary, as results being published do not always accurately reflect the capabilities of the ATP system being considered. A common library of problems is necessary for meaningful system evaluations, meaningful system comparisons, repeatability of testing, and the production of statistically significant results. The TPTP is such a library.
Release v2.1.0 of the TPTP is now available. TPTP v2.1.0 contains 3622 problems in 28 domains. Changes (after v1.2.1) are as follows:
The TPTP is regularly updated with new problems, additional information, and enhanced utilities. If you would like to register as a TPTP user and be kept informed of such developments, please e-mail one of us. Our addresses are Geoff Sutcliffe - geoff@cs.jcu.edu.au, and Christian Suttner - suttner@informatik.tu-muenchen.de.
The TPTP can be obtained by anonymous ftp from the Department of Computer Science, James Cook University, Australia. There are three files in the TPTP distribution: ReadMe-v2.1.0, TPTP-v2.1.0.tar.gz, and TR-v2.1.0.ps.gz. General information about the library is in the ReadMe-v2.1.0 file, the library is packaged in TPTP-v2.1.0.tar.gz, and a technical report describing the TPTP (in postscript form) is in TR-v2.1.0.ps.gz. Please read the ReadMe file, as it contains up-to-date information about the TPTP. The technical report serves as a manual explaining the structure and use of the TPTP. It also explains much of the reasoning behind the development of the TPTP.
FroCoS'98
In various areas of logic, computation, language processing, and artificial intelligence, an obvious need exists for using specialized formalisms and inference mechanisms for special tasks. In order to be usable in practice, these specialized systems must be combined with each other, and they must be integrated into general purpose systems. Recently, the development of general techniques for the combination and integration of special systems has been initiated in many areas.
Frontiers of Combining Systems '98, to be held on October 2-4, 1998, in Amsterdam, is intended to offer a common forum for these research activities. It also aims to offer the possibbility of presenting results on particular instances of combination and integration, and on their practical use.
Topics of interest for the workshop include combination of constraint solving techniques and combination of decision procedures; integration of equational and other theories into deductive systems; combinations of logics and of term rewriting systems; and * hybrid systems in computational linguistics, knowledge representation, natural language processing, and human computer interaction.
Authors are invited to submit a detailed abstract of a full paper of at most 10 pages either by e-mail (sent to frocos98@wins.uva.nl, using `Submission' as the subject line) or by regular mail, (to Maarten de Rijke, attn: FroCoS'98, ILLC, University of Amsterdam, Plantage Muidergracht 24, 1018 TV Amsterdam, The Netherlands) no later than May 15, 1998. The proceedings will be published as a volume of the Kluwer series on ``Applied Logic''.
Information about
FroCoS'98 can be obtained on the World Wide Web.
LD'98
The first international workshop on labeled deduction will take place in Freiburg, Germany, September 7-9, 1998. Papers on current research in all aspects of labeled to ld98@informatik.uni-freiburg.de, before April 15, 1998. For further information, see the Web page.
AiML'98
Advances in Modal Logic is an initiative aimed at presenting an up-to-date picture of the state of the art in modal logic and its many applications. The initiative consists of a workshop series together with volumes based on those workshops.
Advances in Modal Logic '98 is the second workshop organized as part of this initiative. AiML'98 will be held from October 16-18, 1998, in Uppsala, Sweden. Thematic areas of interest at AiML '98 include modal logics of agency and normative systems, algebraic and model-theoretic aspects of modal logic, modal approaches to grammar and natural language semantics computational and philosophical aspects of modal logic, and modal logic and belief revision. Additionally, a special afternoon session on modal logic and belief revision will be chaired by Sven-Ove Hansson and Sten Lindstrom.
Authors are invited to submit a detailed abstract of a full paper of at most 10 pages by e-mail to Heinrich Wansing (e-mail address: wansing@rz.uni-leipzig.de), using `AiML98 Submission' as the subject line. The deadline is June 1, 1998.
E-mail inquiries about AiML '98 should be directed to Krister.Segerberg@filosofi.uu.se. Information about the AiML initiative is on the Web.
CSL '98
The annual conference of the European Association for Computer Science Logic will take place August 23-28, 1998, in Brno, Czech Republic. The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on topics significant for computer science. In 1998 the CSL conference will be organized as a joint event with MFCS (Mathematical Foundations of Computer Science). Authors are invited to submit a draft or full paper (up to 12 pages) by electronic submission to csl98-subm@dbai.tuwien.ac.at by April 15, 1998.
The following is an overview on splitting over clauses. In my judgment, semantics is more important than syntax. Therefore, I prefer to split over clauses based on the meaning of the predicates and functions and constants. In particular, because of my preference for the set of support strategy, I strongly favor predicates, functions, and constants that occur in a well-chosen set of support, that consisting of the special hypothesis and the denial. I emphasize, however, that one should split over clauses only when in trouble--for example, when one is trapped in many clauses of the same weight or when no clauses of small weight are left.
Do's
1. Split over ground tautologies, natural ones as in the subgroups of index 2 theorem. The theorem asserts that subgroups of index 2 are normal. Similar to the manner in which a mathematician might proceed, try two cases: where a is an arbitrary element of the group, first, add to the input the unit clause O(a), which corresponds to the assumption that the element a is in the subgroup O; second, instead add to the input -O(a), which corresponds to the assumption that the element a is not in the subgroup O.
2. Key on constants from the denial or the special hypothesis. In program verification, key on less, equal, and greater. (I endorse choosing a predicate that is from the special hypothesis-for example, that which asserts the subgroup has index 2-and combining it with constants from the denial. Splitting over such an atom appeals to me, as seen when splitting over O(a) and -O(a), to prove that subgroups of index 2 are normal.)
3. Prefer splitting over clauses from the initial set of support, then deduced clauses, then the usable list. (Splitting over a ground clause in the usable list has the danger of focusing on the underlying theory, rather than on the theorem under study.)
4. As for constants to use in producing clauses (not in the input) for splitting, such as tautologies, prefer constants from sos over constants from usable.
5. Prefer (perhaps) simpler literals (e.g., in some cases, one might split over a 3-clause rather than a 2-clause).
6. When hyperresolution is the only inference rule, split over positive clauses only.
7. When no unit clauses remain, split.
8. Split (usually) only over positive clauses to address non-Hornness. However, sometimes split over mixed or negative to get negative units to, in turn, move clauses toward being Horn.
9. Look for non-Horn clauses, not necessarily positive, that share a literal, find (if possible) a ground negative literal that might resolve against the common literal, and split on it to reduce the non-Hornness (for example, in the index 2 problem).
10. After splitting, put the splitter in the hot list.
Don'ts
1. Don't (at least in most cases) split over disjunctions from usable that correspond to negation of the ``and" of the conclusions (e.g., in two-valued sentential calculus).
2. Don't paramodulate from a nonunit clause, even if the clauses are all ground (the mixing of cases hurts).
3. Don't use constants from axioms: such a use is not likely to work, since constants are arbitrarily introduced. (As is known to many, my objection to hyperresolution in some contexts is that it forces one to place in the sos axioms, hence allowing the program to explore the theory rather than concentrating on the theorem under attack.)
Download Postscript file
Download DVI file
1. Introduction
In the 1920s, A. Heyting attempted to axiomatize constructive geometry [1]. Recently, von Plato used different concepts to axiomatize constructive geometry [2]. Specifically, he used point apartness instead of point equality, line apartness instead of line equality, apartness of a point from a line instead incidence of a point with a line, and convergence of two lines instead of parallelism of two lines. Hence, he calls the geometry apartness geometry rather than incidence geometry, as it is known in classical terminology. von Plato's axiomatization of apartness geometry consists of 14 axioms (see AAR Newsletter 37, August 1997). It makes possible the automation of constructive geometry theorem proving.
In [3] we reported results obtained in constructive apartness geometry using our natural deduction automated prover ANDP [4]. In particular, we showed that von Plato's axioms for connecting lines can be replaced by one single axiom; that his axioms for intersection points can be replaced by a single axiom; and that his axiom for constructive uniqueness for lines and points can be replaced by a shorter axiom. We note that people have long been interested in replacing more axioms by fewer axioms, especially by shorter axioms (see, for example, [5-7]).
In this article we report the fact that a shorter and more intuitive formula can be used to constructively replace von Plato's Axiom 4.3, the third axiom of compatibility of equality with apartness and convergence. This result was obtained after many computer experiments using our prover ANDP.
2. Description of ANDP
There are many rules in a natural deduction system adapted from Gentzen system. The rules UG (universal generalization) and EG (existential generalization) are used to introduce quantifiers. The rules US (universal specialization) and ES (existential specialization) are used to eliminate quantifiers. A natural deduction system including the rules UG, EG, US, and ES and rules for connectives is complete.
In our natural deduction prover ANDP, we have two algorithms to handle quantifiers: one is for introducing quantifiers, the other for eliminating quantifiers. If two formulas can become equal after applying the rules for introducing quantifiers, then our algorithm can find the series of operations UG and EG and decide which occurrences of terms should be universally or existentially generalized [4]. Similarly, if two formulas can become equal after applying the rules for eliminating quantifiers, then our algorithm can find the series of operations US and ES and decide which terms should be used to replace the bound variables without using Skolem functions [4].
3. Experiments
In this section we present results from computer experiments made on a SPARCstation-10 at SUNY-Albany.
3.1 Shortening the Third Axiom
The following formula is the third axiom of compatibility of equality with apartness and convergence. We call it the third axiom, for short.
(Ax)(Ay)(Az)[CON x y ->[ DILN y z | CON x z]]
It means that for all lines x, y, and z, if lines x y are convergent, then lines y z are different or lines x z are convergent.
We use the following formula to replace the axiom above.
(Ax)(Ay)[CON x y -> DILN x y]
It means that if lines x y are convergent, they are different.
Clearly, the formula is shorter and more intuitive than the third axiom.
Theorem. The third axiom of compatibility of equality with apartness and convergence can be replaced constructively by the new formula.
Proof. Let the new axiomatization be obtained
from von Plato's axiomatization
for apartness geometry by replacing the third axiom by the new formula above.
Let us prove that new axiomatization
von Plato's axiomatization constructively.
For 
: It is enough to infer the new formula above from von Plato's axiomatization.
It is just Theorem 3.2 in [2].
For 
:
It is enough to infer the third axiom from the new axiomatization.
The mechanical proof of the third axiom from 14 axioms
of the new axiomatization as premises is given in Appendix 1.
The proof, which is classical, has 34 steps and
required 10 CPU-seconds on a SPARCstation-10.
From the proof it is not hard to see that only four axioms of the new axiomatization are used to infer the third axiom. The four axioms are 1.2, 1.3, 1.6, and the new formula.
Motivated by this success, we then removed some of the four axioms to minimize the premises. After several experiments, we obtained a mechanical proof from two axioms as premises. The two axioms are 1.6 and the new formula. The proof, which also is classical, is given in Appendix 2. The proof has 19 steps and required 2 seconds on a SPARCstation 10.
It is easy to transform the classical proof into a constructive proof. We give it as follows.
It is enough to prove 
.
Assume CON l m. Let's prove that 
.
After eliminating quantifiers, it follows from Axiom 1.6 that
.
By assumption, we get 
.
If CON l n, then the conclusion.
Assume CON m n. From the new formula, we get 
.
By the assumption CON m n, then DILN m n, then the conclusion.
Q.E.D.
3.2 Experiments
The following are experiments we did recently to shorten the axioms for apartness geometry.
1. Use the symmetry of DIPT to replace Axiom 1.4.
2. Use the symmetry of DILN to replace Axiom 1.5.
3. Use the symmetry of CON to replace Axiom 1.6.
4. Use the new formula above to replace any one of 14 axioms of von Plato's axiomatization. For example, replace Axiom 1.5 or 1.6.
After many experiments we proved the theorem above.
Acknowledgment
This work was supported by NSFC. I thank Prof. Deepak Kapur for his invitation and for discussions.
Appendix 1
In this appendix we show how one can, from the 14 axioms of the new axiomatization, infer the third axiom of compatibility of equality with apartness and convergence.
The proof has 34 steps. The time consumed on SPARCstation 10 to get the proof is 10 seconds. Only Axioms 1.2, 1.3, 1.6, and the new axiom are used to get the proof.
Solution
1. 14 axioms of new axiomatization for apartness geometry
ASSUMED-PREMISE
2. (Ax)~DILN x x Ax 1.2 SIMP 1
3. (Ax)~CON x x Ax 1.3 SIMP 1
4. (Ax)(Ay)(Az)[CON x y -> CON x z | CON y z] Ax1.6 SIMP 1
5. (Ax)(Ay)[CON x y -> DILN x y] New Ax SIMP 1
6. CON v1 v2 ASSUMED-PREMISE
7. ~DILN v2 v3 ASSUMED-PREMISE
8. (Ay)[CON v1 y -> DILN v1 y] US (v1 x) 5
9. (Ay)(Az)[CON v1 y -> CON v1 z | CON y z] US (v1 x) 4
10. (Ay)[CON v2 y -> DILN v2 y] US (v2 x) 5
11. CON v1 v1 -> DILN v1 v1 US (v1 y) 8
12. ~CON v1 v1 CASE2 11
13. DILN v1 v1 CASE1 11
14. ~CON v1 v1 US (v1 x) 3
15. (Ay)(Az)[CON v2 y -> CON v2 z | CON y z] US (v2 x) 4
16. (Az)[CON v1 v2 -> CON v1 z | CON v2 z] US (v2 y) 9
17. CON v2 v3 -> DILN v2 v3 US (v3 y) 10
18. ~CON v2 v3 MT 17 7
19. CON v1 v2 -> CON v1 v1 | CON v2 v1 US (v1 z) 16
20. CON v1 v1 | CON v2 v1 MP 19 6
21. CON v2 v1 LDS 20 14
22. (Az)[CON v2 v1 -> CON v2 z | CON v1 z] US (v1 y) 15
23. ~DILN v1 v1 US (v1 x) 2
24. CON v2 v1 -> CON v2 v3 | CON v1 v3 US (v3 z) 22
25. CON v2 v3 | CON v1 v3 MP 24 21
26. CON v1 v3 LDS 25 18
27. CON v1 v3 ~-ELIMINATION 13 23
28. CON v1 v3 SAME 26
29. CON v1 v3 CASES 11 28 27
30. ~DILN v2 v3 -> CON v1 v3 CP 29
31. DILN v2 v3 | CON v1 v3 IMP 30
32. CON v1 v2 -> DILN v2 v3 | CON v1 v3 CP 31
33. (Ax)(Ay)(Az)[CON x y -> DILN y z | CON x z] UG 32
34. 14 axioms of new axiomatization for apartness geometry
-> (Ax)(Ay)(Az)[CON x y -> DILN y z | CON x z] CP 33
Appendix 2
From Axiom 1.6 and the new axiom, we infer the third axiom of compatibility of equality with apartness and convergence.
The proof has 19 steps, and the time consumed on SPARCstation-10 is 2 seconds.
Solution
1. (Ax)(Ay)(Az)[CON x y -> CON x z | CON y z]
& (Ax)(Ay)[CON x y -> DILN x y] ASSUMED-PREMISE
2. (Ax)(Ay)(Az)[CON x y -> CON x z | CON y z] SIMP 1
3. (Ax)(Ay)[CON x y -> DILN x y] SIMP 1
4. CON v1 v2 ASSUMED-PREMISE
5. ~DILN v2 v3 ASSUMED-PREMISE
6. (Ay)(Az)[CON v1 y -> CON v1 z | CON y z] US (v1 x) 2
7. (Ay)[CON v2 y -> DILN v2 y] US (v2 x) 3
8. (Az)[CON v1 v2 -> CON v1 z | CON v2 z] US (v2 y) 6
9. CON v2 v3 -> DILN v2 v3 US (v3 y) 7
10. ~CON v2 v3 MT 9 5
11. CON v1 v2 -> CON v1 v3 | CON v2 v3 US (v3 z) 8
12. CON v1 v3 | CON v2 v3 MP 11 4
13. CON v1 v3 RDS 12 10
14. CON v1 v3 SAME 13
15. ~DILN v2 v3 -> CON v1 v3 CP 14
16. DILN v2 v3 | CON v1 v3 IMP 15
17. CON v1 v2 -> DILN v2 v3 | CON v1 v3 CP 16
18. (Ax)(Ay)(Az)[CON x y -> DILN y z | CON x z] UG 17
19. (Ax)(Ay)(Az)[CON x y -> CON x z | CON y z]
& (Ax)(Ay)[CON x y -> DILN x y]
-> (Ax)(Ay)(Az)[CON x y -> DILN y z | CON x z] CP 18