Implementing first order logic in Modula-2 using an intuitionistic approach

ABSTRACT

A type theory is given using extended Modula-2 constructs, and a subset of first order logic is interpreted by certain type constructors of this theory. Under this theory, given a formula of the form for all x find a y such that R(x,y) as a specification, program synthesis amounts to proving the truce of the formula. During the proof a Modula-2 program is extracted automatically which meets the specification.

REFERENCES

• Bates 79: Joseph Louis Bates, A logic for correct program development, 1979
• Bates and Constable 85: Joseph L. Bates , Robert L. Constable, Proofs as programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.1, p.113-136, Jan. 1985 [doi>10.1145/2363.2528]
• Constable 83: R.L. Constable, Programs as proofs. Inf. Proc. Lett, V.16, N.3, 1983.
• Constable 85: R.L. Constable, Constructive mathematics as a programming logic I:some principles of theory. Ann. Discrete Math., V.24 (1985).
• Constable, Johnson, and Eichelaub 82: R. L. Constable , S. D. Johnson , C. D. Eichenlaub, An Introduction to the PL/CV2 Programming Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• Constable et al 86: R L Constable, Implementing mathematics with the Nuprl proof development system, Prentice-Hall, Inc., Upper Saddle River, NJ, 1986
• Heyting 56: A. Heyting, Intuitionism: An introduction. North Holland, Amsterdam, 1956.
• Martin_Löf 82: P. Martin Lof, Constructive mathematics and computer science, In Sixth international congress for logic, methodology, and philosophy of science. North Holland, Amsterdam, 1982.
• Martin_Löf 84: P. Martin Lof, Intuitionistic type theory. Studies in proof theory lecture notes, BIBLIOPOLIS, Napoli, 1984.
• Wirth 82: Niklaus Wirth, Programming in MODULA-2 (3rd corrected ed.), Springer-Verlag New York, Inc., New York, NY, 1985

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: Modula-2

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Program synthesis

General Terms:
Design, Languages, Performance, Theory, Verification