Informal proofs formally checked by machine

Luigia Aiello; Mario Aiello; Giuseppe Attardi; Gianfranco Prini

Annales scientifiques de l'Université de Clermont. Mathématiques (1976)

  • Volume: 60, Issue: 13, page 31-53
  • ISSN: 0249-7042

How to cite

top

Aiello, Luigia, et al. "Informal proofs formally checked by machine." Annales scientifiques de l'Université de Clermont. Mathématiques 60.13 (1976): 31-53. <http://eudml.org/doc/80436>.

@article{Aiello1976,
author = {Aiello, Luigia, Aiello, Mario, Attardi, Giuseppe, Prini, Gianfranco},
journal = {Annales scientifiques de l'Université de Clermont. Mathématiques},
language = {eng},
number = {13},
pages = {31-53},
publisher = {UER de Sciences exactes et naturelles de l'Université de Clermont},
title = {Informal proofs formally checked by machine},
url = {http://eudml.org/doc/80436},
volume = {60},
year = {1976},
}

TY - JOUR
AU - Aiello, Luigia
AU - Aiello, Mario
AU - Attardi, Giuseppe
AU - Prini, Gianfranco
TI - Informal proofs formally checked by machine
JO - Annales scientifiques de l'Université de Clermont. Mathématiques
PY - 1976
PB - UER de Sciences exactes et naturelles de l'Université de Clermont
VL - 60
IS - 13
SP - 31
EP - 53
LA - eng
UR - http://eudml.org/doc/80436
ER -

References

top
  1. 1 - J.A. Robinson - A machine oriented logic based on the resolution principle- Journal of the ACM - Vol.12 - 1965. Zbl0139.12303MR170494
  2. 2 - R. Ehrenfeucht, M. Rabin - There is no perfect proof procedure- Unpublished paper - Underground Jerusalem1972. 
  3. 3 - R. Milner - Logic for computable functions: description of a machine implementation- Artificial Intelligence Memo No 169 - Stanford University - 1972. 
  4. 4 - R. Weyhrauch, A. Thomas - FOL: a proof checker for first order logic- Artificial Intelligence Memo No 235 - Stanford University - 1974. 
  5. 5 - L. Aiello, M. Aiello, R. Weyhrauch - The semantics of PASCAL in LCF- Artificial Intelligence Memo No 221 - Stanford University - 1974. 
  6. 6 - M. Aiello, R. Weyhrauch - Checking proofs in the metamathematics of first order logic- Artificial Intelligence Memo No 222 - Stanford University1974 - Also in Proc. of the Fourth International Joint Conference on Artificial Intelligence - Tbilisi - 1975. 
  7. 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. 8 - D. Scott - An alternative approach to CUCH, IS WIM, OWHY- Unpublished paper- Underground Princeton - 1969. 
  9. 9 - R. Milner- Models of LCF - Artificial Intelligence Memo No 186 - Stanford University1973. 
  10. 10 - A. Church - The calculi of λ-conversion - Annals of Mathematical Studies No 6- Princeton- 1941. Zbl0026.24205JFM67.0041.01
  11. 11 - D. Scott - Continuous lattices - Technical Monograph PRG-7 - Oxford University - 1971. MR404073
  12. 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. 13 - M. Newey- Formal semantics of LISP with applications to program correctness - Thesis- Artificial Intelligence Memo No 257 - Stanford University - 1975. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.