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
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.
- Developer:Sergey D. Mechveliani
152020, Program Systems Institute,
- Number of sites: 1
- In use: since May 2005
- Language: Haskell
(Haskell-2-pre functional extension of Haskell-98
the last system version was tested under ghc-6.2.2, Linux).
Glasgow Haskell ghc-6.2.2
the source program of the last version Dumatel-1.02, and the manual book,
can be copied from
- Related publications:
- "Term rewriting, Equational Reasoning, Automatic proofs".
The book in the archive of Dumatel-1.02 distribution.