OVERVIEW ======== Version 1.3.1 Darwin is a first-order logic prover, an implementation of the Model Evolution Calculus. Darwin is available from http://combination.cs.uiowa.edu/Darwin/ 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.