Informal proofs formally checked by machine
Aiello, Luigia ; Aiello, Mario ; Attardi, Giuseppe ; Prini, Gianfranco
Annales scientifiques de l'Université de Clermont. Mathématiques, Tome 58 (1976), p. 31-53 / Harvested from Numdam
Access to full text
Full (PDF)
Full (DJVU)
Publié le : 1976-01-01
@article{ASCFM_1976__60_13_31_0,
     author = {Aiello, Luigia and Aiello, Mario and Attardi, Giuseppe and Prini, Gianfranco},
     title = {Informal proofs formally checked by machine},
     journal = {Annales scientifiques de l'Universit\'e de Clermont. Math\'ematiques},
     volume = {58},
     year = {1976},
     pages = {31-53},
     mrnumber = {468369},
     zbl = {0352.68110},
     language = {en},
     url = {http://dml.mathdoc.fr/item/ASCFM_1976__60_13_31_0}
}

Aiello, Luigia; Aiello, Mario; Attardi, Giuseppe; Prini, Gianfranco. Informal proofs formally checked by machine. Annales scientifiques de l'Université de Clermont. Mathématiques, Tome 58 (1976) pp. 31-53. http://gdmltest.u-ga.fr/item/ASCFM_1976__60_13_31_0/

1 - J.A. Robinson - A machine oriented logic based on the resolution principle- Journal of the ACM - Vol.12 - 1965. | MR 170494 | Zbl 0139.12303

2 - R. Ehrenfeucht, M. Rabin - There is no perfect proof procedure- Unpublished paper - Underground Jerusalem 1972.

3 - R. Milner - Logic for computable functions: description of a machine implementation- Artificial Intelligence Memo No 169 - Stanford University - 1972.

4 - R. Weyhrauch, A. Thomas - FOL: a proof checker for first order logic- Artificial Intelligence Memo No 235 - Stanford University - 1974.

5 - L. Aiello, M. Aiello, R. Weyhrauch - The semantics of PASCAL in LCF- Artificial Intelligence Memo No 221 - Stanford University - 1974.

6 - M. Aiello, R. Weyhrauch - Checking proofs in the metamathematics of first order logic- Artificial Intelligence Memo No 222 - Stanford University 1974 - Also in Proc. of the Fourth International Joint Conference on Artificial Intelligence - Tbilisi - 1975.

7 - C. Montangero, G. Pacini, F. Turini - MAGMA-LISP: a «machine language» for artificial intelligence - Proceedings of the Fourth International Joint Conference on Artificial Intelligence - Tbilisi - 1975.

8 - D. Scott - An alternative approach to CUCH, IS WIM, OWHY- Unpublished paper- Underground Princeton - 1969.

9 - R. Milner- Models of LCF - Artificial Intelligence Memo No 186 - Stanford University 1973.

10 - A. Church - The calculi of λ-conversion - Annals of Mathematical Studies No 6- Princeton- 1941. | JFM 67.0041.01 | Zbl 0026.24205

11 - D. Scott - Continuous lattices - Technical Monograph PRG-7 - Oxford University - 1971. | MR 404073

12 - R. Milner, L. Morris, M. Newey - A logic for computable functions with reflexive and polymorphic types - Proceedings of the International Symposium of Proving and Improving Programs - Arc et Senans - 1975.

13 - M. Newey- Formal semantics of LISP with applications to program correctness - Thesis- Artificial Intelligence Memo No 257 - Stanford University - 1975.