Étude et implémentation d’un système de déduction pour logique algorithmique. (Study and implementation of a reasoning system for algorithmic logic). (French) Zbl 0655.68118
The author presents LAPD, a prototype for automatic reasoning in logic for abstract programms.
Firstly, one defines the logic supported by LAPD modelled on Salwicki’s algorithmic logic. This logic contains the Hoare’s logic and can easily express some properties which are impossible to be expressed in the last one.
Secondly, the logic is studied in details (including the deduction system and an implementation based on logic for computable function (LCF) and its meta language (ML)). The system contains the integers and, accordingly, it is incomplete. A supplementary proof for this property is given.
Firstly, one defines the logic supported by LAPD modelled on Salwicki’s algorithmic logic. This logic contains the Hoare’s logic and can easily express some properties which are impossible to be expressed in the last one.
Secondly, the logic is studied in details (including the deduction system and an implementation based on logic for computable function (LCF) and its meta language (ML)). The system contains the integers and, accordingly, it is incomplete. A supplementary proof for this property is given.
Reviewer: D.Tātar
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B70 | Logic in computer science |
Software:
LCFReferences:
| [1] | 1. J. W. DE BAKKER, Recursive Programs as Predicates Transformers, in Formal Descriptions of Programming Concepts, E. J. NEUHOLD éd., North Holland, 1978. Zbl0392.68006 MR537905 · Zbl 0392.68006 |
| [2] | 2. J. W. DE BAKKER, Semantics and Termination of Non Deterministic Recursive Programs, in Automata, Languages and Programming, Edimburgh, 1976. Zbl0354.68021 · Zbl 0354.68021 |
| [3] | 3. B. S. CHLEBUS, Completness Proofs for Some Logics of Programs, Z. Math Logik und Grundlagen Math., vol. 28, 1982, p. 49-62. Zbl0491.03008 MR649907 · Zbl 0491.03008 · doi:10.1002/malq.19820280402 |
| [4] | 4. G. COUSINEAU, Les arbres à feuilles indicées : un cadre algébrique de définition des structures de contrôle, Thèse d’état, Paris, 1977. |
| [5] | 5. G. COUSINEAU, An Algebraic Definition of Control Structures, Theoretical computer science, vol. 12, 1980. Zbl0456.68015 MR585111 · Zbl 0456.68015 · doi:10.1016/0304-3975(80)90028-6 |
| [6] | 6. G. COUSINEAU, A Programmation en EXEL, Revue technique THOMSON-CSF, vol. 10, n^\circ 2, 1978, et Vol 11, n^\circ 1, 1979. |
| [7] | 7. G. COUSINEAU, The Algebraic Structure of Flowcharts, 8th MFCS Symposium 1979, Lecture Notes in Computer Science, n^\circ 74, Springer Verlag. |
| [8] | 8. E. ENGELER, Algorithmic Properties of Structures, Math. System Theory, 1, 1967. Zbl0202.00802 MR224473 · Zbl 0202.00802 · doi:10.1007/BF01705528 |
| [9] | 9. P. ENJALBERT, Contribution à la logique algorithmique. Systèmes de déduction pour arbres et schémas de programmes, Thèse d’état, Paris, 1981. |
| [10] | 10. P. ENJABERT, Systèmes de déduction pour les arbres et les schémas de programmes, RAIRO Informatique théorique, vol. 14, n^\circ 3 et vol. 14, n^\circ 4, 1980. Zbl0441.68007 · Zbl 0441.68007 |
| [11] | 11. P. ENJALBERT, Preuves de programmes, Revue technique THOMSON-CSF, vol.12, n^\circ 3, 1980. |
| [12] | 12. D. HAREL, First Order Dynamic Logic, Lecture Notes in Computer Science, n^\circ 68, 1979, Springer Verlag. Zbl0403.03024 MR567695 · Zbl 0403.03024 |
| [13] | 13. M. GORDON, R. MILNER et C. WADSWORTH, Edimburgh LCF, Lecture Notes in Computer Science, n^\circ 78, Springer Verlag. Zbl0421.68039 MR2049352 · Zbl 0421.68039 |
| [14] | 14. R. MILNER, Logic for Computable Functions Description of a Machine Implementation, Stanford Artificial Intelligence Project, Memo AIM-169, Computer Science Department Report CS 288, mai 1972. |
| [15] | 15. R. MILNER, LCF : A Way of Doing Proofs with a Machine. Department of Computer Science, Univ. of Edimburgh. · Zbl 0423.68049 |
| [16] | 16. R. MILNER, A Methodology for Performing Rigorous Proofs About Programs, Proc lst I.B.M. Symposium on Mathematical Foundations of Computer Science, 1976. |
| [17] | 17. R. MILNER, A Theory ofType Polymorphism in Programming, Journal of computer and system science, n^\circ 17, 1978. Zbl0388.68003 MR516844 · Zbl 0388.68003 · doi:10.1016/0022-0000(78)90014-4 |
| [18] | 18. R. MILNER, HOW ML evolved, in Polymorphism, vol. 1, n^\circ 1, janvier 1983, Bell Cabs., L. CARDELLI et D. MCQUEEN éd. |
| [19] | 19. G. MIRKOWSKA, Propositionnal Algorithmic Theory of Arithmetic, Communication manuscrite. |
| [20] | 20. G. MIRKOWSKA, Propositionnal Algorithmic Logic, Lecture Notes in Computer Science, n^\circ 74, 1979, Springer Verlag. |
| [21] | 21. G. MIRKOWSKA, Algorithmic Logic and its Application in the Theory of Programs, Fundamentale Informaticae, vol. I, n^\circ 1 et vol. 1, n^\circ 2, 1977. Zbl0358.68036 MR660300 · Zbl 0358.68036 |
| [22] | 22. L. NOLIN et G. RUGGIU, A Formalization of EXEL, Assoc. Comput. Mathematics SIGACT-SIGPLAN, Symposium on the Principles of Programming Languages, Boston, 1973. Zbl0308.68011 · Zbl 0308.68011 |
| [23] | 23. H. RASIOWA, Algorithmic Logic, I.C.S. P.A.S. Reports n^\circ 281, Institute of Computer Science, Academic des Sciences, Varsovie, 1977. |
| [24] | 24. A. SALWICKI, Formalized Algorithmic Languages, Bull. Acad. Pol. Sci. Ser. Math. Astr. Phys., vol. 18, 1970, p. 227-232. Zbl0198.02801 MR270852 · Zbl 0198.02801 |
| [25] | 25. A. SALWICKI, On Algorithmic Theory of Stacks, Fundamentae Informaticae, vol. III, n^\circ 1, 1980. Zbl0441.68013 MR596731 · Zbl 0441.68013 |
| [26] | 26. A. SALWICKI, On Algorithmic Logic and its Applications, Internal Report, Pol. Ac. of Sci., 1978. · Zbl 0387.68027 |
| [27] | 27. A. SALWICKI, An Algorithmic Approach to Set Theory, Proc. F.C.T. 1977, Lecture Notes in Computer Science, n^\circ 56, 1977, Springer Verlag. Zbl0403.68005 MR483659 · Zbl 0403.68005 |
| [28] | 28. F. GARCIA, Étude et implémentation en ML/LCF d’un système de déduction pour logique algorithmique, Thèse Docteur-Ingénieur, juin 1985, Université Paris-VII. |
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.
