Istituto di Scienza e Tecnologie dell'Informazione     
Martelli A., Montanari U. Theorem proving with structure sharing and efficient unification. (apparso in Note Scientifiche Universita degli Studi di Pisa, Istituto di Scienze della Informazione, settembre). Internal note IEI-B77-07, 1977.
The standard unification algorithm may be extremely inefficient in the context of proof checkers using the Boyer and Moore's technique for structure sharing. An efficient unification algorithm developed by the authors can be used to modify Boyer and Moore's storing mechanism in order to make explicit further factorizations and to eliminate non accessible variables.

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional