×

In praise of impredicativity: a contribution to the formalization of meta-programming. (English) Zbl 1434.68102

Summary: Processing programs as data is one of the successes of functional and logic programming. Higher-order functions, as program-processing programs are called in functional programming, and meta-programs, as they are called in logic programming, are widespread declarative programming techniques. In logic programming, there is a gap between the meta-programming practice and its theory: The formalizations of meta-programming do not explicitly address its impredicativity and are not fully adequate. This article aims at overcoming this unsatisfactory situation by discussing the relevance of impredicativity to meta-programming, by revisiting former formalizations of meta-programming, and by defining Reflective Predicate Logic, a conservative extension of first-order logic, which provides a simple formalization of meta-programming.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science

Software:

Twelf; ML; Automath; HiLog
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Aczel, P.1977. An introduction to inductive definitions. In Handbook of Mathematical Logic, Barwise, Jon, Ed. North-Holland, 739-782.
[2] Aiello, L. C., Cecchi, C. and Sartini, D.1986. Representation and use of meta-knowledge. Proceedings of the IEEE74, 10, 1304-1321.
[3] Apt, K. R. and Ben-Eliyahu, R.1996. Meta-variables in logic programming, or in praise of ambivalent syntax. Fundamenta Informaticae28, 1, 23-36. · Zbl 0865.68024
[4] Apt, K. R. and van Emden, M.1982. Contributions to the theory of logic programming. Journal of the Association for Computating Machinery29, 841-862. · Zbl 0483.68004
[5] Backus, J. W.1959. The syntax and semantics of the proposed international algebraic language of Zürich ACM-GAMM conference. In Proc. of the International Conference on Information Processing, Jun. 1959, Veronese, V., Ed. Paris, France, UNESCO (Paris, France), R. Oldenbourg (München, Germany) and Butterworths (London, Great Britain), 125-132. · Zbl 0112.08301
[6] Barendregt, H.1993. Lambda Calculi with types. In Handbook of Logic in Computer Science. Vol. 2, Background: Computational Structures. Oxford University Press, 117-309.
[7] Barklund, J.1989. What is a meta-variable in Prolog? In Meta-Programming in Logic Programming, Abramson, Harvey and Rogers, M. H., Eds. MIT Press, 383-398.
[8] Barklund, J.1995. Metaprogramming in logic. Encyclopedia of Computer Science and Technology33, 205-227. Supplement 18: Case-Based Reasoning to User Interface Software Tools.
[9] Barklund, J., Costantini, S., Dell’Acqua, P. and Lanzarone, G. A.1994. SLD-resolution with reflection. In Logic Programming, Proceedings of the 1994 International Symposium, Bruynooghe, M., Ed. Melbourne, Australia, 554-568.
[10] Barklund, J., Costantini, S., Dell’Acqua, P. and Lanzarone, G. A.1995a. Semantical properties of encodings in logic programming. In Logic Programming - The 1995 International Symposium, Lloyd, J. W., Ed. MIT Press, Portland, Oregon, USA, 288-302.
[11] Barklund, J., Dell’Acqua, P., Costantini, S. and Lanzarone, G. A.1995b. Semantical properties of SLD-resolution with reflection. In Logic Programming, Proceedings of the Twelfth International Conference on Logic Programming, Sterling, L., Ed. MIT Press, Tokyo, Japan, 830. · Zbl 0964.03032
[12] Barklund, J., Dell’Acqua, P., Costantini, S. and Lanzarone, G. A.2000. Reflection principles in computational logic. Journal of Logic and Computation10, 743-786. · Zbl 0964.03032
[13] Benjamin, P.1990. A meta level manifesto. In Machine Learning, Meta-reasoning and Logics, Brazdil, P. B. and Konolige, K., Eds. Kluwer Academic Publishers, 3-17.
[14] Bezem, M.1999. Extensionality of simply typed logic programs. In Proc. of the 16th International Conference on Logic Programming (ICLP), de, D.Schreye, Ed. MIT Press, 395-410.
[15] Bezem, M.2001. An improved extensionality criterion for higher-order logic programs. In Computer Science Logic, 15th International Workshop, CSL. Vol. 2142, LNCS. Fribourg, L., Ed. Springer-Verlag, Paris, France, 203-216. · Zbl 0999.68035
[16] Böhm, C. and Jacopini, G.1966. Flow diagrams, Turing machines and languages with only two formation rules. Communications of the ACM, 9, 5, 366-371. · Zbl 0145.24204
[17] Boole, G.1854. An Investigation of the Laws of Thought on Which are Founded the Mathematical Theories of Logic and Probabilities. Macmillan. Reprinted by Dover Publications, New York, 1958, and by Cambridge University Press, 2009. · Zbl 1205.03003
[18] Bowen, K. and Kowalski, R.1982. Amalgamating language and metalanguage in logic programming. In Logic Programming, Clark, K. and Tärnlund, S. A., Eds. Academic Press, 153-173.
[19] Bowen, K. A.1985. Meta-level programming and knowledge representation. New Generation Computing3, 359-383.
[20] Bowen, K. A. and Weinberg, T.1985. A meta-level extension of Prolog. In Proc. of the IEEE Symposium on Logic Programming, Cohen, J. and Conery, J., Eds. IEEE, Boston, Massachusetts, USA, 669-675.
[21] Burgess, J. P.2005. Fixing Frege. Princeton University Press, Princeton, NJ, USA. · Zbl 1089.03001
[22] Cardelli, L.2004. Type systems. In CRC Handbook of Computer Science and Engineering, Tucker, A. B., Ed. CRC Press, 2208-2236.
[23] Cardelli, L. and Wegner, P.1985. On understanding types, data abstraction, and polymorphism. ACM Computing Surveys17, 4 (December), 471-522.
[24] Cervesato, I. and Rossi, G.1992. Logic meta-programming facilities in ‘LOG. Research Showcase @ CMU 6-1992, Carnegie Mellon University, School of Computer Science, Computer Science Department.
[25] Chang, C.-L. and Lee, R. C.-T.1997. Symbolic Logic and Mechanical Theorem Proving. Academic Press.
[26] Charalambidis, A., Handjopoulos, K., Rondogiannis, P. and Wadge, william L.. 2013. Extensional higher-order logic programming. ACM Transactions on Computational Logic14, 3, 91-103. · Zbl 1306.68004
[27] Chen, W.1987. A theory of modules based on second-order logic. In Proc. IEEE Symposium on Logic Programming, IEEE Computer Society, San Francisco, California, USA, 24-33.
[28] Chen, W., Kifer, M. and Warren, D. S.1993. HiLog: A foundation for higher-order logic programming. Journal of Logic Programming 15, 3, 187-230. · Zbl 0787.68017
[29] Church, A.1932. A set of postulates for the foundation of logic. Annals of Mathematics - Series233, 2, 346-366. · JFM 58.0997.06
[30] Church, A.1940. A formulation of the simple theory of types. Journal of Symbolic Logic5, 56-68. · JFM 66.1192.06
[31] Chwistek, L.1921. Antynomje logikiformalnej. Przeglad Filozoficzny24, 164-171. In Polish, English translation: Chwistek (1967).
[32] Chwistek, L.1967. Antinomies of formal logic. In Polish Logic: 1920-1939, McCall, S., Ed. Clarendon Press, 338-345. English translation by Z. Jordan of Chwistek (1921).
[33] Clocksin, W. F. and Mellish, C. S.1981. Programming in Prolog. Springer-Verlag. · Zbl 0466.68009
[34] Costantini, S.2002. Meta-Reasoning: A survey. In Computational Logic: Logic Programming and Beyond (Festschrift in honour of Robert Kowalski), Kakas, A. C. and Sadri, F., Eds. Vol. 2408, LNCS. Springer-Verlag, 254-288. · Zbl 1012.68190
[35] Costantini, S. and Lanzarone, G. A.1989. A metalogic programming language. In Proc. of the International Conference on Logic Programming, Jun. 1989, Levi, G. and Martelli, M., Ed. Lisbon, Portugal, 218-233.
[36] Costantini, S. and Lanzarone, G. A.1994. A metalogic programming approach: Language, semantics and applications. Journal of Experimental & Theoretical Artificial Intelligence6, 3, 239-287. · Zbl 0820.68030
[37] Damas, L.1985. Type Assignment in Programming Languages. Ph.D. thesis, Report No. CST-33-85, University of Edinburgh.
[38] Damas, L. and Milner, R.1982. Principal type-schemes for functional programs. In Proc. of the 9th Symposium on Principles of Programming Languages (POPL), DeMillo, R., Ed. ACM, Albuquerque, New Mexico, USA, 207-212.
[39] De Schreye, D. and Martens, B.1992. A sensible least Herbrand semantics for untyped vanilla meta-programming and its extension to a limited form of amalgamation. In Meta-Programming in Logic, Proc. of the 3rd International Workshop on Meta-Programming (META), Jun. 1992, Peterossi, A., Ed. LNCS. Springer-Verlag, Uppsala, Sweden, 192-204.
[40] Dijkstra, E. W.1968. Letters to the editor: Go to statement considered harmful. Communications of the ACM11, 3, 147-148.
[41] Eshghi, K.1986. Meta-language in Logic Programming. Ph.D. thesis, Department of Computing, Imperial College of Science and Technnology, University of London, UK.
[42] Feferman, S.2005. Predicativity. In The Oxford Handbook of Philosophy of Mathematics and Logic, Shapiro, S., Ed. Oxford University Press, 590-624.
[43] Frege, G.1879. Begriffsschrift - Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Verlag von Louis Nebert, Halle an der Saale. In German, English translation: Frege (1967, 2002).
[44] Frege, G.1893. Grundgesetze der Arithmetik, Band I. Verlag Herman Pohle, Jena. In German, partial English translation: Frege (1964). · JFM 25.0101.02
[45] Frege, G.1903. Grundgesetze der Arithmetik, Band II. Verlag Herman Pohle, Jena. In German, partial English translation: Frege (1964). · JFM 34.0071.05
[46] Frege, G.1964. The Basic Laws of Arithmetic. University of California Press, Berkeley, CA, USA. Partial English translation of Frege (1893, 1903) by Montgomery Furth.
[47] Frege, G.1967, 2002. A concept notation: A formula language of pure thought, modelled upon that of arithmetic. In From Frege to Gödel: A Sourcebook in Mathematical Logic, 1879-1931, van Heijenoort, J., Ed. Harvard University Press, 1-82, English translation of Frege (1879).
[48] Gelfond, M. and Lifschitz, V.1988. The stable model semantics for logic programming. In Proc. of the Fifth International Conference on Logic Programming (ICLP), Aug. 1988, Bowen, K. A. and Kowalski, R. A., Eds. MIT Press, Seattle, Washington, 1070-1080.
[49] Gentzen, G.1934. Untersuchungen über das logische Schließen I. Mathematische Zeitschrift39, 2, 176-210. In German. English translations: Gentzen (1964), Gentzen (1969). · Zbl 0010.14501
[50] Gentzen, G.1964. Investigations into logical deduction. American Philosophical Quarterly1, 4 (October), 288-306. English translation of Gentzen (1934).
[51] Gentzen, G.1969. Investigations into logical deduction. In The Collected Works of Gerhard Gentzen, Szabo, M. E., Ed. Studies in logic and the foundations of mathematics. North-Holland, 68-131. English translation of Gentzen (1934).
[52] Giordano, L., Martelli, A. and Rossi, G.1994. Structured Prolog: A language for structured logic programming. Software-Concepts and Tools15, 125-145.
[53] Giordano, L. and Olivetti, N.1994. Combining negation as failure and embedded implications in logic programs. Journal of Logic Programming19, 20, 1-679. · Zbl 0911.68027
[54] Gödel, K.1930. Über die Vollständigkeit des Logikkalküls. Doctoral thesis, University of Vienna, Austria. In German, English translation: Gödel (2002). · JFM 56.0046.04
[55] Gödel, K.1931. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatsheft für Mathematik und Physik38, 173-198. In German, English translation: Gödel (1986). · JFM 57.0054.02
[56] Gödel, K.1944. Russell’s mathematical logic. In The Philosophy of Bertrand Russell, Schilpp, P. A., Ed. Northwestern University, Chicago, IL, USA, 123-153.
[57] Gödel, K.1967, 2002. The completeness of the Axioms of the functional calculus of logic. In From Frege to Gödel: A Sourcebook in Mathematical Logic, 1879-1931. van Heijenoort, J., Ed. Harvard University Press, 582-591.
[58] Gödel, K.1986. On Formally Undecidable Propositions of Principia Mathematica and Related Systems I. Vol. I Publications 1929-1936. Oxford University Press. English translation of Gödel (1930).
[59] Graf, P.1996. Term Indexing. Vol. 1053, LNCS. Springer-Verlag. Doctoral thesis, Saarland University, Germany, 1995. · Zbl 0970.68152
[60] Haemmerlé, R. and Fages, F.2006. Modules for Prolog revisited. In Logic Programming - International Conference on Logic Programming (ICLP), Etalle, S. and Truszczynski, M., Ed. Springer-Verlag, Seattle, Washington, USA. 41-55. · Zbl 1131.68378
[61] Halpern, J. Y. and Moses, Y.1985. A guide to the modal logics of knowledge and belief. In Proc. 9th International Joint Conference on Artificial Intelligence (IJCAI), Joshi, A., Ed. Vol. 1, Morgan Kaufmann, Los Angeles, California, USA, 480-490.
[62] Harper, R., Honsell, F. and Plotkin, G.1993. A framework for defining logics. Journal of the ACM (JACM)40, 1, 143-184. · Zbl 0778.03004
[63] Higgins, C. P.1996. On the declarative and procedural semantics of definite metalogic programs. Journal of Logic and Computation6, 3, 363-407. · Zbl 0851.68011
[64] Hill, P. and Lloyd, J. W.1994. The Gödel Programming Language. MIT Press. · Zbl 0850.68138
[65] Hill, P. M. and Lloyd, J. W.1988. Analysis of meta-programs. In Meta-Programming in Logic Programming, Workshop on Meta-Programming in Logic (META-88), Jun. 1988, Abramson, H. and Rogers, M. H., Eds. MIT Press, Bristol, Great Britain, 23-51.
[66] Hindley, R. J.1969. The principal type-scheme of an object in combinatory logic. Transactions of the American Mathematical Society 146, Bristol, Great Britain, 29-60. · Zbl 0196.01501
[67] Hintikka, J.1964. Knowledge and Belief - An Introduction to the Logic of the Two Notions, 2nd ed. Cornell University Press.
[68] Huet, G. P.1976. Résolution d’équations dans des langages d’ordre 1, 2, …, ω. Doctoral thesis, Mathématiques, Université Paris VII.
[69] Jiang, Y.1994. Ambivalent Logic as the semantic basis of logic programming. In Proc. International Conference on Logic Programming, Hentenryck, P. V., Ed. MIT Press, Santa Marherita Ligure, Italy, 387-401.
[70] Kalsbeek, M. B.1993. The Vanilla Metainterpreter for Definite Logic Programs and Ambivalent Syntax. Tech. Rep. CT 93-01, Institute for Logic Language and Computation, University of Amsterdam.
[71] Kalsbeek, M. B. and Jiang, Y.1995. A vademecum of ambivalent logic. In Meta-Logics and Logic Programming, Apt, K. R. and Turini, F., Ed. MIT Press, 27-56.
[72] Kowalski, R.1973. Predicate logic as a programming language. Memo 70, Department of Artificial Intelligence, Edinburgh University. Also in: Proc. IFIP Congress, Stockholm, North Holland, 1974, 569-574. · Zbl 0297.68006
[73] Kowalski, R.1979. Logic For Problem Solving. North Holland. · Zbl 0426.68002
[74] Kowalski, R. and Kim, J.-S.1991. A metalogic approach to multi-agent knowledge and belief. In Artificial and Mathematical Theory of Computation: Papers in Honor of John McCarthy, Lipschitz, V., Ed. Academic Press, 231-246. · Zbl 0755.68122
[75] Levi, G. and Ramundo, D.1993. A formalization of meta-programming for real. In Proc. of the 10th International Conference on Logic Programming, Jun. 1993, Warren, D. S., Ed. MIT Press, Budapest, Hungary, 354-373.
[76] Levy, J. and Veanes, M.2000. On the undecidability of second-order unification. Information and Computation159, 1-2, 125-150. · Zbl 1005.03007
[77] Link, G., Ed. 2004. One Hundred Years of Russell’s Paradox: Mathematics, Logic, Philosophy. de Gruyter. · Zbl 1050.03003
[78] Liskov, B. and Zilles, S.1974. Programming with abstract data types. ACM SIGPLAN Notices9, 4, 50-59. · Zbl 07526287
[79] Lismont, L. and Mongin, P.1994. On the logic of common belief and common knowledge. Theory and Decision37, 75-106. · Zbl 0831.03014
[80] Lloyd, J. W.1987. Foundation of Logic Programming, 2nd ed. Springer-Verlag. · Zbl 0668.68004
[81] Martelli, A. and Rossi, G.1988. Enhancing Prolog to support Prolog programming environments. In ESOP’88: 2nd European Symposium on Programming, Mar. 1988, Vol. 300, LNCS. Ganzinger, H., Ed. Springer-Verlag, Nancy, France, 317-327.
[82] McCarthy, J. and Levin, M. I.1965. Lisp 1.5 Programmer’s Manual. Tech. Rep., Computation Center, Massachusetts Institute of Technology, USA.
[83] McCarthy, J., Sato, M., Hayashi, T. and Igrashi, S.1978. On the Model Theory of Knowledge. Tech. Rep., AIM-312, Stanford University.
[84] Miller, D.1989. A logical analysis of modules in logic programming. Journal of Logic Programming6, 1-2, 79-108. · Zbl 0681.68022
[85] Miller, D. and Nadathur, G.1988. An overview of Lambda-Prolog. In Proc. Fifth International Conference and Symposium on Logic Programming, Kowalski, R. A. and Bowen, K. A., Eds. MIT Press, Seattle, Washington, USA, 810-827.
[86] Miller, D. and Nadathur, G.2012. Programming with Higher-Order Logic. Cambridge University Press. · Zbl 1267.68014
[87] Milner, R.1978. A theory of type polymorphism in programming. Journal of Computer and System Science17, 348-374. · Zbl 0388.68003
[88] Moschovakis, J.1999, 2015. Intuitionistic Logic. The Metaphysics Research Lab, Center for the Study of Language and Information, Stanford University, Stanford, CA 94305-4115. https://plato.stanford.edu/entries/logic-intuitionistic/.
[89] O’Keefe, R.1990. The Craft of Prolog. MIT Press.
[90] Perlis, A. J. and Samelson, K.1958. Preliminary report: International algebraic language. Communications of the ACM1, 12, 8-22. · Zbl 0084.12401
[91] Perlis, D.1985. Languages with self-reference i: Foundations. Artificial Intelligence25, 3, 307-322. · Zbl 0581.03005
[92] Perlis, D.1988a. Languages with self-reference ii: Knowledge, belief, and modality. Artificial Intelligence34, 2, 179-212. · Zbl 0642.03017
[93] Perlis, D.1988b. Meta in logic. In Meta-level Architectures and Reflection, Maes, P. and Nardi, D., Ed. North-Holland, 37-49. · Zbl 0658.03037
[94] Pfenning, F.1991. Logic Programming in the LF Logical Framework. Research Rep., School of Computer Science, Carnegie Mellon University. · Zbl 0760.68014
[95] Pfenning, F. and Schürmann, C.1999. System description: Twelf - A meta-logical framework for deductive systems. In Proc. of the 16th International Conference on Automated Deduction (CADE). Vol. 1632, LNAI. Ganzinger, H., Ed. Springer-Verlag, Trento, Italy, 202-206.
[96] Pierce, B. C.2002. Types and Programming Languages. MIT Press. · Zbl 0995.68018
[97] Ramsey, F. P.1926. The foundations of mathematics. Proceedings of the London Mathematical Society, Series225, 338-384. · JFM 52.0046.01
[98] Robinson, A. and Voronkov, A., Eds. 2001. Handbook of Automated Reasoning. Vol. 1. ScienceDirect. · Zbl 0964.00020
[99] Robinson, G. and Wos, L.1968. Completeness of paramodulation. In Proc. of the Spring 1968 Meeting of the Association for Symbolic Logic, Journal of Symbolic Logic, Vol. 34, (1969), 102-103.
[100] Robinson, G. and Wos, L.1969. Paramodulation and theorem proving in first order theories with equality. In Machine Intelligence 4. Edinburgh University Press, 135-150. Proc. of the Fourth Annual Machine Intelligence Workshop. Edinburgh, 1968. Reprinted in Siekmann and Wrightson (1983, pp. 98-3134). · Zbl 0219.68047
[101] Rossi, G.1989. Meta-programming facilities in an extended Prolog. In Proc. of the Fifth International Conference on Artificial Intelligence and Information-Control Systems of Robots - 89, Plander, I., Ed. World Scientific, distributed by North Holland, Štrbské Pleso, Czechoslovakia
[102] Rossi, G.1992. Programs as data in an extended Prolog. The Computer Journal36, 3, 217-226.
[103] Russell, B.1907. On some difficulties in the theory of transfinite numbers and order types. Proceedings of the London Mathematical Societys2-4, 1, 29-53. · JFM 37.0074.01
[104] Russell, B.1908. Mathematical logic as based on the theory of types. American Journal of Mathematics30, 222-262. · JFM 39.0085.03
[105] Russell, B.1986. The Collected Papers of Bertrand Russell. Vol. 6, Logical and Philosophical Papers 1909-13. George Allen & Unwin. · Zbl 1066.01522
[106] Siekmann, J. H. and Wrightson, G., Eds. 1983. Automation of Reasoning. Symbolic Computation (Artificial Intelligence). Vol. 1, Classical Papers on Computational Logic 1957-1966. Springer-Verlag. · Zbl 0567.03001
[107] Siklóssy, L.1976. Let’s Talk Lisp. Prentice-Hall.
[108] Sterling, L. S. and Shapiro, E. Y.1994. The Art of Prolog, 2nd ed. MIT Press. · Zbl 0850.68137
[109] Sugano, H.1989. Reflective Computation in Logic Language and Its Semantics. Tech. Rep., International Institute for Advanced Study of Social and Information Science, Fujitsu Limited.
[110] Sugano, H.1990. Meta and reflective computation in logic programming and its semantics. In Proc. of the 2nd Workshop on Meta-Programming in Logic Programming (META), Bruynooghe, M., Ed. Springer-Verlag, Leuven, Belgium, 19-34.
[111] Tarski, A.1935. Der Wahrheitsbegriff in den formalisierten Sprachen. Studia Philosophica: commentarii Societatis Philosophicae Polonorum146, 261-405. In German, English translation: Tarski (1935). · Zbl 0013.28903
[112] Tarski, A.1935. The concept of truth in formalized languages. In Logic, Semantics, Metamathematics, Papers from 1923 to 1938, 2nd ed. Corcoran, J., Eds. Hackett Publishing Company, Inc., 152-278. · Zbl 0013.28903
[113] Trump, D.2017. “Why would Kim Jong-un insult me by calling me ‘old’, when I would NEVER call him ‘short and fat’? Oh well, I try so hard to be his friend - And maybe someday that will happen!”. Twitter Web Client https://twitter.com/realdonaldtrump/status/929511061954297857.
[114] van Ditmarsch, H., Halpern, J. Y., van der Hoek, W. and Kooi, B., Eds. 2015. Handbook of Epistemic Logic. College Publications. · Zbl 1392.03009
[115] van Emden, M. and Kowalski, R.1976. The semantics of predicate logic as a programming language. Journal of the Association for Computating Machinery23, 733-742. · Zbl 0339.68004
[116] van Harmelen, F.1989. A classification of metalevel architectures. In Logic-based Knowledge Representation, Jackson, P. M., Reichgelt, J., and van Harmelen, F., Eds. MIT Press, 1-35. · Zbl 0669.68057
[117] van Harmelen, F.1992. Definable naming relations in meta-level systems. In Proc. of the Third Workshop on Meta-Programming in Logic (META), Uppsala, Sweden, Vol. 649, LNCS, Pettorossi, A., Ed. Springer-Verlag, 89-104.
[118] von Kutschera, F.1989. Gottlob Frege: Eine Einführung in sein Werk, de Gruyter, Berlin. In German. · Zbl 0686.03002
[119] Wadge, W. W. 1991. Higher-order horn-logic programming. In Logic Programming: Proceedings of the 1991 International Symposium, Saraswat, V. A. and Ueda, K., Eds. MIT Press, 289-303.
[120] Weyhrauch, R. W.1980. Prolegomena to a theory of mechanized formal reasoning. Artificial Intelligence13, 1-2, 133-170. · Zbl 0435.68070
[121] Whitehead, A. N. and Russell, B.1910, 1912, 1913. Principia Mathematica. Vols. 1-3. Cambridge University Press. · JFM 41.0083.02
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.