ERCIM News No.26 - July 1996 - CNR
Reasoning in Symbolic Computation Systems
by Gianna Cioni and Attilio Colagrossi
Symbolic and algebraic computation systems have been used as
tools for solving mathematical problems in many different application fields.
In the last years, the aim of developers in the design of new systems has
been to overcome the gap between the user's wishes and the effective features
of these systems, especially with respect to the semantic correctness of
computations. Nowadays, such systems generally offer a good degree of performance,
flexibility and friendliness, but they are still far from reflecting the
typical way in which researchers operate. A careful consideration of reasoning
aspects and the integration into both the languages and the environments
of automated deduction capabilities is currently being considered as a way
to bridge the gap between systems and users.
Over the last five years, a collaboration between the 'Istituto di Analisi
dei Sistemi ed Informatica' (IASI-CNR) and two Rome universities ('La Sapienza'
and the 'Third University') has focused on the definition of methodologies,
languages and tools for an advanced algebraic computation system.
The common approach followed to define the mathematical structures manipulated
by symbolic computation systems is axiomatization. This requires the specification
of the underlying sets, of the operations and of the axioms. These mathematical
structures can be represented by object-oriented language constructs, such
as classes. All the elements of interest can be viewed, during the run-time,
as instances of classes or objects. The hierarchical structuring of a collection
of classes representing mathematical structures is particularly useful as
it provides a suitable notion of inheritance. In this way, when specifying
a derived structure, only the new features have to be defined. The inheritance
mechanism defined for mathematical objects is specialisation, ie subclassing
is allowed only in those cases where the subclass is a specialisation of
the superclass. This kind of inheritance also holds for the attribute property
of class structure, representing the axioms of the mathematical structures
to be modelled. In fact, the properties of a superclass are inherited by
its subclasses.
After having developed some automatic deduction tools capable of manipulating
logic properties (mainly in first order logic) with a good degree of naturalness
and friendliness (for instance a sequential calculus to be used either as
an automatic or interactive tool), we started to integrate them into the
object-oriented environment mentioned above for treating mathematical objects.
The reasoning apparatus is used at compilation time, ie at a static level,
for evaluating logical relations among different classes, in order to rearrange
the given hierarchy in a better way with respect to particular parameters,
depending on the specific application. For instance, the implication relation
between two classes allows a structure to be linearized, eliminating multiple
inheritances and ambiguity elements. Again, the detection of new relations
from old ones, allows a user to build a structure with all possible connections
among different classes given explicitly so that all possible dependencies
are clear. These applications examine one of the principal topics of software
engineering: how to increase the expressiveness and/or the efficiency of
a specification.
The reasoning apparatus is also used at run-time, ie at instance level,
thus offering the users the chance to work with an algebraic computation
system integrated with automated deduction in the same way as they work
by pencil or using more traditional systems. This approach also responds
to the need for semantic correctness, allowing the required computations
to be performed in a totally axiomatized environment.
Please contact:
Gianna Cioni - IASI-CNR
Tel: +39 6 7716436
E-mail: cioni@iasi.rm.cnr.it
return to the contents page