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

return to the contents page