- Bliksem 1.10
- E 0.5
- E-SETHEO csp99 and E-SETHEO-FLOTTER csp99
- FDP 0.9
- Fiesta 2
- Gandalf c-1.8c (CASC-15 MIX Division winner)
- HOTTER 0.0
- MUSCADET v2.1
- Otter-MACE 437
- SCOTT IV
- SSCPA 1999.6
- SPASS 0.95TPTP (CASC-15 FOF and SAT Division winner)
- SPASS 1.0.0TPTP
- Vampire 0.0
- Waldmeister 798 (CASC-15 UEQ Division winner)
- Waldmeister 799

Max-Planck-Institut für Informatik

nivelle@mpi-sb.mpg.de

In the automode Bliksem 1.10 is able to recognize decidable classes. However these are unlikely to show up in the competition. Apart from that, the automode is still quite primitive. We don't know how to select the right strategy + order.

Bliksem 1.00 has had soundness problems. We believe that there is no way in which the correctness of a program with the complexity of Bliksem can be guaranteed. We do not give any such guarantees for Bliksem 1.10. Instead Bliksem 1.10 is able to output its proofs with such a level of specification that they can be easily checked by another computer program. In the future we plan to have the proofs checked by a type checker, namely COQ [BB+96].

http://www.mpi-sb.mpg.de/~nivelle

- BG90
- Bachmair L., Ganzinger H. (1990),
**On Restrictions of Ordered Paramodulation with Simplification**, Stickel M.E.,*Proceedings of the 10th International Conference on Automated Deduction*(Kaiserslautern, Germany), pp.427-441, Lecture Notes in Artificial Intelligence 449, Springer-Verlag. - BB+96
- Barras B. et al (1996),
**The COQ Proof Assistent Reference Manual**, Version 6.1, INRIA, Nancy, France. - DeN49
- DeNivelle H. (1994),
**Resolution Games and Non-Liftable Resolution Orderings**, Pacholski L., Tiuryn J.,*Computer Science Logic*, pp.279-293, Springer-Verlag. - Den98
- DeNivelle H. (1998),
**A Resolution Decision Procedure for the Guarded Fragment**, Kirchner C., Kirchner H.,*Proceedings of the 15th International Conference on Automated Deduction*(Lindau, Germany), pp.191-204, Lecture Notes in Artificial Intelligence 1421, Springer-Verlag. - FL+93
- Fermüller C., Leitsch A., Tammet T., Zamov N. (1993),
**Resolution Methods for the Decision Problem**, Lecture Notes in Computer Science 679, Springer-Verlag. - Rob65
- Robinson J.A. (1965),
**A Machine-Oriented Logic Based on the Resolution Principle**,*Journal of the ACM*12(1), pp.23-41.

Institut für Informatik, Technische Universität München

schulz@informatik.tu-muenchen.de

The calculus used by E combines superposition [BG94]
(with selection of negative literals) and rewriting. For the special case
that only unit clauses are present, this calculus degenerates into
*unfailing completion* [BDP89]. For the
Horn case, E can simulate variants of the positive unit strategy described
in [Der91]. No special rules for non-equational
literals have been implemented, i.e., resolution is simulated via
paramodulation and equality resolution.

Proof search in E is controlled by a literal selection strategy and an
evaluation heuristic. A variety of selection strategies (including
e.g., *no selection*, or *select all negative literals*) is
available. Evaluation heuristics can be constructed on the fly by
combining various parameterized primitive evaluation functions. We
also aim at including some learning heuristics into the prover by the
competition date. A simple automatic mode can select strategy and
heuristic based on simple problem characteristics.

The program has been successfully installed under SunOS 4.3.x, Solaris 2.x, HP-UX B 10.20, and various versions of Linux. Sources are available freely from:

http://wwwjessen.informatik.tu-muenchen.de/~schulz/WORK/eprover.html

- BDP89
- Bachmair L., Dershowitz N., Plaisted D.A. (1989),
**Completion Without Failure**, Ait-Kaci H., Nivat M.,*Resolution of Equations in Algebraic Structures*, pp.1-30, Academic Press. - BG94
- Bachmair L., Ganzinger H. (1994),
**Rewrite-Based Equational Theorem Proving with Selection and Simplification**,*Journal of Logic and Computation*4(3), pp.217-247. - Der91
- Dershowitz N. (1991),
**Ordering-Based Strategies for Horn Clauses**, Mylopolous J., Reiter R.,*Proceedings of the 12th International Joint Conference on Artificial Intelligence*(Sydney, Australia), pp.118-124, Morgan-Kaufmann. - MI+97
- Moser M., Ibens O., Letz R., Steinbach J., Goller C., Schumann J.,
Mayr K. (1997),
**SETHEO and E-SETHEO: The CADE-13 Systems**,*Journal of Automated Reasoning*18(2), pp.237-246. - Sch99
- Schulz S. (1999),
**System Abstract: E 0.3**, Ganzinger H.,*Proceedings of the 16th International Conference on Automated Deduction*(Trento, Italy), Lecture Notes in Artificial Intelligence, Springer-Verlag.

Institut für Informatik, Technische Universität München

{letz,schulz,stenzg,wolfa}@informatik.tu-muenchen.de

E-SETHEO-FLOTTER includes the program FLOTTER [WGR96] as a preprocessing module for transforming non-clausal formulae to clausal form.

On the top level, the system performs a parallelization of different
strategies stemming from the system P-SETHEO
[Wol98a]. In contrast to
P-SETHEO, in the version 99csp of E-SETHEO, the different strategies
are run sequentially, one after the other, depending on the allocation
of resources to the different strategies, so-called *schedules*.
A schedule is determined from rough syntactic
characteristics of the input formula (e.g., if it is a Horn formula
without equality).
The schedules have been computed from a large number of experimental
data using a combination of a genetic algorithm
[SW99]
and a gradient procedure [Wol98b].

The program runs under Solaris 2.6. Sources are available freely.

- MI+97
- Moser M., Ibens O., Letz R., Steinbach J., Goller C., Schumann J.,
Mayr K. (1997),
**SETHEO and E-SETHEO: The CADE-13 Systems**,*Journal of Automated Reasoning*18(2), pp.237-246. - Sch99
- Schulz S. (1999),
**System Abstract: E 0.3**, Ganzinger H.,*Proceedings of the 16th International Conference on Automated Deduction*(Trento, Italy), Lecture Notes in Artificial Intelligence, Springer-Verlag. - SW99
- Stenz G., Wolf A. (1999),
**Strategy Selection by Genetic Programming**, Kumar A., Russell I.,*Proceedings of the 12th Florida Artificial Intelligence Research Symposium*(Orlando, USA), pp.346-350, AAAI Press. - WGR96
- Weidenbach C., Gaede B., Rock G. (1996),
**SPASS and FLOTTER**, McRobbie M., Slaney J.K.,*Proceedings of the 13th International Conference on Automated Deduction*(New Brunswick, USA), pp.141-145, Lecture Notes in Artificial Intelligence 1104, Springer-Verlag. - Wol98a
- Wolf A. (1998),
**p-SETHEO: Strategy Parallelism in Automated Theorem Proving**, de Swart H.,*Proceedings of International Conference TABLEAUX'98: Analytic Tableaux and Related Methods*(Oisterwijk, The Netherlands), pp.320-324, Lecture Notes in Artificial Intelligence 1397, Springer-Verlag. - Wol98b
- Wolf A. (1998),
**Strategy Selection for Automated Theorem Proving**, Giunchiglia F.,*Proceedings of the 8th International Conference on Artificial Intelligence: Methodology, Systems, Applications (AIMSA)*(Sozopol, Bulgaria), pp.452-465, Lecture Notes in Artificial Intelligence 1480, Springer-Verlag.

Institute for Computer Science, University of Koblenz-Landau

peter@uni-koblenz.de

The model construction technique is similar to the one of the predecessor calculus "Hyper Tableaux - The Next Generation" described in [Bau98]. Since there is no paper on FDP yet, this is the only relevant publication so far.

Proof search in FDP can be semantically guided by supplying an "initial interpretation", and proof search means to modify this initial interpretation until success. By default, a "trivial" initial interpretation is used that assign true to all positive literals. This emphasizes the role of negative clauses.

There is no built-in equality-handling (yet!) and so far FDP is restricted to clausal logic without equality. Currently, equality is treated in a preprocessing transformation similar to Brand's well-known STE-transformation.

The current implementation is available through the WWW at:

http://www.uni-koblenz.de/~peter/FDP/

Comments etc. are highly welcome!

In the MIX division, I expect better performance for non-equality problems than for equality problems, and better performance for non-Horn problems than for Horn problems.

FDP decides function-free clause logic. Many SAT problems are of this kind. Therefore, FDP participates in the SAT division as well.

- Bau98
- Baumgartner P. (1998),
**Hyper Tableaux - The Next Generation**, de Swart H.,*Automated Reasoning with Analytic Tableaux and Related Methods: Proceedings of TABLEAUX'98*(Oisterwijk, The Netherlands), pp.60-76, Lecture Notes in Computer Science 1397, Springer-Verlag.

Technical University of Catalonia (UPC)

roberto@lsi.upc.es

The main characteristic of this system is that it does not adjust any system parameters according to the given axiom set or conjecture. This is of course not realistic w.r.t. real-world applications. But we want to make the point that we strongly believe that this is also the case for the other extreme, i.e., applying specific strategies (for very small problem sets), discovered by studying proofs obtained by running (sometimes several) provers on the competition problem set without any time limit. This of course gives no real information either about the behaviour of a prover in a five-minutes run on a new problem.

The following are the fixed settings used at the competition (but of course this does not mean that the prover includes no other orderings or selection strategies; all system parameters can be set in a flexible way):

Fiesta always uses a lexicographic path ordering with a precedence where symbols are first compared by arity (a larger arities means larger in the precedence) and second by order of appearance in the input.

The selection of the next rule used for superposition consists of picking every three cycles once the oldest one, and twice the smallest one according to the size measure where symbols are counted as their arity plus one, and variables as one.

The system has a self-adjusting policy for deleting too large equations: initially the weight limit is small (27), but each time completion terminates without a proof, it restarts with the limit incremented by four (hence this policy is not a source of incompleteness).

If a proof is found, it is output in a format readible by our Prolog proof checker.

Terms sometimes carry additional marks used for indicating that they are in normal form, or as an index in an LPO-cache that avoids the repeated comparision of the same terms with LPO. This is quite useful for rewriting with rules that are not orientable a priori, which is done eagerly.

We believe however, that the performance of Fiesta at the competition will give some evidence for the fact that with such a table we could prove most if not all problems.

Department of Computer Science, University of Göteborg

tammet@cs.chalmers.se

The basic idea of the automatic mode in Gandalf - also used during the CASC-14 competition - is time-slicing: Gandalf selects a set of different search strategies, allocates time to these and finally runs the strategies one after another.

The selection of strategies and the percentage of time they receive is in a somewhat ad hoc way based on the characteristics of the problem: percentage of Horn and almost-Horn clauses, the number of clauses, percentage of clauses where literals can be ordered using term and variable depths.

There exist also versions of Gandalf for intuitionistic logic and type theory, see [Tam96] and [TS96]. More information about Gandalf can be found in [Tam98].

The source, binaries, manual and other materials are available at:

http://www.cs.chalmers.se/~tammet/gandalf/

Gandalf is likely to do well in the UEQ, SAT and FOF categories, although it is unlikely it will win any of these.

- Tam98
- Tammet T. (1998),
**Towards Efficient Subsumption**, Kirchner C., Kirchner H.,*Proceedings of the 15th International Conference on Automated Deduction*(Lindau, Germany), Lecture Notes in Artificial Intelligence, Springer-Verlag. - Tam96
- Tammet T. (1996),
**A Resolution Theorem Prover for Intuitionistic Logic**, McRobbie M., Slaney J.K.,*Proceedings of the 13th International Conference on Automated Deduction*(New Brunswick, USA), pp.2-16, Lecture Notes in Artificial Intelligence 1104, Springer-Verlag. - TS96
- Tammet T., Smith J. (1996),
**Optimised Encodings of Fragments of Type Theory in First Order Logic**, Berardi S., Coppo M.,*Types for Proofs and Programs: Proceedings of the International Workshop TYPES'95*(Torino, Italy), pp.265-287, Lecture Notes in Artificial Intelligence 1158, Springer-Verlag.

Department of Computer Science, University of Iowa

hzhang@cs.uiowa.edu

The model generation method is a new method [Zh99] which represents models by rewrite rules. SATO [Zh97], an implementation of the Davis-Putnam method, is also built into HOTTER as a decision procedure for the propositional logic.

For the SAT problems, McCune's MACE [McC98b] is used to test if the input clauses have small finite models. If it does not have, HOTTER takes it over.

- HS99
- Hodgson K., Slaney J.K. (1999),
**Semantic guidance with SCOTT**, Technical Report TR-ARP-01-99, Automated Reasoning Project, Australian National University, Canberra, Australia. - MW97
- McCune W.W., Wos L. (1997),
**Otter: The CADE-13 Competition Incarnations**,*Journal of Automated Reasoning*18(2), pp.211-220. - McC94
- McCune W.W. (1994),
**Otter 3.0 Reference Manual and Guide**, Technical Report ANL-94/6, Argonne National Laboratory, Argonne, USA. - McC98a
- McCune W.W. (1998),
**Otter: An Automated Deduction System**, http://www.mcs.anl.gov/home/mccune/ar/otter/. - McC98b
- McCune W.W. (1998),
**MACE: Models and Counterexamples**, http://www.mcs.anl.gov/home/mccune/ar/mace/. - Zha97
- Zhang H. (1997),
**SATO: an Efficient Propositional Prover**, http://www.cs.uiowa.edu/~hzhang/sato/. - Zha99
- Zhang H. (1999),
**Automated Construction of Rewrite Rule Models**, http://www.cs.uiowa.edu/~hzhang/model/.

Université René Descartes (Paris 5), UFR de Mathématiques et Informatique

pastre@math-info.univ-paris5.fr

Methods are those used by humans, and are executed according to a plan decided by metarules and heuristics. Methods include splitting theorems into two or more subtheorems (conjonctive conclusion or disjunctive hypotheses), treatment of universal, existential or disjunctive conclusion, treatment of existential or disjunctive hypotheseses (one at a time when it is decided (by heuristic rules), replacement of the conclusion by its definition. Hypotheses are never replaced by their definition. Instead, rules are built by metarules from definitions and used to deduce new hypotheses from old ones. Universal hypotheses are not added. Instead, rules are built as from the definitions. Functional symbols may be used, but an automatic creation of intermediate objects allows to flatten deep subformulae and treat them as if concepts were defined by predicate symbols. Positive properties are privileged, in hypotheses and in conclusion. So, a special treatment of negation is done. The successive steps of a proof may be forward deduction (deduce new hypotheses from old ones), backward deduction (replace the conclusion by a new one) or refutation (only if the conclusion is a negation).

The system is also able to work with second order statements. It may also receive knowledge and know-how for a specific domain from a human user; see [Pas89] and [Pas93]. These two possibilities are not used while working with the TPTP Library.

- Ble71
- Bledsoe W.W. (1971),
**Splitting and Reduction Heuristics in Automatic Theorem Proving**,*Artificial Intelligence*2, pp.55-77. - Pas78
- Pastre D. (1978),
**Automatic Theorem Proving in Set Theory**,*Artificial Intelligence*10, pp.1-27. - Pas89
- Pastre D. (1989),
**MUSCADET : An Automatic Theorem Proving System using Knowledge and Metaknowledge in Mathematics**,*Artificial Intelligence*38, pp.257-318. - Pas93
- Pastre D. (1993),
**Automated Theorem Proving in Mathematics**,*Annals of Mathematics and Artificial Intelligence*8, pp.425-447.

Mathematics and Computer Science, Argonne National Laboratory

mccune@mcs.anl.gov

- MW97
- McCune W.W., Wos L. (1997),
**Otter: The CADE-13 Competition Incarnations**,*Journal of Automated Reasoning*18(2), pp.211-220. - McC94
- McCune W.W. (1994),
**Otter 3.0 Reference Manual and Guide**, Technical Report ANL-94/6, Argonne National Laboratory, Argonne, USA. - McC98a
- McCune W.W. (1998),
**Otter: An Automated Deduction System**, http://www.mcs.anl.gov/home/mccune/ar/otter/. - McC98b
- McCune W.W. (1998),
**MACE: Models and Counterexamples**, http://www.mcs.anl.gov/home/mccune/ar/mace/.

Automated Reasoning Project, Australian National University

{kahlil, jks}@arp.anu.edu.au

Unlike previous versions [Sla93,SLM94], the current version of SCOTT searches for maximally consistent subsets much more aggressively, and manages the cost of this much more intelligently. Most importantly, however, our naïve notions of semantic guidance have been superseded by those with genuine theoretical support. In addition, semantic resolution has been tentatively implemented and, provided it can be made sufficiently stable, will be incorporated in the competition version.

- HS99
- Hodgson K., Slaney J.K. (1999),
**Semantic guidance with SCOTT**, Technical Report TR-ARP-01-99, Automated Reasoning Project, Australian National University, Canberra, Australia. - McC94
- McCune W.W. (1994),
**Otter 3.0 Reference Manual and Guide**, Technical Report ANL-94/6, Argonne National Laboratory, Argonne, USA. - SLM94
- Slaney J.K., Lusk E., McCune W.W. (1994),
**SCOTT: Semantically Constrained Otter, System Description**, Bundy A.,*Proceedings of the 12th International Conference on Automated Deduction*(Nancy, France), pp.764-768, Lecture Notes in Artificial Intelligence 814, Springer-Verlag. - Sla93
- Slaney J.K. (1993),
**SCOTT: A Model-Guided Theorem Prover**, Bajcsy R.,*Proceedings of the 13th International Conference on Artificial Intelligence*(Chambery, France), pp.109-114, Morgan-Kaufman. - Sla94
- Slaney J.K. (1994),
**FINDER: Finite Domain Enumerator, System Description**, Bundy A.,*Proceedings of the 12th International Conference on Automated Deduction*(Nancy, France), pp.798-801, Lecture Notes in Artificial Intelligence 814, Springer-Verlag.

Department of Computer Science, James Cook University

geoff@cs.jcu.edu.au

The choice of what syntactic characteristics are used to form the SPCs is based on community input and analysis of system performance data. Performance data for the available ATP systems, for problems in the TPTP [SS98], is used to evaluate the systems within each SPC.

SSCPA has five modes of operation, which differ in terms of systems
chosen, CPU allocation to each system, CPU priority for each system,
and start time for each system.
In CASC-16 SSCPA will run the *eager* mode, which uses three or
four recommended systems, CPU allocation halving from the time limit,
equal CPU priority, and all systems starting together.

http://www.cs.jcu.edu.au/cgi-bin/tptp/SystemOnTPTPFormMaker

- SS99a
- Sutcliffe G., Seyfang D. (1999),
**Smart Selective Competition Parallelism ATP**, Kumar A., Russell I.,*Proceedings of the 12th Florida Artificial Intelligence Research Symposium*(Orlando, USA), pp.341-345, AAAI Press. - SS98
- Sutcliffe G., Suttner C.B. (1998),
**The TPTP Problem Library: CNF Release v1.2.1**,*Journal of Automated Reasoning*21(2), pp.177-203. - SS99b
- Sutcliffe G., Suttner C.B. (1999),
**The CADE-15 ATP System Competition**,*Journal of Automated Reasoning*.

Max-Planck-Institut für Informatik

weidenb@mpi-sb.mpg.de

The splitting rule splits clauses, if possible, into variable disjoint parts that can be independently refuted. This rule is not necessary for completeness of the calculus but it makes SPASS an efficient decision procedure for several decidable subclasses of first-order logic [HS97].

We put a lot of effort in a clause normal form translation that produces small clause normal forms. The major techniques are renaming and improved Skolemization [NRW98].

The SPASS distribution containing the source code for SPASS is freely available from the SPASS homepage. The code should compile and run on any machine where the usual GNU tools are available. This has been tested on SUN Sparc workstations under Solaris and SunOS, on personal computers under Linux and Solaris and on Dec Alpha workstations under Digital Unix.

- GMW97
- Ganzinger H., Meyer C., Weidenbach C. (1997),
**Soft Typing for Ordered Resolution**, McCune W.W.,*Proceedings of the 14th International Conference on Automated Deduction*(Townsville, Australia), pp.321-335, Lecture Notes in Artificial Intelligence 1249, Springer-Verlag. - HS97
- Hustadt U., Schmidt R.A. (1997),
**On Evaluating Decision Procedures for Modal Logics**, Pollack M.E.,*Proceedings of the 15th International Joint Conference on Artificial Intelligence*(Nagoya, Japan), pp.202-207. - NRW98
- Nonnengart A., Rock G., Weidenbach C. (1998),
**On Generating Small Clause Normal Forms**, Kirchner C., Kirchner H.,*Proceedings of the 15th International Conference on Automated Deduction*(Lindau, Germany), Lecture Notes in Artificial Intelligence, Springer-Verlag. - Wei97
- Weidenbach C. (1997),
**SPASS: Version 0.49**,*Journal of Automated Reasoning*2(18), pp.247-252. - Wei98
- Weidenbach C. (1998),
**Sorted Unification and Tree Automata**, Bibel W., Schmitt P.H.,*Automated Deduction, A Basis for Applications*, Kluwer Academic Publishers.

Max-Planck-Institut für Informatik

weidenb@mpi-sb.mpg.de

The prover is available for many platforms, in particular, we now also provide a Windows 95/98/NT version including a neat graphical user interface.

- AO93
- Antoniou G., Ohlbach H-J. (1983),
**Terminator**, Bundy A.,*Proceedings of the 8th International Joint Conference on Artificial Intelligence*(Karlsruhe, Germany), pp.916-919. - WA+99
- Weidenbach C., Afshordel B., Brahm U., Cohrs C., Engel T., Keen E.,
Theobalt C., Tpoic D. (1999),
**System Description: SPASS Version 1.0.0**, Ganzinger H.,*Proceedings of the 16th International Conference on Automated Deduction*(Trento, Italy), Lecture Notes in Artificial Intelligence, Springer-Verlag. - Wei99
- Weidenbach C. (1999),
**SPASS: Combining Superposition, Sorts and Splitting**, Robinson A., Voronkov A.,*Handbook of Automated Reasoning*, Elsevier Science.

Computer Science Department, The University of Manchester

{riazanoa,voronkov}@cs.man.ac.uk

- Gra96
- Graf P. (1996),
**Term Indexing**, Lecture Notes in Computer Science 1053, Springer-Verlag. - McC92
- McCune W.W. (1992),
**Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval**,*Journal of Automated Reasoning*9(2), pp.147-167. - McC94
- McCune W.W. (1994),
**Otter 3.0 Reference Manual and Guide**, Technical Report ANL-94/6, Argonne National Laboratory, Argonne, USA. - RSV99
- Ramakrishnan I.V., Sekar R., Voronkov A. (1999),
**Term Indexing**, Robinson A., Voronkov A.,*Handbook of Automated Reasoning*, Elsevier Science. - Sti89
- Stickel M.E. (1989),
**The Path Indexing Method for Indexing Terms**, Technical Note 473, SRI International, Menlo Park, USA. - Vor95
- Voronkov A. (1995),
**The Anatomy of Vampire**,*Journal of Automated Reasoning*15(2), pp.237-265.

FB Informatik, Universität Kaiserslautern

{hillen,jaeger,loechner}@informatik.uni-kl.de,arnim.buch@sdm.de

The main completion loop is parameterized by a selection heuristic and a reduction ordering. Both are derived from the algebraic structure described by the axioms. Since last year, the derivation process has been lifted such that control knowledge is expressed declaratively, which eases the integration of human experience. For full flexibility, the search parameters may be re-instantiated during the proof search.

Recently, we also realized a database-driven mechanism which allows simple extensions of the underlying inference calculus, e.g. for reasoning on Horn clauses as described in [BDP89:pp.24ff].

To incorporate goal orientation into the completion procedure, the hypotheses are blown up to sets of rewrite successors and sometimes predecessors. A step-by-step proof object is constructed at run-time.

Our ATP system is implemented in ANSI-C and runs under Sun-OS, Solaris and Linux. The Waldmeister distribution contains an easy-to-use version along with documentation material and problem sets. If you are interested in tackling problems with Waldmeister, just send an e-mail to the authors.

- BDP89
- Bachmair L., Dershowitz N., Plaisted D.A. (1989),
**Completion Without Failure**, Ait-Kaci H., Nivat M.,*Resolution of Equations in Algebraic Structures*, pp.1-30, Academic Press. - BH96
- Buch A., Hillenbrand T. (1996),
**Waldmeister: Development of a High Performance Completion-Based Theorem Prover**, SEKI-Report SR-96-01, AG Effiziente Algorithmen, Universitaet Kaiserslautern, Kaiserslautern, Germany. - HB+97
- Hillenbrand T., Buch A., Vogt R., Löchner B. (1997),
**Waldmeister: High Performance Equational Deduction**,*Journal of Automated Reasoning*18(2), pp.265-270.

FB Informatik, Universität Kaiserslautern

{hillen,jaeger,loechner}@informatik.uni-kl.de,arnim.buch@sdm.de

This year's version of our unit equality theorem prover is in most parts identical to Waldmeister 798 that won the CASC-15 UEQ competition with an enormous lead [SS99]. Since last year's description is included in this collection we will only report on the differences here.

Recently, Waldmeister has successfully been integrated into the Omega proof development environment [BC+97]. Moreover, we have established a convenient WWW interface that is reachable via:

http://www-avenhaus.informatik.uni-kl.de/waldmeisterFrom this URL further documents and the complete Waldmeister distribution containing an easy-to-use version together with problems and a manual are available.

- BDP89
- Bachmair L., Dershowitz N., Plaisted D.A. (1989),
**Completion Without Failure**, Ait-Kaci H., Nivat M.,*Resolution of Equations in Algebraic Structures*, pp.1-30, Academic Press. - BC+97
- Benzmüller C., Cheikhrouhou L., Fehrer D., Fiedler A., Huang X.,
Kerber M., Kohlhase M., Konrad K., Meier A., Melis E., Schaarschmidt W.,
Siekmann J., Sorge V. (1997),
**OMEGA: Towards a Mathematical Assistant**, McCune W.W.,*Proceedings of the 14th International Conference on Automated Deduction*(Townsville, Australia), pp.146-160, Lecture Notes in Artificial Intelligence 1249, Springer-Verlag. - HJL99
- Hillenbrand T., Jaeger A., Löchner B. (1999),
**Waldmeister - Improvements in Performance and Ease of Use**, Ganzinger H.,*Proceedings of the 16th International Conference on Automated Deduction*(Trento, Italy), Lecture Notes in Artificial Intelligence, Springer-Verlag. - SS99
- Sutcliffe G., Suttner C.B. (1999),
**The CADE-15 ATP System Competition**,*Journal of Automated Reasoning*.