OVERVIEW ======== Darwin is a first-order logic prover, an implementation of the Model Evolution Calculus. Darwin is available from http://www.mpi-sb.mpg.de/~baumgart/DARWIN/. CONTENT ======= AUTHORS responsible for the design and implementation INSTALL installation instructions CHANGES changes between versions LICENSE license and copyright README this file DESIGN sketch of Darwin's architecture Makefile Makefiles to build darwin OCamlMakefile interactive.py starts darwin in an interactive OCaml top level src/ the source code doc/ documentation doc/darwin_handbook.pdf manual, description of calculus, proof procedure, architecture, algorithms, data structures, ... doc/darwin/ contains the interface documentation if built during the installation (see INSTALL) test/ unit tests for darwin's source eval/ scripts and problem set definitions for evaluating and testing darwin on the TPTP DOCUMENTATION ============= The calculus is presented in Baumgartner, Tinelli. The Model Evolution Calculus. http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-1-2003.pdf http://citeseer.ist.psu.edu/566633.html Darwin's implementation is shortly described in Baumgartner, Fuchs, Tinelli. Darwin: A Theorem Prover for the Model Evolution Calculus. http://www.mpi-sb.mpg.de/~baumgart/publications/darwin.pdf Darwin's implementation and usage is extensively explained in Fuchs. Darwin: A Theorem Prover for the Model Evolution Calculus. doc/darwin_handbook.pdf TPTP (/eval) ==== The directory eval contains several scripts useful 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. Note: Darwin uses tme as its input format, so any tested TPTP problems have to be converted to tme. 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 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 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.