                  A N N O U N C E M E N T


                       D u m a t e l

    a prover program based on equational reasoning,  Version 1.02


is available, together with its source program and manual book,
at the following addresses:

  http://www.botik.ru/~mechvel/papers.html  click at `dumatel'
                                                     (Russian site),
  ftp.botik.ru/pub/local/Mechveliani/dumatel/        (same site),

  http://www.haskell.org/dumatel/distrib/            (USA site)


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. 
To use Dumatel-1.02, user needs to be familiar with Haskell
programming.

`Dumatel' is a joke Russian word, it stands for `thinker'.

What it has. Abilities 
----------------------
* TRW interpreter `reduce', subdued to an explicitly given partial 
  term ordering parameter.
* `Unfailing' Knuth-Bendix completion methods  ukb, ukbb,
  where the latter method extends the former with a certain 
  specialized completion for the Boolean connectives.
* The inductive prover `prove', including also the refutation
  procedure for the predicate calculus, using  ukbb. 
  The prover reasons about equational specifications, transforming 
  them dynamically.
* So far, it is able to solve in a real time only simple problems, 
  and not all of them. Examples of successful proof:
  (1) Prove  
      list |-inductive-  forall Xs ((reverse reverse Xs) = Xs),
      where "reverse" is defined recursively via the list 
      concatenation "+", and "+" defined recursively via ":"
      (`cons').
  (2) naturalNumbers |-inductive-  forall [n, m] (n+m = m+n),
      where "+" is defined via the "successor" operator by the 
      equations  [n+0 = 0,  n+(s m) = s (n+m)].
  Example of failure:
  (3) naturalNumbers |-inductive-  forall [n, m] (n*m = m*n),
      where the multiplication "*" is defined in (2) via "+":
      [n*0 = 0,  n*(s m) = n + n*m].
  We can fix this example, with its neighbours, but then we shall 
  discover the next simple fail example ... 

So far, everything is programmed in Haskell, even pattern matching 
and term unification.

See the  Manual  for further information.

Particular features
-------------------
* United completion method for unfailing completion and refutation 
  procedure with Boolean terms.
* Heuristics for certain equational lemma search method.
* The resource distribution approach in the prover strategy is 
  applied in order to avoid too deep proof branches.

Possible application area
-------------------------
* Automatic reasoning in mathematics and in functional programming.
* Extension of computer algebra systems with proof facilities.
* Symbolic optimization of functional programs, support for the 
  approach with the `algebra' of functional programs.

Other prover systems
--------------------
See  http://www.rewriting.org
Dumatel-1.02 is a newcomer. We looked into the papers and manuals on
some other provers, but so far, never compared Dumatel to them, and
never benchmarked it.

On Haskell language
-------------------
For the  Haskell language  materials, and its implementation systems 
see the site
                           http://www.haskell.org

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

Ports:    Dumatel-1.02 was tested under  ghc-6.2.2, Linux.
------
WARNING:  we expect that each Dumatel version will work 
          (literally as it is) only under some single GHC version.

On the other hand, it should be easy to port to higher GHC versions.
We believe, it can be ported (with some effort) to other Haskell 
implementations. 

Machines, environment
---------------------
Dumatel has to work everywhere where the aforementioned Haskell 
language implementations work -- many machines and systems. 
To install Dumatel on your particular machine, find the GHC 
system at  http://haskell.org/ghc  and install it as it is explained 
there. Then, follow the document  install.txt  of the Dumatel 
distribution.

Manual (`book'):  see  dm/book.ps  contained in the distribution.
---------------

Current notes
-------------
such as known bugs and their work-arounds, are contained in the file
                       .../dumatel/notes/1.02.txt

in the distribution directory; the contents of this file is supposed 
to update with currently appearing notices.


Remarks are welcome:   mechvel@botik.ru
--------------------

Serge Mechveliani,
Program Systems Institute, 152020, Pereslavl-Zalessky, Russia.
e-mail  mechvel@botik.ru
http://www.botik.ru/~mechvel






