Abstract
Throughout the centuries the great themes of pure mathematics, which were conceived without thought of usefulness, have been transformed to essential tools for scientific understanding. This lecture is devoted to the theme that this transformation is now happening to mathematical logic, and that a subject of applied logic is emerging akin in its range and power to classical applied mathematics. This adds further weight to the argument that the investment of intellectual and material capital in mathematical research pays a rich dividend.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
A. V. Aho and J. D. Ullman [ 1979 ], “Universality of data retrieval languages,” Proc. Sixth ACM Symp. on POPL, 110–117.
J. F. Allen [ 1981 ], “An interval-based representation of temporal knowledge,” Proc. Seventh JJCAJ, Vancouver, 221–226.
J.F. Allen and J.A. Koomen [ 1983 ], “Planning using a temporal world model,” Proc. Eighth IJCAI, 741–747.
H. Andreka and I. Nemeti [ 1976 ], “The generalized completeness of Horn predicate logic as a programming language,” DAI Report 21, University of Edinburgh.
P. B. Andrews [ 1982 ], “A look at TPS,” Sixth Conf. on Automated Deduction, Lecture Notes in Computer Science 138, Springer-Verlag, New York.
K. Apt [ 1981 ], “Ten years of Hoare logic, a survey (part 1),” ACM Trans, on Prog. Languages and Systems, 3, 431–483.
K. Apt [ 1985 ], Logics and Models of Concurrent Systems (K. Apt, ed.), NATO ASI Series, Springer-Verlag, Berlin.
K. Apt and M. H. van Emden [ 1982 ], “Contributions to the theory of logic program-ming,” J. ACM, to appear.
K. Balogh [ 1975 ], “Software applications of mathematical logic” (Hungarian), Proc. Conf. Prog. Systems, Szeged, Hungary, 26–44.
K. Balogh [ 1981 ], “On an interactive program verifier for PROLOG programs,” Proc. of Coll. on Math. Logic in Programming, Salgotarjan, Hungary, 1978; republished (B. Domoki and T. Gergely, eds.), North Holland Pub. Co., Amsterdam.
L. Banachowski, A. Kreczmar, G. Mirkowska, H. Rasiowa and A. Salwicki [1977], “An introduction to algorithmic logic,” in Mathematical Foundations of the Theory of Programs ( Mazurkiewitz and Pawlak, eds. ), Warsaw, 7–99.
H. P. Barendregt [ 1984 ], The Lambda Calculus (revised edition), Studies in Logic 103, North Holland, Amsterdam.
H. Barringer [ 1985 ], A Survey of Verification Techniques for Parallel Programs, Lecture Notes in Computer Science 191, Springer-Verlag, Berlin.
J. L. Bates and R. L. Constable [ 1982 ], “Definition of micro-PRL,” Technical Report TR 82–492, Dept. Computer Science, Cornell University, Ithaca, New York.
J. L. Bates and R. Constable [ 1985 ], “Proofs as programs,” ACM Trans, on Program-ming Languages and Systems, 7.
M. Beeson [ 1984 ], “Proving programs and programming proofs,” Proc. Seventh Intl. Cong. Logic, Phil., and Method, of Sci., North Holland, Amsterdam.
E. Berlekamp, J. Conway and R. Guy [ 1982 ], Chapter 25 of Winning Ways, Academic Press, New York.
J. Benthem Van [1983], The Logic of Time, Reidel.
W. W. Bledsoe [ 1977 ], “Non-resolution theorem proving” Art. Intell, 9, 1–35.
W. Bledsoe and P. W. Loveland [ 1985 ], Special Session on Automatic Theorem Proving, Cont. Math. 29, Amer. Math. Soc., Providence, Rhode Island.
M. Bergmann and H. Kanoui [ 1973 ], “Application of mechanical theorem proving to symbolic calculus,” Third Intl. Symp. of Advanced Computing Methods in Theoretical Physics, C.N.R.S., Marseille.
E. Bishop [ 1967 ], Foundations of Constructive Analysis, McGraw Hill, New York.
E. Bishop [ 1970 ], “Mathematics as a numerical language,” in Intuitionism and Proof Theory ( J. Myhill et al., eds.), North Holland, Amsterdam.
D. G. Bobrow [1980], Special Issue on Non-Monotonic Logic (K. Bobrow, ed.), Art. Intell., 13.
G. Boole [1854], Laws of Thought’, in Collected Logical Works, Open Court, La Salle, Illinois, 1952.
K. A. Bowen and R. A. Kowalski [ 1982 ], “Amalgamating language and metalanguage in logic programming,” in Clark and Tärnlund.
R. S. Boyer and J. S. Moore [ 1973 ], “Proving theorems about LISP functions,” Proc. IJCAI3 (N. Nilsson, ed.).
R. S. Boyer and J. S. Moore [ 1979 ], A Computational Logic, Academic Press, New York.
R. J. Brachman and H. J. Levesque [ 1985 ], Readings in Knowledge Representation, Morgan Kauffman, Los Altos, California.
B. Bradley and M. Schwartz [1979], Possible Worlds, Oxford.
L. E. J. Brouwer [ 1975 ], Collected Works 1 ( A. Heyting, ed.), North Holland, Ams-terdam.
Lee Brownston, R. Farrell, E. Kant and N. Martin [ 1985 ], Programming Expert Systems in OPS5, Addison-Wesley, Reading, Massachusetts.
de Bruijn [ 1980 ], “A survey of Project Automath,” in To H. B. Curry: Essays on Combinatory Logic, Calculus, Lambda Calculus, and Proof Theory ( J. P. Seldin and J. R. Hindley, eds.), Academic Press, London.
M. E. Bruynooghe [ 1976 ], “An interpreter for predicate logic programs I,” Report CW10, Appl. Math, and Prog. Division, Katholieke Universiteit, Leuven, Bel-gium.
A. Bundy [1983], The Computer Modelling of Mathematical Reasoning, Academic Press.
W. Bürge [ 1978 ], Recursive Programming Techniques, Addison-Wesley, Reading, Massachusetts.
A. W. Burks [1970], Essays on Cellular Automata, University of Illinois Press.
R. M. Burstall and J. Darlington [ 1977 ], “A transformation system for developing recursive programs,” J. ACM, 24, 44–67.
J. A. Campbell [ 1984 ], Implementations of PROLOG, Wiley, New York.
C. L. Chang and R. Lee [ 1973 ], Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York.
A. Church [1932/33], “A set of postulates for the foundations of logic,” Ann. Math., 33, 346–366
A. Church [ 1941 ], The Calculi of Lambda-Conversion, Ann. Math. Studies 6, Princeton University Press, Princeton, New Jersey.
A. Church and J. B. Rosser [ 1936 ], “Some properties of conversion,” Trans. Amer. Math. Soc., 39, 472–482.
K. L. Clark [ 1978 ], “Negation as failure,” in Gallaire and Minker.
K. L. Clark and M. H. van Emden [ 1981 ], “Consequence verification of flowcharts,” IEEE Trans, on Software Engineering, SE-7, 52–60.
K. L. Clark and F. G. McCabe [ 1982 ], “PROLOG: a language for implementing expert systems,” in Machine Intelligence 10 (J. E. Hayes, D. Michie and Y. H. Pao, eds.), Ellis Horwood Ltd., Chichester, England, 455–470.
K. L. Clark and S. Sickel [ 1977 ], “Predicate logic: a calculus for deriving programs,” Proc. Fifth IJCAI, Cambridge, Massachusetts.
K. L. Clark and S.-A. Tarnlund [ 1977 ], “A first order theory of data and programs,” Proc. IFIP-77, Toronto, North Holland, Amsterdam, 939–944.
K. L. Clark and S.-A. Tärnlund [ 1982 ], Logic Programming, APIC Studies in Data Processing 16, Academic Press, London.
W. F. Clocksin and C. S. Mellish [ 1984 ], Programming in PROLOG, Springer-Ver lag, Berlin.
E. F. Codd [ 1970 ], “A relational model of data for large shared data banks,” Comm. ACM, 13, 377–387.
E. F. Codd [ 1971 ] “A database sublanguage founded on the relational calculus,” Proc. ACM SIGFIDET Workshop on Data Description, Access, and Control (Codd and Dean, eds.), ACM, San Diego, 35–68.
E. F. Codd [ 1972 ], “Relational completeness of data base sublanguages,” in Data Base Systems (R. Rustin, ed.), Courant Comp. Symp. 6, Prentice Hall, Englewood Cliffs, New Jersey, 65–98.
A. Colmerauer, H. Kanoui, R. Pasero and P. Roussel [ 1972 ], “Un système de commu-nication homme-machine en Français,” Preliminary Report, Art. Intell. Group of Aix-Marseille, Luminy, France.
A. Colmerauer, “Metamorphosis grammars,” in Natural Language Communication with Computers (L. Bole, ed.), Lecture Notes in Computer Science 63, Springer- Verlag, Berlin, 133–189.
A. Colmerauer [ 1979 ], “Sur les bases théoriques de PROLOG,” Group Programmation et Languages AFC ET, Division Théorique et Technique de l’Informatique 9.
A. Colmerauer, H. Kanoui and M. van Canegham [ 1981 ], “Last steps toward an ultimate PROLOG,” Proc. Seventh IJCAI, Vancouver.
R. L. Constable [ 1971 ], “Constructive mathematics and automatic programming,” Proc. IFIP Congress, Ljubljana, 229–233.
R. L. Constable [ 1983 ], “Partial functions in constructive formal theories,” Proc. Sixth G. I. Conf., Lecture Notes in Computer Science 135, Springer-Ver lag, Berlin.
R. L. Constable [ 1985 ], “Constructive mathematics as a programming logic I: some principles of theory,” Annals of Discrete Mathematics, 2, 21–38.
R. L. Constable [ 1985 ], “The semantics of evidence,” Technical Report TR 85-684, Dept. Computer Science, Cornell University, Ithaca, New York.
R. L. Constable [ 1985 ], “Investigations of type theory in programming logics and in-telligent systems,” Technical Report TR 85–701, Dept. Computer Science, Cornell University, Ithaca, New York.
R. L. Constable and M. J. O’Donnell [ 1978 ], A Programming Logic, Winthrop, Cambridge, Massachusetts.
H. B. Curry [ 1929 ], “An analysis of logical substitution,” Am. J. Math., 51, 363–384.
H. B. Curry [ 1930 ], “Grundlagen der Kombinatorischen Logik,” Am. J. Math, 52, 509–536, 789–834.
V. Dahl [ 1981 ], “On data base system development through logic,” Research Report, Dept. of Mathematics, Faculty of Exact Sciences, University of Buenos Aires, Argentina.
M. Davis [ 1980 ], “The mathematics of non-monotonic reasoning,” Art. Intell, 13, 73–80.
M. Davis and H. Putnam [ 1960 ], “A computing procedure for quantification theory,” J ACM, 7, 201–215.
E. W. Dijkstra [ 1976 ], A Discipline of Programming, Prentice Hall, Englewood Cliffs, New Jersey.
J. Doyle [ 1979 ], “A truth maintenance system,” Art. Intell, 12, 231–272.
J. Doyle [ 1983 ], “The ins and outs of reason maintenance,” IJCAI, 8, 349–351.
R. O. Duda, P. E. Hart and N. J. Nilsson [ 1976 ], “Subjective Bayesian methods for rule-based inference systems,” Proc. Nat. Comp. Conf. (AFIPS Conference Proc. 45), 1075–1082.
H. Ehrig and B. Mahr [ 1985 ], Fundamentals of Algebraic Specification, Springer- Verlag, Berlin.
E. Engeler [ 1967 ], “Algorithmic properties of structures,” Math. Syst. Theory, 1, 183–195.
L. Fox [ 1966 ], Advances in Programming and Non-Numerical Computation, Perga- mon Press, London.
M. J. Fischer and R. E. Ladner [ 1978 ], “Propositional dynamic logic of regular pro-grams,” J. of Comp. Sci. and Sys. Sci., 18, 194–211.
R. Floyd [ 1967 ], “Assigning meanings to programs,” in Mathematical Aspects of Computer Science ( J. T. Schwartz, ed.), Proc. Symp. Appi. Math. XIX, Amer. Math. Soc., Providence, Rhode Island, 19–32.
D. Gabbay [ 1982 ], “Intuitionistic basis for non-monotonic logic,” Proc. Conf. on Automated Deduction, Lecture Notes in Computer Science 6, Springer-Verlag, Berlin.
D. Gabbay and F. Guenthner [1983/4], Handbook of Philosophical Logic.
D. Gabbay, A. Pnueli, S. Shelah and J. Stain [ 1980 ], “On the temporal logic of programs,” Proc. 18th Symp. on Math. Found, of Computer Science, Lecture Notes in Computer Science 54, Springer-Ver lag, Berlin, 112–152.
H. Gallaire [ 1981 ], “The impact of logic on databases,” Proc. Seventh Conf. on Very Large Databases, Cannes, France.
H. Gallaire and C. Lasserre [ 1979 ], “Controlling knowledge deduction in a declarative approach,” Proc. IJCAI 6, Tokyo.
H. Gallaire and C. Lasserre [1980], “A control metalanguage for Logic Programming,” in Tärnlund [ 1980 ].
H. Gallaire and J. Minker [ 1978 ], Logic and Databases, Plenum Press, New York.
H. Gallaire, J. Minker and J. M. Nicholas [ 1980 ], Advances in Database Theory, vol. 1, Plenum Press, New York.
M. R. Garey and D. S. Johnson [ 1979 ], Computers and Intractability: A Guide to the Theory of N P-Completeness, Freeman, New York.
G. E. Gentzen [ 1969 ], The Collected Works of Gerhard Gentzen (M. E. Szabo, ed.), North Holland, Amsterdam.
K. Godei [ 1930 ], “Die Vollständigkeit der Axiome des Logischen Functionenkalkuls,” Monat. Math. Phys., 37, 349–360, in van Heijenoort.
K. Godei [ 1931 ], “Ueber Formal Unentscheidbare Sätze der Principia Mathematica und Verwandter Systeme, I,” Monatsh. Math., 38, 173–198, in van Heijenoort.
A. Goodal [ 1985 ], The Guide to Expert Systems, Learned Information (Europe), Besselsleigh Rd. Abingdon, Oxford, England.
M. J. C. Gordon [ 1973 ], Evaluation and Denotation of Pure LISP, A Worked Example in Semantics, Ph.D. Diss., University of Edinburgh.
M. J. C. Gordon [ 1979 ], The Denotational Description of Programming Languages, Springer-Verlag, Berlin.
M. J. C. Gordon, R. Milner and C. Wadsworth [1979], Edinburgh LCF. A Mechanical Logic of Computation, University of Edinburgh.
C. C. Green [ 1969a ], The Application of Theorem Proving Question-Ansewring Systems, Ph.D. Diss., Stanford. C. C. Green [1969b], “The application of theorem proving to problem solving,” Proc. IJCAI 1, Washington, D.C., 219–240.
C. C. Green [ 1969c ], “Theorem proving by resolution as a basis for question-answering systems,” in Machine Intelligence 4, Edinburgh University Press, 183–205.
Peter Grey [ 1984 ], Logic, Algebra, and Databases, Wiley, New York.
D. Gries [ 1981 ], The Science of Programming, Springer-Verlag, Berlin.
Y. Gurevich [ 1985 ], “Logic and the challenge of computer science,” Technical Report CRL-TR-10-85, University of Michigan Computing Laboratory.
J. Halpern, Z. Manna and B. Moszkowski [ 1983 ], “A hardware semantics based on temporal intervals,” Proc. 19th Intl. Coll. on Automata, Languages, and Programming, Lecture Notes in Computer Science 54, 278–292.
A. Hansson and S. A. Tärnlund [ 1979 ], “A natural programming calculus,” Proc. IJCAI 6, Tokyo.
D. Harel [ 1979 ], First Order Dynamic Logic, Lecture Notes in Computer Science 68, Springer-Verlag, Berlin.
D. Harel [ 1984 ], “Dynamic logic,” in Gabbay and Guenthner.
D. Harel, D. Kozen and R. Parikh [ 1982 ], “Process logic: expressiveness, decidability, completeness,” J. Comp. Sys. Sci., 25, 144–170.
D. Harel, A. Meyer and V. R. Pratt [ 1977 ], “Computability and completeness in the logic of programs,” Ninth ACM Symp. Theory of Comp., 261–268.
D. Harel, A. Pnueli and J. Stavi [ 1983 ], “Propositional dynamic logic of nonregular programs,” J. Comp. Sys., 16, 222–243.
P. J. Hayes [ 1977 ], “In defense of logic,” IJCAI, 5, 559–565.
P. Henderson [ 1980 ], Functional Programming: Application and Implementation, Prentice Hall, Englewood Cliffs, New Jersey.
J. Herbrand [ 1930 ], “Researches in the theory of demonstration, investigations in proof theory,” in van Heijenoort.
A. Heyting [ 1966 ], Intuitionism, North Holland, Amsterdam.
D. Hilbert [ 1902 ], The Foundations of Geometry, Open Court Pub. Co., La Salle, Illinois.
R. Hill [ 1974 ], “Lush-resolution and its completeness,” DCL Memo 78, Dept. Art. Intell., University of Edinburgh.
J. R. Hindley [ 1983 ], “The completeness for typed lambda terms,” Theor. Comp. Sci., 22, 1–17.
J. R. Hindley, B. Lercher and J. P. Seldin [1972], Introduction to Combinatory Logic, Cambridge University Press.
C. A. R. Hoare [ 1969 ], “An axiomatic basis for computer programming,” Comm. Assoc. Comp. Mach., 12, 576–583.
C. A. R. Hoare [ 1985 ], Communicating Sequential Processes, Prentice Hall, Englewood Cliffs, New Jersey.
C. J. Hogger [ 1978 ], “Program synthesis in predicate logic,” Proc. AISB/GI Conf. on AI, Hamburg, Germany.
C. J. Hogger [ 1982 ], “Logic Programming and program verification,” in Programming Technology: State of the Art Report ( P. J. L. Wallis, ed.), Pergamon Infotech Ltd., Maidenhead, England.
C. J. Hogger [1984], Introduction to Logic Programming, Academic Press.
J. E. Hopcroft and J. D. Ullman [ 1979 ], Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, Reading, Massachusetts.
G. Huet [ 1974 ], “A unification algorithm for typed lambda calculus,” Note de Travail A055, Inst, de Rech. 250, Lab. de Rech, en Informatique et d’Automatique.
G. Huet [ 1977 ], “Confluent reductions, abstract properties, and applications to term rewriting systems,” 18th IEEE Symp. on the Found, of Comp. Sci., 30–45.
G. Huet and D. C. Oppen [ 1980 ], “Equations and rewrite rules: a survey,” in Formal Languages: Perspectives and Open Problems (R. Book, ed. ), Academic Press.
G. E. Hughes and M. J. Cresswell [ 1968 ], An Introduction to Modal Logic, Methuen, London.
N. Immerman [ 1982 ], “Relational queries computable in polynomial time,” 14th ACM Symp. Theor. of Comp., 147–152.
B. E. Jacobs [ 1985 ], Applied Database Logic, vol. 1, Prentice Hall, Englewood Cliffs, New Jersey.
J.-P. Jouannaud [ 1985 ], Rewriting Techniques and Applications (J.-P. Jouannaud, ed.), Lecture Notes in Computer Science 202, Springer-Verlag, Berlin.
K. Kahn [ 1981 ], “Uniform — a language based on unification which unifies (much of) LISP, PROLOG, and ACT1,” IJCAI-81.
W. Kamp [ 1968 ], Tense Logics and the Theory of Linear Order, Ph.D. Diss., UCLA.
S. C. Kleene [ 1936 ], “A-definability and recursiveness,” Duke Math. J., 2, 340–353.
S. C. Kleene [ 1950 ], Introduction to Metamathematics, Van Nostrand, New York.
F. Kluzniak and S. Szpakowicz [1985], PROLOG for Programmers, Academic Press.
D. E. Knuth and P. B. Bendix [ 1970 ], “Simple word problems in universal algebra,” in Computational Problems in Abstract Algebra (Leech, ed.), 263–297.
R. A. Kowalski [1970], Studies in the Completeness and Efficiency of Theorem Proving by Resolution, Ph.D. Diss., University of Edinburgh.
R. A. Kowalski [ 1971 ], “Linear resolution with selector function,” Art. Intell., 2, 227–260.
R. A. Kowalski [ 1974a ], “Logic for problem solving,” DCL Memo 75, Dept. Art. Intell., University of Edinburgh.
R. A. Kowalski [ 1974b ], “Predicate logic as a programming language,” Proc. IFIP-74, North Holland, Amsterdam, 569–574.
R. A. Kowalski [ 1978 ], “Logic for data descriptions,” in Gallaire and Minker.
R. A. Kowalski [ 1979a ], “Algorithm = Logic + Control,” Comm. ACM, 22, 424–431.
R. A. Kowalski [ 1979b ], Logic for Problem Solving, Art. Intell. Series 7, Elsevier- North Holland, New York.
R. A. Kowalski [ 1981 ], “Logic as a database language,” Proc. of Workshop on Database Theory, Cetraro, Italy.
R. A. Kowalski [ 1983 ], “The relationahip between Logic Programming and logic speci-fication,” BCS-FACS Workshop on Program Specification and Verification, University of York.
R. A. Kowalski and D. Kuehner [ 1971 ], “Linear resolution with selector function,” Art. Intell., 2, 227–260.
D. Kozen and R. Parikh [ 1982 ], “An elementary proof of the completeness of PDL,” Theor. Comp. Sci., 14 (1981), 113–118.
G. Kreisel [ 1957 ], “Countable functional” Summaries of talks given at the AMS Summer Institute in Recursion Theory, 1957.
G. Kreisel [ 1959 ], “Interpretation of analysis by means of constructive functionals of finite types,” in Constructivity in Mathematics (A. Heyting, ed.), North Holland, Amsterdam, 101–128.
S. Kripke [ 1963 ], “Semantical considerations on modal logic,” Acta Phil. Fennica, 16, 83–94.
S. Kripke [1972], “Naming and necessity,” in Semantics of Natural Language ( Harmon and Davidson, eds. ), Reidel, 253–356.
P. J. Landin [ 1964 ], “The mechanical evaluation of expressions,” Comp. J., 6, 308– 320.
P. J. Landin [ 1965 ], “A correspondence between Algol 60 and Church’s lambda calculus,” ACM, 8, 158–165.
P. J. Landin [ 1966a ], “A lambda calculus approach,” in Advances in Programming and Non-Numerical Computation (L. Fox, ed.), Pergamon Press, Oxford, 97– 141.
P. J. Landin [ 1966b ], “The next 700 programming languages,” Comm. ACM, 9, 157– 164.
D. B. Lenat [ 1977 ], “Automated theory formation in mathematics,” Proc. IJCAI-77 (R. J. Reddy, ed. ), 1093–1105.
C. I. Lewis and C. H. Langford [1932], Symbolic Logic, New York.
J. W. LLoyd [ 1984 ], Foundations of Logic Programming, Springer-Verlag, Berlin.
D. Loveland [ 1978 ], Automatic Theorem Proving: A Logical Basis, North Holland, Amsterdam.
W. Lukaszewicz [ 1983 ], “General approach to non-monotonic logics,” Proc. Eighth IJCAI, Karlsruhe, 352–354.
J. McArthur [1979], Tense Logic, Reidel.
J. McCarthy [1960], “Recursive functions of symbolic expressions and their computation by machine,” Comm. Assoc. Comp. Mach., 3, 184–195.
J. McCarthy [1962], “Computer programs for checking mathematical proofs,” in Re-cursive Function Theory (Proc. Symp. Pure Math.), Amer. Math. Soc., Provi-dence, Rhode Island, 219–227.
J. McCarthy [ 1963a ], “A basis for a mathematical theory of computation,” in Computer Programming and Formal Systems ( P. BrafTort and D. Hirschberg, eds.), North Holland, Amsterdam, 33–70.
J. McCarthy [1963b], “Towards a mathematical science of computation,” in Information Processing, North Holland, Amsterdam, 21–28.
J. McCarthy [1965], “Problems in the theory of computation,” Proc. of the IFIPS Congress, 219–222.
J. McCarthy [ 1980 ], “Circumscription as a form of non-monotonic reasoning,” Art. Intell., 13, 27–39.
J. McCarthy, P. W. Abrahams, D. J. Edwards, T. P. Hart and M. I. Levin [1965], LISP 1.5 Programmer’s Manual, MIT Press, Cambridge, Massachusetts.
D. McDermott [ 1982 ], “Non-monotonic logic II: non-monotonic modal theories,” J ACM, 29, 33–57.
D. McDermott and J. Doyle [ 1980 ], “Non-monotonic logic I,” Art. Intell., 13, 41–72.
Z. Manna [ 1974 ], Mathematical Theory of Computation, McGraw-Hill, New York.
Z. Manna [ 1980 ], “Logic of programs,” Proc. IFIPS Congress, Toyko and Melbourne, 41–51.
Z. Manna, S. Ness and J. E. Vuillemin [1972], “Inductive methods for proving properties of programs,” Proc. of ACM Conference, New York.
Z. Manna and A. Pnueli [1970], “Formalization of properties of functional programs,” J. Assoc. Comp. Mach., 17, 555–569.
Z. Manna and A. Pnueli [1979], “The modal logic of programs,” Proc. Sixth Intl. Symp. on Automata, Languages, and Programming, Graz, Austria, Lecture Notes in Computer Science 71, Springer-Verlag, Berlin, 385–409.
Z. Manna and A. Pnueli [ 1982 ], “Verification of concurrent programs: the temporal framework,” in The Correctness Problem in Computer Science ( R. S. Boyer and J. S. Moore, eds.), International Lecture Series in Computer Science, Academic Press, 215–273.
Z. Manna and R. Waldinger [ 1980 ], “A deductive approach to program synthesis,” ACM Trans, on Prog. Languages and Semantics, 2, 90–121.
Z. Manna and P. Wolper [ 1984 ], “Synthesis of communicating processes from temporal logic,” ACM Trans, on Programming and Systems, 6, 63–93.
A. Martelli and U. Montanari [1976], “Unification in linear time and space,” Internal Report B76-16, University of Pisa.
P. Martin-Löf [1975], “An intuitionistic theory of types: predicative part,” in Logic Colloquium 1973 ( H. E. Rose and J. C. Shepherdson, eds.), North Holland, Amsterdam.
P. Martin-Löf [1982], “Constructive mathematics and computer programming,” in Sixth Intl. Cong, for Logic, Phil, and Method, of Science, North Holland, Amsterdam.
Mathlab Group [1977], MACSYMA Reference Manual, Technical Report, MIT. R. E. Milne [ 1974 ], The Formal Semantics of Computer Languages and Their Imple-mentations, Ph.D. Thesis, University of Cambridge.
R. E. Milne and C. A. Strachey [1976], A Theory of Programming Language Semantics (2 vols.), Chapman and Hall, London, and John Wiley, New York.
A. J. R. G. Milner [ 1973 ], “An approach to the semantics of parallel programs,” Proc. Convegno di Information Teorica, Instituto di Elaborazione della Informazione, Pisa.
A. J. R. G. Milner [1975], “Processes: a mathematical model of computing agents,” in Logic Colloquium ’73 (H. E. Rose and J. C. Shepherdson, eds. ), 157–174.
A. J. R. G. Milner [1980], A Calculus of Communicating Systems, Lecture Notes in Computer Science 92, Springer-Verlag, New York.
J. Minker [ 1977 ], “Control structure of a pattern directed search system,” Technical Rept. 503, Dept. of Computer Science, University of Maryland.
R. Moore [ 1983 ], “Semantical considerations on nonmonotonic logic,” Proc. Eighth IJCAI, 272–279.
R. C. Moore [ 1985 ], “Semantical constructions on nonmonotonic logic,” AI J, 25, 75–94.
J. H. Morris [ 1968 ], Lambda Calculus Models of Programming Languages, Ph.D. Diss., MIT.
B. Moszkowski and Z. Manna [ 1983 ], “Reasoning in interval temporal logic,” in Logic of Programs (Clarke and Kozen, eds.), Lecture Notes in Computer Science 164, 371–381.
P. Naur [ 1969 ], “Proofs of algorithms by general snapshots,” BIT, 6, 310–316.
A. Nerode [ 1959 ], “Some Stone spaces and recursion theory,” Duke J. Math., 26, 397–405.
N. Nilsson [1980], Principles of Artifìcial Intelligence, Tioga Pub. Co., Palo Alto, California.
B. Nordstrom [1981], “Programming in constructive set theory: some examples,” Proc. 1981 ACM Conf. on Functional Programming Languages and Computer Architecture, 48–54.
P. Nordstrom and K. Petersson [1983], “Types and specification,” in Information Processing 83 (R. E. A. Mason, ed.), North Holland, Amsterdam, 915–920.
B. Nordstrom and J. Smith [1983], “Why type theory for programming?”, Proc., Computer Science Memo 80, Programming Methodology Group, Dept. Computer Science, University of Göteborg.
M. J. O’Donnell [985], Equational Logic as a Programming Language, MIT Press, Cambridge, Massachusetts.
S. Owicki and D. Gries [1976], “Verifying properties of parallel programs: an axiomatic approach,” CACM, 19, 279–284.
S. Owicki and D. Gries [1976], “An axiomatic proof technique for parallel programs,” Acta Informatica, 6.
R. Parikh [1978], “The completeness of propositional dynamic logic,” in Math. Found, of Computer Science 1978, Seventh Symp., Lecture Notes in Computer Science 64, Springer-Verlag, Berlin, 403–415.
R. Parikh [1985], Logics of Programs (R. Parikh, ed. ), Lecture Notes in Computer Science 193.
M. S. Paterson and M. N. Wegman [1976], “Linear unification,” Proc. Eighth ACM Symp. on Theor. of Comp., 181–186.
L. M. Pereira and L. F. Monteiro [ 1981 ], “The semantics of parallelism and coroutining in Logic Programming,” Coll. on Math. Logic in Programming, Salgotarjan, Hungary, North Holland, Amsterdam, 611–657.
G. D. Plotkin [1972], “Building-in equational theories,” Mach. Intell, 7 ( B. Meitzer and D. Michie, eds. ), 73–90.
G. D. Plotkin [1976], “A power domain construction,” SIAM J. on Comp., 5, 452–487.
A. Pnueli [ 1977 ], “The temporal logic of programs,” Proc. 18th IEEE Symp. on Found. Comp., Providence, Rhode Island.
V. Pratt [ 1976 ], “Semantical considerations on Floyd-Hoare logic,” 17th Annual IEEE Symp. on Found, of Comp. Sci., New York, 109–121.
V. Pratt [1980], “Applications of modal logic to programming,” Studia Logica, 39, 257–274.
PRL Staff [1985], Implementing Mathematics with the Nuprl Proof Development System, Computer Science Dept., Cornell University.
P. Raulefs, J. Siekmann, P. Szabo and E. Unvericht [1978], “A short survey of the state of the art in matching and unification problems,” AISB Quarterly, 32, 17–21.
R. Reiter [1978], “On closed world data bases,” in Gallaire and Minker [ 1978 ].
R. Reiter [1980], “A logic for default reasoning,” Art. Intell., 81–132.
R. Reiter [1985], “A theory of diagnosis from first principles,” Technical Report 187/86, Dept. of Computer Science, University of Toronto.
G. Robinson and L. Wos [1969], “Paramodulation and theorem proving in first order logic with equality,” in Machine Intelligence 4 (B. Meitzer and D. Michie, eds.), Edinburgh University Press, Edinburgh, 135–150.
J. A. Robinson [1965], “A machine-oriented logic based on the resolution principle,” J. Assoc. Comp. Mach., 12, 23–41.
J. A. Robinson [1965], “Automatic deduction with hyper-resolution,” Intl. J. of Comp. Math., 1, 227–234.
J. A. Robinson [1971], “Computational logic: the unification algorithm,” in Machine Intelligence 6 (B. Meitzer and D. Mitchie, eds.), Edinburgh University Press, Edinburgh, 63–72.
J. A. Robinson [ 1979 ], Logic: Form and Function. The Mechanization of Deductive Reasoning, Edinburgh University Press, Edinburgh.
J. A. Robinson and E. E. Siebert [ 1980 ], “Logic Programming in LISP,” Research Report, School and Information and Computer Science, Syracuse University, Syracuse, New York.
J. A. Robinson and L. Wos [1969], “Paramodulation and theorem proving in first order logic with equality,” in Machine Intelligence (D. Michie, ed. ), Edinburgh University Press, 103–133.
B. K. Rosen [ 1974 ], “Correctness of parallel programs: the Church-Rosser approach,” IBM Research Rpt. RC5107, T. J. Watson Research Center, Yorktown Heights, New York.
P. Roussel [ 1975 ], “PROLOG: manuel de reference,” Research Report, Art. Intell. Group of Aix-Marseille, Luminy, France.
A. Salwicki [ 1970 ], “Formalized algorithmic languages,” Bull. Acad. Polon. Sci. Math. Astron. Phy, 18, 227–232. Schröder [1890], Vorlesungen über die Algebra der Logik (3 vol., 1890-1905), Leipzig.
D. S. Scott [ 1970 ], “Outline of a mathematical theory of computation,” Proc. Fourth Ann. Princeton Symp. on the Semantics of Algorithmic Languages (E. Engeler, ed.).
D. S. Scott [ 1970 ], “Constructive validity in mathematics,” Symposium on Automatic Demonstration, Lecture Notes in Mathematics 125, Springer-Verlag, Berlin.
D. S. Scott [ 1972 ], “Lattice theory, data types, and semantics,” NYU Symp. on Formal Semantics (R. Rustin, ed.), Prentice Hall, New York.
D. S. Scott [ 1973 ], “Models for various type-free calculi,” in Logic, Method., and Phil, of Science IV ( P. Suppes, L. Henkin, A. Joja and G. C. Moisel, eds.), North Holland, Amsterdam.
D. S. Scott [ 1976 ], “Data types as lattices,” SIAM J. on Computing, 5, 522–587.
D. S. Scott [ 1977 ], “Logic and programming languages,” Comm. ACM, 20, 634–641.
D. S. Scott [ 1980 ], “Lambda calculus: some models, some philosophy,” Kleene Symposium (J. Barwise, K. Kunen and J. Keisler, eds.), North Holland, Amsterdam, 223–265.
D. S. Scott [ 1981 ], “Lectures on a mathematical theory of computation,” Tech. Monograph PRG-19, Oxford University Programming Lab., Oxford, England.
D. S. Scott and G. Strachey [ 1971 ], “Towards a mathematical semantics for computer languages,” Proc. Symp. on Computers and Automata 21 ( J. Fox, ed.), Polytechnic Institute of Brooklyn Press, New York.
K. Segerberg [ 1982 ], A Completeness Theorem in the Modal Logic of Programs, Universal Algebra and Applications (T. Traczyk, ed.), Banach Center Publications 9, PWN-Polish Scientific Publishers, Warsaw.
J. C. Shepherdson [ 1984 ], “Negation as failure,” J. Logic Programming, 1, 51–79.
J. C. Shepherdson [ 1985 ], “Negation as failure II,” J. Logic Programming, 185–202.
M. Shönfinkel [ 1924 ], “Uber die Bausteine der Mathematischen Logik,” Math. Ann., 92, 305–316.
J. H. Siekmann [1984], “Universal unification,” Seventh Int. Conf. in Automated Deduction, Lecture Notes in Computer Science 170, 1–42.
J. H. Siekman and G. Wrightson [ 1983 ], The Automation of Reasoning: Collected Papers from 1957 to 1970 (2 vol.), Springer-Verlag, Berlin.
T. Skolem [ 1920 ], “Logisch-Kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit Mathematischer Sätze nebst einer Theoreme über Dichte Mengen,” in van Heijenoort.
J. Smith [ 1982 ], “The identification of propositions and types in Martin-Löfs type theory: a programming example,” in Foundations of Computer Science, Lecture Notes in Computer Science 158 (M. Karpinski, ed.), 445–454.
S. Stenlund [ 1972 ], Combinators, Lambda Terms and Proof-Theory, D. Reidel, Dorddrecht.
E. Stoy [ 1981 ], Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, Massachusetts.
S.-A. Tärnlund [ 1975 ], “An interpreter for the programming language predicate logic,” Proc. Fourth IJCAI, Tbilisi, Georgia, USSR, 601–608.
S.-A. Tärnlund [ 1977 ], “Horn clause computability,” BIT, 17, 215–226.
S.-A. Tärnlund [ 1978 ], “An axiomatic database theory,” in Gallaire and Minker.
S.-A. Tärnlund [ 1980 ], Proc. of the Logic Programming Workshop, Debrecen, Hungary.
A. Tarski [ 1956 ], Logic, Semantics, Metamathematics (papers from 1923 to 1936 ), J. W. Woodger, tr., Oxford, Clarendon Press.
R. D. Tennent [ 1981 ], Principles of Programming Languages, Prentice Hall, New York.
A. S. Troelstra [ 1974 ], Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics 344, Springer-Verlag, Berlin.
A. M. Turing [ 1936 ], “On computable numbers, with an application to the Entschei-dungsproblem,” Proc. Lond. Math. Soc., 42, 230–265.
M. H. van Emden [ 1977 ], “Programming in resolution logic,” in Machine Intelligence 8, 266–299.
K. H. van Emden [ 1978 ], “Computation and deductive information retrieval,” in Formal Description of Programming Concepts ( E. Neuhold, ed.), Proc. of Conf. on Theoretical Comp. Sci., University of Waterloo, Ontario, Canada.
K. H. van Emden and R. A. Kowalski [ 1976 ], “The semantics of predicate logic as a programming language,” J. ACM, 23, 733–742.
M. H. van Emden and G. J. de Lucena Filho [1982], “Predicate logic as a language for parallel programming,” in Clarke and Tärnlund [ 1982 ].
J. van Heijenoort [ 1967 ], From Frege to Gödel, Harvard University Press, Cambridge, Massachusetts.
Moshe Vardi [ 1982 ], “The complexity of relational query languages,” 14th ACM Symp. Comp. Theory, 137–146.
J. Von Neumann [1966], Theory of Self-Reproducing Automata, University of Illinois Press.
C. P. Wadsworth [ 1976a ], Semantics and Pragmatics of The Lambda Calculus, Ph.D. Thesis, University of Oxford.
C. P. Wadsworth [ 1976b ], “The relation between computational semantics and deno tational properties for Scott’s Dw models of The Lambda Calculus,” SIAM J. on Comp., 5, 488–521.
D. H. D. Warren [ 1977 ], “Implementing PROLOG—compiling predicate logic programs,” DAI Research Report 39, 40, University of Edinburgh.
D. A. Waterman [ 1985 ], A Guide to Expert Systems, Addison-Wesley, Reading, Mas-sachusetts.
L. W. Weber and N. J. Nilsson [ 1981 ], Readings in Artificial Intelligence, Morgan Kauffman, Los Altos, California.
R. Wilensky [ 1984 ], Lispcraft, Norton, New York.
L. Wos, R. Overbeek, E. Lusk and J. Boyle [ 1984 ], Automated Reasoning, Prentice Hall, Englewood Cliffs, New Jersey.
L. Wos et al. [ 1984 ], “An overview of automated reasoning,” J. of Automated Reasoning, 1, 1–48.
J. J. Zeman [1973], Modal Logic, Oxford.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1986 Springer-Verlag New York Inc
About this paper
Cite this paper
Nerode, A. (1986). Applied Logic. In: Ewing, R.E., Gross, K.I., Martin, C.F. (eds) The Merging of Disciplines: New Directions in Pure, Applied, and Computational Mathematics. Springer, New York, NY. https://doi.org/10.1007/978-1-4612-4984-9_10
Download citation
DOI: https://doi.org/10.1007/978-1-4612-4984-9_10
Publisher Name: Springer, New York, NY
Print ISBN: 978-1-4612-9385-9
Online ISBN: 978-1-4612-4984-9
eBook Packages: Springer Book Archive