Serge D. Mechveliani mechvel at botik.ru
Mon May 16 08:20:19 EDT 2005

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

http://www.botik.ru/~mechvel/papers.html  click at `dumatel'
(Russian site),
ftp.botik.ru/pub/local/Mechveliani/dumatel/        (same 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'
It is presented as a library of functions and data structures.
To use Dumatel-1.02, user needs to be familiar with Haskell
programming.

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

See the  book.ps  for further information.

Ports:    Dumatel-1.02 was tested under  ghc-6.2.2, Linux.
------

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

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

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

```