- Darwin 1.3
- FM-Darwin 1.3
- DCTP 10.21p (CASC-20 EPR division winner)
- E and EP 0.99
- Equinox 1.0
- Faust 1.0
- Geo 2006i
- iProver 0.1
- MathServe 0.80
- Muscadet 2.6
- Octopus 2006
- Otter 3.3
- Paradox 1.3 (CASC-20 SAT division winner)
- Paradox 2.0
- Theo 2006
- Vampire 8.0 (CASC-20 MIX and FOF divisions winner)
- Vampire 8.1
- Waldmeister 704 (CASC-20 UEQ division winner)
- Waldmeister 806

The current version of Darwin implements first-order versions of unit propagation inference rules analogously to a restricted form of unit resolution and subsumption by unit clauses. To retain completeness, it includes a first-order version of the (binary) propositional splitting inference rule.

Proof search in Darwin starts with a default interpretation for a given clause set, which is evolved towards a model or until a refutation is found.

Improvements to the previous version include additional preprocessing steps, less memory requirements, and lemma learning [BFT06b].

Darwin is implemented in OCaml and has been tested under various Linux distributions. It is available from:

http://goedel.cs.uiowa.edu/Darwin/

The system tries to find a finite domain model for sizes 1,2,.. by equisatisfiable preserving transformation into corresponding function-free clause sets, which are decided by the Darwin prover [BFT06a].

FM-Darwin operates similarly to the finite model finder Paradox [CS03]. Unlike Paradox, it is not based on reduction to propositional satisfiability problems, but on reduction to satisfiability problems of (not necessarily ground) function-free clause sets instead.

Similar to Paradox FM-Darwin uses clause splitting, term definitions, static symmetry reduction, sort inference, and lemmas. In constrast, clause splitting and term definitions are only applied in a restricted way, that is for variable disjunct clause and ground terms, as ground instantiation is not performed and thus the exponential increase in the size of the clause set does not happen.

FM-Darwin is available from:

http://goedel.cs.uiowa.edu/Darwin/

Like Paradox, FM-Darwin is a complete method for function-free clause sets, and can also detect unsatisfiability if the totality axioms are not used in a refutation.

Technische Universität München, Germany

DCTP 10.21p is a strategy parallel version using the technology of E-SETHEO [SW99] to combine several different strategies based on DCTP 1.31.

We are currently integrating a range of new techniques into DCTP which are mostly based on the results described in [LS04], as well as a certain form of unit propagation. We are hopeful that these improvements will be ready in time for CASC-J2.

Institut für Informatik, Technische Universität, Germany

E is based on the DISCOUNT-loop variant of the *given-clause*
algorithm, i.e. a strict separation of active and passive facts.
Proof search in E is primarily controlled by a literal selection
strategy, a clause evaluation heuristic, and a simplification
ordering. The prover supports a large number of preprogrammed literal
selection strategies, many of which are only experimental. Clause
evaluation heuristics can be constructed on the fly by combining
various parameterized primitive evaluation functions, or can be
selected from a set of predefined heuristics. Supported term orderings
are several parameterized instances of Knuth-Bendix-Ordering (KBO) and
Lexicographic Path Ordering (LPO).

The prover uses a preprocessing step to convert formulas in full first order format to clause normal form. This step may introduce (first-order) definitions to avoid an exponential growth of the formula. Preprocessing also unfolds equational definitions and performs some simplifications on the clause level.

The automatic mode determines literal selection strategy, term ordering, and search heuristic based on simple problem characteristics of the preprocessed clausal problem.

EP 0.99 is just a combination of E 0.99 in verbose mode and a proof analysis tool extracting the used inference steps.

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

EP 0.99 is a simple Bourne shell script calling E and the postprocessor in a pipeline.http://www.eprover.org

E distinguishes problem classes based on a number of features, all of which have between 2 and 4 possible values. The most important ones are:

- Is the most general non-negative clause unit, Horn, or Non-Horn?
- Is the most general negative clauce unit or non-unit?
- Are all negative clauses unit clauses?
- Are all literals equality literals, are some literas equality literals, or is the problem non-equational?
- Are there a few, some, or many clauses in the problem?
- Is the maximum arity of any function symbol 0, 1, 2, or greater?
- Is the sum of function symbol arities in the signature small, medium, or large?

For classes above a threshold size, we assign the absolute best heuristic to the class. For smaller, non-empty classes, we assign the globally best heuristic that solves the same number of problems on this class as the best heuristic on this class does. Empty classes are assigned the globally best heuristic. Typically, most selected heuristics are assigned to more than one class.

EP 0.99 will be hampered by the fact that it has to analyse the
inference step listing, an operation that typically is about as
expensive as the proof search itself. Nevertheless, it should be
competitive among the CNF^{*} and FOF^{*} systems.

Chalmers University of Technology, Sweden

- Give all ground clauses in the problem to a SAT solver.
- Run the SAT-solver.
- If a contradiction is found, we have a proof and we terminate.
- If a model is found, we use the model to indicate which new ground instantiations should be added to the SAT-solver.
- Goto 2.

University of Miami, USA

- Kernel that functions as a persistent storage of inferences, provides indexing, implementation of all the inference rules and simplifications, and engages strategies built on top of it in a non-intrusive, transparent interaction.
- Individual strategies
- Strategy Manager that examines the problem, splits it into subproblems and chooses the most appropriate strategy for each.

The website for the project is at this address:

http://umsis.miami.edu/~ypuzis/FAUST-AutomatedTheoremProver.html

- Putting each negated conjecture clause into individual subproblem.
- Augmenting each subset with axioms that pass the pure literal deletion test (with respect to clauses in the subproblem).
- Choosing an appropriate strategy and ordering method for each subproblem (based on, for example, presence or absence of equality clauses).

- Performing subsumption against inferences obtained from all threads.
- Inferences done once (including by a different thread) are never redone.

Forall x1, ..., xn A1 /\ ... /\ Ap /\ v1 != w1 /\ ... /\ vq != wq -> Z(x1,...,xn).The

`Z(x1,...,xn)` must have one of the following three forms:

- The false constant
`FALSE`. - A disjunction
`B1 | ... | Br`. The atoms`Bk`must be non-equality atoms. The arguments of the atoms`Bk`are among the variables`x1, ..., xn`. There are no function symbols, and no constants in the atoms`Bk`. - An existential quantification
`EXISTS y B`.`y`is a variable distinct from`x1,...,xn`.`B`is an atom which has all arguments among`x1,...,xn,y`.

During search, Geo searches for a model of the geometric formulas by backtracking. At each choice point, after all subbranches have been refuted, it derives a new rule of Type 1, which refutes the current model attempt without backtracking. In this way, Geo learns during backtracking.

In case Geo finds a finite model, it simply prints the model. In case no
model exists, it will eventually learn the rule `-> FALSE`,
so that it is able to output a refutation proof.

The final aim of geometric resolution, and of Geo, is to obtain a prover that is both good at finding proofs, and at finding finite models.

The University of Manchester, England

Universität des Saarlandes, Germany

MathServe currently integrates the ATP systems Otter 3.3, EP 0.91, SPASS 2.2 and Vampire 8.0. All ATP services get a problem description in the new TPTP format (TPTP Library v3.1.1) and a time limit in seconds as an input. The problem is transformed into the provers' input format using the tptp2X utility. The result specifies the status of the given problem with one of the statuses defined in the SZS Status Ontology [SZS04].

Since MathServe does not form an ATP system on its own it only enters the Demonstration Division of the CASC.

Université René Descartes (Paris 5), France

http://www.math-info.univ-paris5.fr/~pastre/muscadet/muscadet.html

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, Pas93]. These two possibilities are not used while working with the TPTP Library.

McGill University, Canada

Argonne National Laboratory, USA

Otter 3.3 [McC03a] is an ATP system for statements in first-order (unsorted) logic with equality. Otter is based on resolution and paramodulation applied to clauses. An Otter search uses the "given clause algorithm", and typically involves a large database of clauses; subsumption and demodulation play an important role.

Otter is written in C. Otter uses shared data structures for clauses and terms, and it uses indexing for resolution, paramodulation, forward and backward subsumption, forward and backward demodulation, and unit conflict. Otter is available from:

http://www-unix.mcs.anl.gov/AR/otter/

Otter's original automatic mode, which reflects no tuning to the TPTP problems, will be used.

Otter has been entered into CASC as a stable benchmark against which progress can be judged (there have been only minor changes to Otter since 1996 [MW97], nothing that really affects its performace in CASC). This is not an ordinary entry, and we do not hope for Otter to do well in the competition.

*Acknowledgments: Ross Overbeek, Larry Wos, Bob Veroff, and
Rusty Lusk contributed to the development of Otter.*

Chalmers University of Technology and Gothenburg University, Sweden

Paradox incorporates the following features: Polynomial-time
*clause splitting heuristics*, the use of *incremental SAT*,
*static symmetry reduction* techniques, and the use of *sort
inference*.

The main differences with Paradox 1.0 are: a better SAT-solver, better memory behaviour, and a faster clause instantiation algorithm.

- Analyze the problem, finding an upper bound N on the domain size of models, where N is possibly infinite. A finite such upper bound can be found, for example, for EPR problems.
- Flatten the problem, and split clauses and simplify as much as possible.
- Instantiate the problem for domain sizes 1 up to N, applying the SAT solver incrementally for each size. Report "SATISFIABLE" when a model is found.
- When no model of sizes smaller or equal to N is found, report "CONTRADICTION".

Chalmers University of Technology and Gothenburg University, Sweden

See the description of Paradox 1.3 for general information.

McGill University, Canada

When Theo participated in the 2004 CASC Competition, it used a learning strategy [NW04] briefly described in this paragraph. When given a theorem, it first created a list of potential ways to "weaken" the theorem by weakening one of the clauses. It then randomly selected one of the weakenings, tried to prove the weakened version of the theorem, and then used the results from this effort to help prove the given theorem. A weakened version was created by modifying one clause by replacing a constant or function by a variable or by deleting a literal. Certain clauses from the proof of the weakened version were added to the base clauses when Theo next attempted to prove the given theorem. In addition, base clauses that participated in the proof of the weakened version were placed in the set-of-support. Theo then attempted to prove the given theorem with the revised set of base clauses.

The learning strategy was further developed for the 2005 competition as described here. When Theo is given a theorem, it first tries to prove a weakened version. It does this for 50% of the allotted time. If successful, it then attempts to prove the given theorem as described in the previous paragraph. If unsuccessful, however, Theo then weakens the given theorem further by weakening an additional clause. With two clauses now weakened, Theo then attempts to prove the given theorem for 50% of the remaining time (25% of the originally allotted time). If successful, Theo uses the results to attempt to prove the given theorem. If unsuccessful, Theo picks two other weakenings and tries again for 50% of the remaining time. Now certain weakened proofs are thrown out, as they generally seem to be useless. Weakened proofs that are shorter than three inferences are considered useless, as are those that are less than five and do not involve the negated conclusion. Attempts to improve the learning strategy are of major interest in the ongoing development of Theo.

For this 2006 competition, efforts have been made to avoid attempting
certain weakenings in the first place.
These weakenings tend to produce useless proofs. As a trivial example,
weakening `equal(X,X)` to `equal(X,Y)` is highly likely to
produce a trivial proof.
In addition to work on the learning strategy, the procedure for transforming
FOFs to CNF has been improved.

University of Manchester, England

A number of efficient indexing techniques are used to implement all major operations on sets of terms and clauses. Run-time algorithm specialisation is used to accelerate some costly operations, e.g., checks of ordering constraints. Although the kernel of the system works only with clausal normal forms, the shell accepts a problem in the full first-order logic syntax, clausifies it and performs a number of useful transformations before passing the result to the kernel. When a theorem is proved, the system produces a verifiable proof, which validates both the clausification phase and the refutation of the CNF.

- Choice of the main saturation procedure :
- Limited Resource Strategy
- DISCOUNT loop
- Otter loop

- A variety of optional simplifications.
- Parameterised reduction orderings.
- A number of built-in literal selection functions and different modes of comparing literals.
- Age-weight ratio that specifies how strongly lighter clauses are preferred for inference selection.
- Set-of-support strategy.

The automatic mode of Vampire 8.0 is derived from extensive experimental data obtained on problems from TPTP v3.0.1. Input problems are classified taking into account simple syntactic properties, such as being Horn or non-Horn, presence of equality, etc. Additionally, we take into account the presence of some important kinds of axiom, such as set theory axioms, associativity and commutativity. Every class of problems is assigned a fixed schedule consisting of a number of kernel strategies called one by one with different time limits.

Main differences between Vampire 8.0 and 7.0

- a naming technique for a short clause form transformation
- a better Skolemisation algorithm
- the new TPTP input syntax as well as the KIF syntax
- possibility of working with multiple knowledge bases
- a query answering mode
- lexicographic path ordering

University of Manchester, England

No system description supplied. However, see the description of Vampire 8.0 for general information. Minor changes have been made, including a bugfix in the FOF to CNF conversion.

http://www.waldmeister.org

No system description supplied. However, see the description of Waldmeister 704 for general information.

- AHL03
- Avenhaus J., Hillenbrand T., Löchner B. (2003),
**On Using Ground Joinable Equations in Equational Theorem Proving**,*Journal of Symbolic Computation*36(1-2), pp.217-233, Elsevier Science. - 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. - BT03
- Baumgartner P., Tinelli C. (2003),
**The Model Evolution Calculus**, Baader F.,*Proceedings of the 19th International Conference on Automated Deduction*(Miami, USA), pp.350-364, Lecture Notes in Artificial Intelligence 2741, Springer-Verlag. - BFT04
- Baumgartner P., Fuchs A., Tinelli C. (2004),
**Darwin - A Theorem Prover for the Model Evolution Calculus**, Sutcliffe G., Schulz S., Tammet T.,*Proceedings of the Workshop on Empirically Successful First Order Reasoning, 2nd International Joint Conference on Automated Reasoning*(Cork, Ireland). - BFT06a
- Baumgartner P., Fuchs A., Tinelli C. (2006),
**Implementing the Model Evolution Calculus**,*International Journal on Artificial Intelligence Tools*15(1), pp.21-52. - BFT06b
- Baumgartner P., Fuchs A., Tinelli C. (2006),
**Lemma Learning in the Model Evolution Calculus**, Hermann M., Voronkov A.,*Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning*(Phnom Penh, Cambodia), Lecture Notes in Artificial Intelligence. - BF+06
- Baumgartner P., Fuchs A., de Nivelle H., Tinelli C. (2006),
**Computing Finite Models by Reduction to Function-Free Clause Logic**, Ahrendt W., Baumgartner P., de Nivelle H.,*Proceedings of the 3rd Workshop on Disproving - Non-Theorems, Non-Validity, Non-Provability, 3rd International Joint Conference on Automated Reasoning*(Seattle, USA). - Bil96
- Billon J-P. (1996),
**The Disconnection Method: A Confluent Integration of Unification in the Analytic Framework**, Miglioli P., Moscato U., Mundici D., Ornaghi M.,*Proceedings of TABLEAUX'96: the 5th Workshop on Theorem Proving with Analytic Tableaux and Related Methods*(Palermo, Italy), pp.110-126, Lecture Notes in Artificial Intelligence 1071, Springer-Verlag. - Ble71
- Bledsoe W.W. (1971),
**Splitting and Reduction Heuristics in Automatic Theorem Proving**,*Artificial Intelligence*2, pp.55-77. - CS03
- Claessen K., Sorensson N. (2003),
**New Techniques that Improve MACE-style Finite Model Finding**, Baumgartner P., Fermueller C.,*Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications*(Miami, USA). - GK03
- Ganzinger H., Korovin K. (2003),
**New Directions in Instantiation-Based Theorem Proving**, Kolaitis P.,*Proceedings of the 18th IEEE Symposium on Logic in Computer Science*(Ottawa, Canada), pp.55-64. - GK04
- Ganzinger H., Korovin K. (2004),
**Integrating Equational Reasoning into Instantiation-Based Theorem Proving**, Marcinkowski J., Tarlecki A.,*Proceedings of the 18th International Workshop on Computer Science Logic, 13th Annual Conference of the EACSL*(Karpacz, Poland), pp.71-84, Lecture Notes in Computer Science 3210. - 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), pp.232-236, Lecture Notes in Artificial Intelligence 1632, Springer-Verlag. - Hil03
- Hillenbrand T. (2003),
**Citius altius fortius: Lessons Learned from the Theorem Prover Waldmeister**, Dahn I., Vigneron L.,*Proceedings of the 4th International Workshop on First-Order Theorem Proving*(Valencia, Spain), Electronic Notes in Theoretical Computer Science 86.1, Elsevier Science. - LS01
- Letz R., Stenz G. (2001),
**Model Elimination and Connection Tableau Procedures**, Robinson A., Voronkov A.,*Handbook of Automated Reasoning*, pp.2015-2114, Elsevier Science. - LS04
- Letz R., Stenz G. (2004),
**Generalised Handling of Variables in Disconnection Tableaux**, Rusinowitch M., Basin D.,*Proceedings of the 2nd International Joint Conference on Automated Reasoning*(Cork, Ireland), pp.289-306, Lecture Notes in Artificial Intelligence 3097. - Loe04a
- Löchner B. (2004),
**A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting**, Rusinowitch M., Basin D.,*Proceedings of the 2nd International Joint Conference on Automated Reasoning*(Cork, Ireland), pp.45-59, Lecture Notes in Artificial Intelligence 3097. - Loe04b
- Loechner B. (2004),
**What to Know When Implementing LPO**, Sutcliffe G., Schulz S., Tammet T.,*Proceedings of the Workshop on Empirically Successful First Order Reasoning, 2nd International Joint Conference on Automated Reasoning*(Cork, Ireland). - MarURL
- Martin D. et al. (URL),
**OWL-S 1.1 Release**, http://www.daml.org/services/owl-s/1.1/. - 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),
**A Davis-Putnam Program and its Application to Finite First-Order Model Search: Quasigroup Existence Problems**, ANL/MCS-TM-194, Argonne National Laboratory, Argonne, USA. - McC03a
- McCune W.W. (2003),
**Otter 3.3 Reference Manual**, ANL/MSC-TM-263, Argonne National Laboratory, Argonne, USA. - New01
- Newborn M. (2001),
**Automated Theorem Proving: Theory and Practice**, Springer. - NW04
- Newborn M., Wang Z. (2004),
**Octopus: Combining Learning and Parallel Search**,*Journal of Automated Reasoning*33(2), pp.171-218. - 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. - Pas01
- Pastre D. (2001),
**Muscadet2.3 : A Knowledge-based Theorem Prover based on Natural Deduction**, Gore R., Leitsch A., Nipkow T.,*Proceedings of the International Joint Conference on Automated Reasoning*(Siena, Italy), pp.685-689, Lecture Notes in Artificial Intelligence 2083, Springer-Verlag. - Pas02
- Pastre D. (2002),
**Strong and Weak Points of the Muscadet Theorem Prover**,*AI Communications*15(2-3), pp.147-160. - Pas06
- Pastre D. (2006),
**Complementarity of Natural Deduction and Resolution Principle in Empirically Automated Theorem Proving**, http://www.math-info.univ-paris5.fr/~pastre/compl-ND-RP.pdf. - RV02
- Riazanov A., Voronkov A. (2002),
**The Design and Implementation of Vampire**,*AI Communications*15(2-3), pp.91-110. - Sch02
- Schulz S. (2002),
**E: A Brainiac Theorem Prover**,*AI Communications*15(2-3), pp.111-126. - Sch04a
- Schulz S. (2004),
**System Abstract: E 0.81**, Rusinowitch M., Basin D.,*Proceedings of the 2nd International Joint Conference on Automated Reasoning*(Cork, Ireland), pp.223-228, Lecture Notes in Artificial Intelligence 3097. - Sch04b
- Schulz S. (2004),
**Simple and Efficient Clause Subsumption with Feature Vector Indexing**, Sutcliffe G., Schulz S., Tammet T.,*Proceedings of the Workshop on Empirically Successful First Order Reasoning, 2nd International Joint Conference on Automated Reasoning*(Cork, Ireland). - SW99
- Stenz G., Wolf A. (1999),
**E-SETHEO: Design, Configuration and Use of a Parallel Automated Theorem Prover**, Foo N.,*Proceedings of AI'99: The 12th Australian Joint Conference on Artificial Intelligence*(Sydney, Australia), pp.231-243, Lecture Notes in Artificial Intelligence 1747, Springer-Verlag. - Ste02a
- Stenz G. (2002),
**DCTP 1.2 - System Abstract**, Fermüller C., Egly U.,*Proceedings of TABLEAUX 2002: Automated Reasoning with Analytic Tableaux and Related Methods*(Copenhagen, Denmark), pp.335-340, Lecture Notes in Artificial Intelligence 2381, Springer-Verlag. - Ste02b
- Stenz G. (2002),
**The Disconnection Calculus**, PhD thesis, Institut für Informatik, Technische Universität München, Munich, Germany. - SS01
- Sutcliffe G., Suttner C.B. (2001),
**Evaluating General Purpose Automated Theorem Proving Systems**,*Artificial Intelligence*131(1-2), pp.39-54. - SZS04
- Sutcliffe G., Zimmer J., Schulz S. (2004),
**TSTP Data-Exchange Formats for Automated Theorem Proving Tools**, Zhang W., Sorge V.,*Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems*, pp.201-215, Frontiers in Artificial Intelligence and Applications 112, IOS Press. - Vor05
- Voronkov A. (2005),
**Vampire Reference Manual and User's Guide**, http://www.vampire.fm.