OVERVIEW
========

Version 1.4.5

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.