Information Technology Reference
In-Depth Information
From a Computer Algebra Library to a System
with an Equational Prover
Serge Mechveliani
152020, Program Systems Institute, Pereslavl-Zalessky, Russia
mechvel@botik.ru
Abstract. We consider joining to our computer algebra library a cer-
tain prover based on the TRW machine with an order-sorted algebraic
specification language for input. A resource distribution approach helps
to automate the proof tactics. Inductive reasoning is organized through
adding of equalities. The unfailing Knuth-Bendix completion combined
with special completion for the Boolean terms enables proofs in predicate
logic. The question is how to develop further a language for equational
reasoning/computing, the prover library and special provers to make pos-
sible the solution of more substantial problems than the ones mentioned
in the examples.
Keywords: computer algebra, equational prover, term rewriting.
For several years we have been developing a computer algebra (CA) library called
DoCon ( www.botik.ru/~mechvel/papers.html ). It is written in the Haskell
language and implements a good-sized piece of commutative algebra. Now, in
order to extend the ability to operate with explicit knowledge about domains, we
aim at the following two goals. (1) To develop and implement an adequate “ob-
ject” language ( OL ) based on order-sorted equational specifications (OSTRW),
a prover related to OL, and to incorporate the existing CA library and prover
into one system. (2) To enrich the existing tactics, the prover library, etc., in
order to make the system more effective in solving problems.
The project also has relevance to the area of partial evaluation, since such a
prover also allows automated reasoning about functional programs.
Our program is called Dumatel (a joke Russian word from the novel “Skazka
o troike” by brothers Strugatsky, it stands for “thinker”).
As an introduction, some ideas related to the project can be found in [5], [3],
[4], [6], [1], and the manual for the Maude system. Among the projects with a
similar direction, we can mention Theorema ( www.theorema.org ). There is also
the Maude system ( maude.cs.uiuc.edu ) remarkable for its treating of OSTRW,
reflexion , AC (associative and commutative) operators. In this four-page paper
we cannot describe the design principles in much detail. More information will
be available in
Reference: the initial open source Dumatel system version, together with some
expanded documentation, is expected to appear during 2004. The relevant URL
is www.botik.ru/~mechvel (/papers.html) .
Search WWH ::




Custom Search