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@botik.ru -------------------- Serge Mechveliani, Program Systems Institute, 152020, Pereslavl-Zalessky, Russia. e-mail mechvel@botik.ru http://www.botik.ru/~mechvel