(06.10.2010):
Darwin is no longer actively maintained.
All development has moved to its successor, E-Darwin.
(06.10.2009):
Darwin 1.4.5
released, minor fixes.
(15.09.2008):
Darwin 1.4.4
released, a TME fix.
(08.05.2008):
Darwin 1.4.3
released, some TPTP related fixes.
(11.01.2008):
Darwin 1.4.2
(minor changes and fixes) released,
applications section updated.
(20.07.2007):
Darwin won the EPR divison of the CASC competition 2007.
(01.07.2007):
Darwin 1.4.1
(SZS ontology compliant)
and
Darwin 1.3.1
(bugfix)
released.
(28.05.2007):
Darwin 1.4
released.
(24.08.2006):
Darwin won the EPR divison of the CASC competition 2006.
(20.07.2006):
Darwin 1.3
released, papers about
Lemma Learning
and
Finite Model Finding.
(20.03.2005):
IJAIT paper
describing Darwin 1.1 available.
(03.01.2005):
Darwin 1.1 available.
(10.10.2004):
section on Applications.
Darwin is an automated theorem prover for first order clausal logic. It accepts problems formulated in tptp or tme format, non-clausal tptp problems are clausified using the eprover. Equality is not built into the currently implemented version of the calculus, it is instead automatically axiomatized for a given problem. Darwin is a decision procedure for function-free clause sets, and is in general faster and scales better on such problems than propositional approaches.
Darwin is the first implementation of the Model Evolution Calculus (see papers below). The Model Evolution Calculus lifts the propositional DPLL procedure to first-order logic. One of the main motivations for this approach was the possibility of migrating to the first-order level some of those very effective search techniques developed by the SAT community for the DPLL procedure.
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. The search space is explored by iterative deepening over the term depth of candidate literals. Darwin employs a uniform search strategy for all problem classes.
The central data structure is the context. A context represents an interpretation as a set of first-order literals. The context is grown by using instances of literals from the input clauses. The implementation of Darwin is intended to support basic operations on contexts in an efficient way. This involves the handling of large sets of candidate literals for modifying the current context. The candidate literals are computed via simultaneous unification between given clauses and context literals. This process is sped up by storing partial unifiers for each given clause and merging them for different combinations of context literals, instead of redoing the computations of the partial unifiers.
For efficient filtering of unneeded candidates against context literals, discrimination tree or substitution tree indexing is employed. The splitting rule generates choice points in the derivation which are backtracked using a form of backjumping similar to the one used in DPLL-based SAT solvers. Also similiar to SAT solvers, lemmas can be learned from closed branches and used to prune the remaining search space.
With Version 1.3 Darwin can be used as a finite model finding for first-order logic with equality. The approach is similar to other finite model finders like paradox, but instead of transforming a problem to propositional logic, it is converted to function-free first-order logic. Thus, Darwin scales significantly better for higher symbol arities and domain sizes wrt. to memory consumption.
Darwin runs on Unix systems (various versions tested with FreeBSD, Debian, Gentoo, SUSe, Red Hat, Ubuntu, MaxOS X), and Windows. Darwin is distributed in source format under the GNU General Public License (GPL). In order to compile the source, the OCaml compiler in version 3.08 or newer has to be installed. The installation process is described in the INSTALL file (in brief, install OCaml and run gnu make).
Currently available versions:
The automated theorem proving systems competition
CASC
is held each year at the major conference CADE/IJCAR (International Conference on Automated Reasoning).
Darwin 1.3 won the
EPR division
(function-free clause logic, for which Darwin is a decision procedure)
in the
CASC-J3
competitions held in 2006 and 2007,
and the finite model finding variant of Darwin scored third in the SAT category (satisfiable first-order logic formulas) both times.
Darwin up to 1.1 was evaluated on the clausal problems without equality of the TPTP problem library (version 2.6 or newer). Darwin performs well on problems from the Bernays-Schoenfinkel-Class, average for Horn problems, weak for non-Horn problems. As neither the Model Evolution Calculus nor Darwin handles equality yet (this is ongoing research), Darwin is not suited for problems with equality. In conclusion, Darwin performs quite well on clause sets without function symbols (except constants), the EPR division. It is very weak on Horn problems with equality (HEQ) and better on non-Horn problems without equality (NNE).
Benchmarked versions:
Darwin has been used in the following projects:
We would be delighted to learn about more applications of Darwin and include references here!
Darwin is developed by Peter Baumgartner, Alexander Fuchs (main developer) and Cesare Tinelli.
The material on this site is based upon work partially supported by the National Science Foundation under Grant No. 237422.
Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation.