In spite of the remarkable achievements recently obtained in the field of mechanization of formal reasoning, the overall usability of interactive provers does not seem to be sensibly improved since the advent of the ``second generation'' of systems, in the mid of the eighties. We try to analyze the reasons of such a slow progress, pointing out the main problems and suggesting some possible research directions.

A., A., C., S.C. (2010). Some Considerations on the Usability of Interactive Provers. [10.1007/978-3-642-14128-7_13].

Some Considerations on the Usability of Interactive Provers.

ASPERTI, ANDREA;SACERDOTI COEN, CLAUDIO
2010

Abstract

In spite of the remarkable achievements recently obtained in the field of mechanization of formal reasoning, the overall usability of interactive provers does not seem to be sensibly improved since the advent of the ``second generation'' of systems, in the mid of the eighties. We try to analyze the reasons of such a slow progress, pointing out the main problems and suggesting some possible research directions.
2010
Intelligent Computer Mathematics
147
156
A., A., C., S.C. (2010). Some Considerations on the Usability of Interactive Provers. [10.1007/978-3-642-14128-7_13].
A., Asperti; C., Sacerdoti Coen
File in questo prodotto:
Eventuali allegati, non sono esposti

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: https://hdl.handle.net/11585/93290
 Attenzione

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

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 3
social impact