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
CHANGES			changes between versions
README			this file


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, ...