E-Darwin -
A Theorem Prover for the Model Evolution Calculus with Equality
Page still under construction!
E-Darwin is an automated theorem prover for first-order clausal logic with equality.
It accepts problems in tptp
or tme syntax.
Non-clausal input is clausified using the eprover (or soon
a built-in clausifier).
E-Darwin implements the Model Evolution calculus and several variants thereof which include equality reasoning,
see the papers.
The system is a based on the Darwin prover.
As Darwin is no longer actively maintained, E-Darwin will eventually subsume all of its functions.
The development of E-Darwin forked off from Darwin 1.3, so at the moment E-Darwin still needs to catch up
on the changes made between Darwin 1.3 and its last version, Darwin 1.4.5.
You can download the current (26-09-2011) version of E-Darwin
here.
Some software requirements:
- E-Darwin requires a version of OCaml (3.09.3 or higher).
- The installer configuration script of E-Darwin requires Python,
though you may get away with using the default configuration.
- If you want to use formula input (TPTP "fof"), then you should have the eprover
for clausification.
So far the majority of the relevant papers are for Darwin and the Model Evolution calculus.
The following list is therefore mostly identical to the
Darwin publications.
-
Peter Baumgartner, Björn Pelzer, Cesare Tinelli.
Model Evolution with Equality - Revised and Implemented
Submitted for journal publication, June 2010.
[ Abstract
| BibTeX
| PDF
]
-
Peter Baumgartner, Alexander Fuchs, Hans de Nivelle, Cesare Tinelli.
Computing Finite Models by Reduction to Function-Free Clause Logic
Journal of Applied Logic (JAL), 2007.
[ Abstract
| BibTeX
| Preprint (PDF)
]
-
Peter Baumgartner, Alexander Fuchs, Hans de Nivelle, Cesare Tinelli.
Computing Finite Models by Reduction to Function-Free Clause Logic
Disproving'06, Workshop at IJCAR'06, 2006.
[ Abstract
| BibTeX
| PDF
| Slides (PDF)
]
-
Peter Baumgartner, Alexander Fuchs, Cesare Tinelli.
Lemma Learning in the Model Evolution Calculus
(Preliminary) long version of a conference submission, May 2006, accepted.
[ Abstract
| BibTeX
| PDF
]
-
Peter Baumgartner, Alexander Fuchs, Cesare Tinelli.
Implementing the Model Evolution Calculus
System description (version 1.1).
Special Issue of the International Journal of Artificial Intelligence Tools (IJAIT), 2005.
[ Abstract
| BibTeX
| Preprint (PDF)
]
-
Alexander Fuchs.
Darwin - A Theorem Prover for the Model Evolution Calculus
Master's thesis.
Extended system description and handbook (version 1.0), 2004.
[ Abstract
| BibTeX
| PDF
]
-
Peter Baumgartner, Alexander Fuchs, Cesare Tinelli.
Darwin - A Theorem Prover for the Model Evolution Calculus
System description (version ESFOR) at IJCAR 2004 workshop
ESFOR (aka S4).
[ Abstract
| BibTeX
| PDF
| Slides (PDF)
]
-
Peter Baumgartner, Cesare Tinelli.
The Model Evolution Calculus with Equality
CADE-20 conference paper, 2005.
[ Abstract
| BibTeX
| PDF
]
-
Peter Baumgartner, Cesare Tinelli.
The Model Evolution Calculus
(The Model Evolution calculus is the successor of
FDPLL, a
First-Order Davis-Putnam-Logeman-Loveland Procedure.)
E-Darwin is maintained by Björn Pelzer.
Home