×
Aiello, Luigia; Aiello, Mario; Attardi, Giuseppe; Prini, Gianfranco

Informal proofs formally checked by machine. (English) Zbl 0352.68110

Ann. Sci. Univ. Clermont 60, Math. 13 (Actes Semin. int. Ete Logique, Clermont-Ferrand 15-26 Juillet 1975), 31-53 (1976).
Page: −5 −4 −3 −2 −1 ±0 +1 +2 +3 +4 +5 Show Scanned Page
scan of Zbl 0352.68110

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q25 Analysis of algorithms and problem complexity

Software:

MAGMA-Lisp; LCF
Cite Review PDF
Full Text: Numdam EuDML

References:

[1] 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 · Zbl 0139.12303 · doi:10.1145/321250.321253
[2] 2 - R. Ehrenfeucht , M. Rabin - There is no perfect proof procedure - Unpublished paper - Underground Jerusalem 1972 .
[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 . · Zbl 0368.68019
[6] 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 . · Zbl 0646.03009
[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 . · Zbl 0297.68072
[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 University 1973 . · Zbl 0364.02018
[10] 10 - A. Church - The calculi of \lambda -conversion - Annals of Mathematical Studies No 6 - Princeton - 1941 . Zbl 0026.24205 | JFM 67.0041.01 · Zbl 0026.24205
[11] 11 - D. Scott - Continuous lattices - Technical Monograph PRG - 7 - Oxford University - 1971 . MR 404073 · Zbl 0239.54006
[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 .
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.