OVERVIEW ======== E-Darwin 1.4 based on Darwin 1.3 E-Darwin is a first-order logic prover with equality, an implementation of the Model Evolution Calculus with Equality. The original Darwin is a first-order logic prover, an implementation of the Model Evolution Calculus. Darwin is available at http://combination.cs.uiowa.edu/Darwin/ E-Darwin is available at http://www.uni-koblenz.de/~bpelzer/edarwin CASC ==== E-Darwin requires OCaml 3.09.3 or newer for compiling. The configuration script 'configure.py' requires an installation of Python, but the default configuration/Makefile should be sufficient in most cases. To compile, change into the E-Darwin directory ('e-darwin', the one where this README is located in). If you wish/need to configure, type python ./configure.py This creates a properly configured Makefile. After that, type make to compile E-Darwin. The E-Darwin directory will then contain the executable 'e-darwin'. This is the E-Darwin prover, it requires no further files for operation and be copied into any directory. In the following we assume the executable to remain in the original directory, though. To execute E-Darwin for CASC, type ./e-darwin -if tptp -pl 0 -pev TPTP where is the full name (with path) of a tptp problem file. The flag '-if tptp' forces the prover to read all input as tptp syntax. The flag '-pl 0' turns down the output verbosity to the minimum where only the SZS result is printed. The flag '-pev TPTP' tells E-Darwin to look for files specified by 'include'-directives in locations relative to the path specified by the environmental variable $TPTP. FOF problems must be clausified. E-Darwin attempts to do this using the eprover. E-Darwin looks for the eprover first in the directory containing the E-Darwin executable, then in the enviroment program path. If an eprover executable is stored elsewhere, its path can be specified for E-Darwin using the flag -eprover , for example ./e-darwin -eprover /bin/provers/eprover -if tptp -pl 0 -pev TPTP If using eprover is not an option, E-Darwin can use its builtin clausifier, which is a bit experimental at this point. To do this, use the flag -cl Builtin, for example ./e-darwin -cl Builtin -if tptp -pl 0 -pev TPTP Result output: If E-Darwin terminates on its own, then it prints one of the following results to stdout: % SZS status Unsatisfiable when E-Darwin has determined the input to be an unsatisfiable problem (CNF or FOF without conjecture); % SZS status Satisfiable indicates a satisfiable input problem (CNF or FOF without conjecture); % SZS status Theorem indicates a conjectural FOF problem determined to be a theorem; % SZS status CounterSatisfiable indicates a conjectural FOF problem determined to be a non-theorem. ========================================================================================== The remainder of this document consists of the content of the original (non-CASC-oriented) README-file. CONTENT ======= AUTHORS responsible for the design and implementation INSTALL installation instructions CHANGES changes between versions LICENSE license and copyright README this file configure.py configuration script to create a Makefile Makefile.in template Makefile used by configure.py Makefile.default default Makefile to build darwin OCamlMakefile core Makefile included by other Makefiles interactive.py starts darwin in an interactive OCaml top level (currently not working) src/ the source code doc/ documentation doc/darwin/ contains the interface documentation if built during the installation (see INSTALL) test/ unit tests for darwin's source (mostly outdated and not working) eval/ scripts and problem set definitions for evaluating and testing darwin on the TPTP DOCUMENTATION ============= These references are all available on the official web page. The calculus is presented in Baumgartner, Tinelli. The Model Evolution Calculus. The implementation of Darwin 1.0 is shortly described in: Baumgartner, Fuchs, Tinelli. Darwin: A Theorem Prover for the Model Evolution Calculus. The implementation and usage of Darwin 1.0 is explained in: Fuchs. Darwin: A Theorem Prover for the Model Evolution Calculus. The implementation of Darwin 1.1 is shortly described in: Baumgartner, Fuchs, Tinelli. Darwin: Implementing the Model Evolution Calculus. The Lemma Learning option of version 1.3 is described in: Baumgartner, Fuchs, Tinelli. Lemma Learning in the Model Evolution Calculus The Finite Model Finding mode of version 1.3 is described in: Baumgartner, Fuchs, de Nivelle, Tinelli. Computing Finite Models by Reduction to Function-Free Clause Logic TPTP (/eval) ==== The directory eval contains several scripts used to evaluate and compare darwin and (potentially) other provers over TPTP problems restricted by time and memory limits. Although these scripts are written in python they only work with Linux. They have to be adapted to work with other Unixes or Windows. RunProblems.py Runs a prover over files containing TPTP problem lists. The output of the prover is scanned for statistical information and a found proof, a summary for each problem is printed to a file. The prover, the TPTP directory, file extensions, statistic key words, the memory and the CPU limit must be specified by editing constants in the script. StatsProblems.py Creates a summary (solved, timeout, out of memory, ...) for a list of summary created by RunProblems.py StatsExtended.py Creates more detailed summaries than StatsProblems.py RunCasc.py Wrapper for RunProblems to simplify runs over the problem sets used in the CASC19, CASC19 competitions StatsCasc.py Wrapper for StatsProblems to simplify runs over the problem sets used in the CASC19, CASC19 competitions FindProblems.py Finds subsets of the tptp corresponding to various criteria, like cnf, equality, Horn, BS, ... UNIT TESTS (/test) ========== These tests are ugly and cover only a part of the source. Nevertheless, they proved quite helpful during development. They are (all or some) run with the script test/make_test.py.