Dumatel, a Prover based on Equational Reasoning

This is a study in combining Computer algebra, Term rewriting and Automatic proofs. The current system of Dumatel-1.02 is presented as a library of Haskell functions. It contains 1) TRW interpreter subdued to an explicitly given partial term ordering parameter, 2) `unfailing' Knuth-Bendix completion methods ukb, ukbb, whith a certain specialized completion for Boolean connectives, 3) the inductive prover, including also the refutation procedure for predicate calculus, using ukbb.