Maple’s symbolic evaluator, together with a feature that is usually known as the assume facility, implements a powerful form of conditional rewriting. In a previous paper the authors showed that Maple’s evaluation process can be recast as constraint contextual rewriting (CCR), a form of conditional rewriting that incorporates the services provided by a decision procedure through a well- specified interface. In the present paper, this analysis is extended to a component of the assume facility that deals with problems beyond linear arithmetic and that we call the general solver. This led to the discovery of a fault that causes Maple to return wrong results with some contexts. The reason for this is that the facility wrongly assumes that the general solver is complete in the sense that it uses all the available assumptions in the context. While a simple fix to this problem would reduce the logical strength of the assume facility, we show that a more general approach inspired by techniques available in CCR does not suffer from the problem and naturally leads to stronger forms of simplification.

A Reconstruction and Extension of Maple's Assume Facility via Constraint Contextual Rewriting.

Armando, Alessandro;
2005

Abstract

Maple’s symbolic evaluator, together with a feature that is usually known as the assume facility, implements a powerful form of conditional rewriting. In a previous paper the authors showed that Maple’s evaluation process can be recast as constraint contextual rewriting (CCR), a form of conditional rewriting that incorporates the services provided by a decision procedure through a well- specified interface. In the present paper, this analysis is extended to a component of the assume facility that deals with problems beyond linear arithmetic and that we call the general solver. This led to the discovery of a fault that causes Maple to return wrong results with some contexts. The reason for this is that the facility wrongly assumes that the general solver is complete in the sense that it uses all the available assumptions in the context. While a simple fix to this problem would reduce the logical strength of the assume facility, we show that a more general approach inspired by techniques available in CCR does not suffer from the problem and naturally leads to stronger forms of simplification.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11582/21497
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact