[Haskell] `Dumatel' software announcement

[Serge D. Mechveliani]

                  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.

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