Dumatel. A prover based on equational reasoning.

Dumatel-1.02 is a prover based on many-sorted term rewriting (TRW) and equational reasoning.
It is a program package written in a purely functional, `lazy' language Haskell. It is presented as a library of functions and data structures.
Its design keys are:
unfailing Knuth-Bendix completion, and its specialization for Boolean terms, skolemization for predicate calculus formulae, inductive proof, resource distribution.

Developer
Serge Mechveliani , Program Systems Institute , Pereslavl-Zalessky , Russia.
e-mail: mechvel@botik.ru

Language extension
Dumatel is written in what we call Haskell-2-pre - certain functional extension of Haskell-98 .
This extension includes the multiparametric classes, overlapping instances, other minor features.

Ports
Dumatel-1.02 of May 2005 was tested under the Glasgow Haskell tool of ghc-6.2.2, Linux
(see http://haskell.org for information on the Haskell implementations).
We hope, it can be ported to other systems. It works everywhere where the GHC tool works - many machines and operation systems.

Downloading: Dumatel is available from

See the sub-directories in ./dumatel/ for the information on each actual version.
The sub-directory ./notes/ contains the files with the accumulated notes on each version - bugs discovered, recommendations and others - the contents of these files update now and then.

Send remarks to Serge Mechveliani mechvel@botik.ru