[Haskell] `Dumatel' software announcement
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,
at the following addresses:
http://www.botik.ru/~mechvel/papers.html click at `dumatel'
ftp.botik.ru/pub/local/Mechveliani/dumatel/ (same site),
http://www.haskell.org/dumatel/distrib/ (USA site)
a prover based on many-sorted term rewriting (TRW) and equational
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
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
* So far, it is able to solve in a real time only simple problems,
and not all of them. Examples of successful proof:
list |-inductive- forall Xs ((reverse reverse Xs) = Xs),
where "reverse" is defined recursively via the list
concatenation "+", and "+" defined recursively via ":"
(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
Program Systems Institute, 152020, Pereslavl-Zalessky, Russia.
e-mail mechvel at botik.ru
More information about the Haskell