JAR
2007
13 years 11 months ago
2007
The vision of a computerised assistant to mathematicians has existed since the inception of theorem proving systems. The Alcor system has been designed to investigate and explore h...
TPHOL
1999
IEEE
14 years 3 months ago
1999
IEEE
Abstract. We present a generic approach to readable formal proof documents, called Intelligible semi-automated reasoning (Isar). It addresses the major problem of existing interact...
TACAS
2009
Springer
14 years 6 months ago
2009
Springer
We introduce the All-Termination(T) problem: given a termination solver, T, and a program (a set of functions), find every set of formal arguments whose consideration is sufficie...