Q: Systems for Algebraic/ Structural Reasoning

Florian Kammueller (Florian.Kammueller@cl.cam.ac.uk)
Thu, 07 Mar 1996 19:30:32 +0000

I am currently comparing the systems IMPS, PVS and Larch with respect to
their facilities to perform proofs in abstract algebra. The major concern of
this is to find out if the objects of concern, e.g. groups, rings, etc.,
may be expressed as single theories or modules, respectively. That is, the carrier
of a group is expressed as a type, the operations as functions over that
type. This representation is suggested by the systems descriptions.
It allows to instantiate the theory of e.g. groups to, say, a type of
integers together with its functions 0, +, and - . An instantiation like
that would then produce the results showed on an abstract level about groups
automatically for the type of integers after we show that the type integer
meets the group axioms.

But, it is not directly possible to talk _about_ groups in formulas though
this is absolutly common in mathematics. It is not possible in this "theory"
representation unless we redefine the whole theory again as a predicate.

My question is now: Are there any other theorem proving systems which offer
an explicit theory notion and allow to do the described change of viewpoint
in a more elegant way?

Florian