Two techniques are designed for eliminating quantifiers from an existentially quantified conjunction of dyadic literals, in terms of the operators o, boolean AND, and (-1) of the Tarski-Chin-Givant formalism of relations. The use of such techniques is illustrated through increasingly challenging examples, and their algorithmic complexity is assessed. (C) 2002 Elsevier Science B.V. All rights reserved.
Compiling dyadic first-order specifications into map algebra
CANTONE, Domenico;
2003-01-01
Abstract
Two techniques are designed for eliminating quantifiers from an existentially quantified conjunction of dyadic literals, in terms of the operators o, boolean AND, and (-1) of the Tarski-Chin-Givant formalism of relations. The use of such techniques is illustrated through increasingly challenging examples, and their algorithmic complexity is assessed. (C) 2002 Elsevier Science B.V. All rights reserved.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.
