PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Aiello L., Aiello M., Prini G. Un sistema interattivo per la dimostrazione di proprieta' di programmi e schemi. Internal note IEI-B74-43, 1974.
 
 
Abstract
(English)
This paper describes an interactive proof checker under development at Pisa. It is based on the LCF implemented by Robin Milner at Stanford and is primarily intended for proving properties of programs and program schemata. We outline the structure of the checker and its most relevant features: goal structure simplification mechanism, flexible interaction and proof construction.
Subject


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