Personal Reflections on the Role of Mathematical Logic in Computer Science

Kfoury, Assaf

doi:10.3233/FI-2019-1860

Artykuł - szczegóły

Tytuł artykułu

Personal Reflections on the Role of Mathematical Logic in Computer Science

Autorzy

Kfoury Assaf

Wybrane pełne teksty z tego czasopisma

https://fi.episciences.org/

Identyfikatory

DOI

10.3233/FI-2019-1860

Warianty tytułu

Języki publikacji

Abstrakty

This article traces in broad strokes the evolution of the intimate relationship between mathematical logic and computer science. The emphasis is on turning points in this relationship, i.e., moments when new directions of research were opened and new connections were established between the two fields. The article is not a comprehensive account and history of the relationship, but a personal perspective of a profoundly changed, and still changing, inter-dependence between two mainstays of the mathematical disciplines.

Słowa kluczowe

computer logic symbolic logic mathematical logic history of accounting reflections

Wydawca

IOS Press

Czasopismo

Fundamenta Informaticae

Rocznik

2019

Tom

Vol. 170, nr 1-3

Strony

207--221

Opis fizyczny

Bibliogr. 63 poz.

Twórcy

autor

Kfoury Assaf

kfoury@bu.edu

Computer Science Department, Boston University, Boston, MA 02215, USA

Bibliografia

[1] Davis M. Influences of Mathematical Logic on Computer Science. In: Herken R (ed.), The Universal Turing Machine: A Half-Century Survey, pp. 315-326. Oxford University Press 1088. ISBN-0-19-853741-7.
[2] Halpern J, Harper R, Immerman N, Kolaitis P, Vardi M, Vianu V. On the Unusual Effectiveness of Logic in Computer Science. The Bulletin of Symbolic Logic, 2001. 7(2):213-236. doi:10.2307/2687775.
[3] Davis M. Why Gödel Didn’t Have Church’s Thesis. Information and Control, 1982. 54:3-24. doi:10.1016/S0019-9958(82)91226-8.
[4] Davis M. Mathematical Logic and the Origin of Modern Computers. In: Phillips ER (ed.), Studies in the History of Mathematics, pp. 137-167. Mathematical Association of America, Washington, DC, USA, 1987. ISBN-0-88385-128-8.
[5] Davis M. The Early History of Automated Deduction. In: Robinson A, Voronkov A (eds.), Handbook of Automated Reasoning, chapter 1, pp. 4-15. Elsevier, 2001. ISBN-9780444829498.
[6] Kfoury A. Mathematical Logic in Computer Science. CoRR, 2018. abs/1802.03292. 1802. 03292, URL http://arxiv.org/abs/1802.03292.
[7] Barwise J, Keisler H, Kunen K, Moschovakis Y, Troelstra A. Handbook of Mathematical Logic. Elsevier (North Holland), 1977. ISBN-072042285X, 9780720422856.
[8] Buss SR, Kechris AS, Pillay A, Shore RA. The Prospects for Mathematical Logic in the Twenty-First Century. The Bulletin of Symbolic Logic, 2001. 7(2):169-196. doi:10.2307/2687773.
[9] Sangiorgi D. On the Origins of Bisimulation and Coinduction. ACM Trans. Program. Lang. Syst. (TOPLAS), 2009. 31(4):1-41. doi:10.1145/1516507.1516510.
[10] Sangiorgi D. Introduction to Bisimulation and Coinduction. Cambridge University Press, 2012. doi:10.1017/CBO9780511777110.
[11] Sangiorgi D, Rutten J. Advanced Topics in Bisimulation and Coinduction. Cambridge Tracts in Theoretical Computer Science, Vol. 52. Cambridge University Press, 2011. ISBN-107004977, 9781107004979.
[12] Grädel E, Kolaitis P, Libkin L, Marx M, Spencer J, Vardi M, Venema Y, Weinstein S. Finite Model Theory and Its Applications. Texts in Theoretical Computer Science. Springer, 2007. doi:10.1007/3-540-68804-8.
[13] Pierce BC. Types and Programming Languages. MIT Press, 2002. ISBN-0-262-16209-1.
[14] Gunter CA. Semantics of Programming Languages. MIT Press, 1992. ISBN-0262570955, 9780262570954.
[15] Mitchell JC. Foundations for Programming Languages. MIT Press, 1996. ISBN-10:0262133210, 13:978-0262133210.
[16] Gunter CA, Mitchell JC (eds.). Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design. MIT Press, 1994. ISBN-10:026207155X, 13:978-0262071550.
[17] Pierce BC (ed.). Advanced Topics in Types and Programming Languages. MIT Press, 2005. ISBN-10:0262162288, 13:978-0262162289.
[18] Nederpelt R, Geuvers H. Type Theory and Formal Proof - An Introduction. Cambridge University Press, 2014. ISBN-10:110703650X, 13:978-1107036505.
[19] Kroening D, Strichman O. Decision Procedures, An Algorithmic Point of View. Texts in Theoretical Computer Science. Springer, 2008. doi:10.1007/978-3-540-74105-3.
[20] Schöning U, Toran J. The Satisfiability Problem: Algorithms and Analysis. Mathematik fur Anwendungen. Lehmanns Fachbuchhandlung GmbH, 2013. ISBN-386541527X, 9783865415271.
[21] Marquis JP, Reyes GE. The History of Categorical Logic. In: Gabbay DM, Kanamori A, Woods J (eds.), Handbook of the History of Logic, volume 6, pp. 1-116. Elsevier (North Holland), 2012.
[22] Barr M, Wells C. Category Theory for Computing Science, Third Edition. Prentice-Hall Int. Series in Computer Science, 1998.
[23] Flum J, Grädel E, Wilke T (eds.). Logic and Automata: History and Perspectives. Texts in Logic and Games, Volume 2. Amsterdam University Press, 2008. ISBN 9789053565766. URL http://www.jstor.org/stable/j.ctt46mv83.
[24] Blackburn P, Benthem JFAKv, Wolter F. Handbook of Modal Logic, Volume 3 (Studies in Logic and Practical Reasoning). Elsevier Science Inc., New York, NY, USA, 2006. ISBN-0444516905.
[25] Vardi MY. Automata-Theoretic Techniques for Temporal Reasoning. In: Blackburn P, Benthem JFAKv, Wolter F (eds.), Handbook of Modal Logic, Volume 3, chapter 17, pp. 971-986. Elsevier Science Inc., 2006. doi:10.1016/S1570-2464(07)80020-6.
[26] Kozen D, Tiuryn J. Logics of Programs. In: van Leeuwen J (ed.), Handbook of Theoretical Computer Science, volume B, chapter 14, pp. 789-840. North Holland, Amsterdam, 1989.
[27] Harel D, Kozen D, Tiuryn J. Dynamic Logic. MIT Press, 2000. ISBN-0262082896.
[28] Hoare CAR. An Axiomatic Basis for Computer Programming. Commun. ACM, 1969. 12(10):576-580. doi:10.1145/363235.363259.
[29] Howard W. The Formulas-as-Types Notion of Construction. In: Seldin J, Hindley J (eds.), To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp. 479-490. Academic Press, Boston, 1980. Original version circulated privately in 1969. ISBN-978-0-12-349050-6.
[30] Sørensen MH, Urzyczyn P. Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics). Elsevier Science Inc., New York, NY, USA, 2006. ISBN-0444520775.
[31] Gonthier G, Asperti A, Avigad J, Bertot Y, Cohen C, Garillot F, Le Roux S, Mahboubi A, O’Connor R, Biha SO, Pasca I, Rideau L, Solovyev A, Tassi E, Théry L. A Machinechecked Proof of the Odd Order Theorem. In: Blazy S, Paulin-Mohring C, Pichardie D (eds.), Proceedings of the 4th International Conference on Interactive Theorem Proving, ITP’13. Springer-Verlag, Berlin, Heidelberg, 2013 pp. 163-179. ISBN 978-3-642-39633-5. doi:10.1007/978-3-642-39634-2_14.
[32] Hales T, Adams M, Bauer G, Dang TD, Harrison J, Hoang LT, Kaliszyk C, Magron V, McLaughlin S, Nguyen TT, Nguyen QT, Nipkow T, et al. A Formal Proof of the Kepler Conjecture. Forum of Mathematics, Pi, 2017. 5. doi:10.1017/fmp.2017.1.
[33] Heule MJH, Kullmann O, Marek VW. Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer. CoRR, 2016. abs/1605.00723. 1605.00723, URL http://arxiv.org/abs/1605.00723.
[34] Wells J. Typability and Type Checking in System F Are Equivalent and Undecidable. Annals of Pure and Applied Logic, 1999. 98(1):111-156. doi:https://doi.org/10.1016/S0168-0072(98)00047-5.
[35] Kfoury A, Tiuryn J, Urzyczyn P. The Undecidability of the Semi-unification Problem. Information and Computation, 1993. 102(1):83-101. doi:https://doi.org/10.1006/inco.1993.1003.
[36] Walukiewicz I. Completeness of Kozen’s Axiomatisation of the Propositional μ-Calculus. Inf. Comput., 2000. 157(1-2):142-182. doi:10.1006/inco.1999.2836.
[37] Szelepcsényi R. The Method of Forced Enumeration for Nondeterministic Automata. Acta Inf., 1988. 26(3):279-284. doi:10.1007/BF00299636.
[38] Immerman N. Nondeterministic Space is Closed Under Complementation. SIAM J. Comput., 1988. 17(5):935-938. doi:10.1137/0217058.
[39] Girard JY. Interprétation Fonctionelle et Elimination des Coupures dans l’Arithmétique d’Ordre Supérieur, 1972. Thèse dEtat, Université Paris VII.
[40] Reynolds JC. Towards a Theory of Type Structure. In: Robinet B (ed.), Programming Symposium, Lecture Notes in Computer Science, Volume 19. Springer-Verlag, 1974 pp. 408-425. ISBN-3-540-06859-7.
[41] Girard JY. The System F of Variable Types, Fifteen Years Later. Theoretical Computer Science, 1986. 45:159-192. URL https://doi.org/10.1016/0304-3975(86)90044-7.
[42] Huet G. Formal Structures for Computation and Deduction, 1986. Unpublished manuscript of lecture notes, downloadable from http://pauillac.inria.fr/huet/PUBLIC/Formal_Structures.pdf.
[43] Girard JY. Une Extension de l’Interprétation de Gödel à l’Analyse, et son Application à l’Elimination des Coupures dans l’Analyse et la Théorie des Types. Studies in Logic and the Foundations of Mathematics, 1971. 63:63-92. doi:http://dx.doi.org/10.1016/S0049-237X(08)70843-7. Proceedings of the Second Scandinavian Logic Symposium, URL http://www.sciencedirect.com/science/article/pii/S0049237X08708437.
[44] Statman R. Number Theoretic Functions Computable by Polymorphic Programs (Extended Abstract). In: 22nd Annual Symposium on Foundations of Computer Science, Nashville, Tennessee, USA, 28-30 October 1981. IEEE Computer Society, 1981 pp. 279-282. doi:10.1109/SFCS.1981.24.
[45] Friedman H. Algorithmic Procedures, Generalized Turing Algorithms, and Elementary Recursion Theory. In: Gandy R, Yates C (eds.), Logic Colloquium ’69, pp. 361-389. North-Holland, 1970. URL https://doi.org/10.1016/S0049-237X(08)71238-2.
[46] Kfoury A. Definability by Programs in First-Order Structures. Theoretical Computer Science, 1983. 25(1):1-66. doi:http://dx.doi.org/10.1016/0304-3975(83)90013-0.
[47] Paterson MS, Hewitt CE. Comparative Schematology. In: Record of the Project MAC Conference on Concurrent Systems and Parallel Computation. ACM, 1970 pp. 119-128. doi:10.1145/1344551.1344563.
[48] Kfoury A. The Pebble Game and Logics of Programs. In: Harrington L, Morley M, Simpson S, Scedrov A (eds.), Harvey Friedman’s Research on the Foundations of Mathematics, pp. 317-329. North-Holland, 1985. URL https://doi.org/10.1016/S0049-237X(09)70165-X.
[49] Hindley JR. M. H. Newman’s Typability Algorithm for Lambda-calculus. Journal of Logic and Computation, 2008. 18(2):229-238. doi:10.1093/logcom/exm001.
[50] Cardone F, Hindley JR. Lambda-Calculus and Combinators in the 20th Century. In: Gabbay D, Woods J (eds.), Handbook of the History of Logic (Logic from Russell to Church), volume 5, pp. 723-818. Elsevier (North Holland), 2009. ISBN-978-0-44-451620-6.
[51] Moses J. Macsyma: A Personal History. Journal of Symbolic Computation, 2012. 47(2):123-130. doi:http://dx.doi.org/10.1016/j.jsc.2010.08.018.
[52] Durán AJ, Pérez M, Varona JL. The Misfortunes of a Trio of Mathematicians Using Computer Algebra Systems. Can We Trust in Them? Notices of the AMS, 2014. 61(10):1249-1252. doi:http://dx.doi.org/10.1090/noti1173.
[53] Bundy A. Automated Theorem Provers: A Practical Tool for the Working Mathematician? Annals of Mathematics and Artificial Intelligence, 2011. 61(1):3-14. doi: 10.1007/s10472-011-9248-8.
[54] Clarke E, Zhao X. Analytica - A Theorem Prover for Mathematica. Technical report, Carnegie Mellon University, Pittsburgh, PA, USA, 1992.
[55] Ballarin C, Homann K, Calmet J. Theorems and Algorithms: An Interface Between Isabelle and Maple. In: Proceedings of the 1995 International Symposium on Symbolic and Algebraic Computation, ISSAC ’95. ACM, New York, NY, USA. ISBN 0-89791-699-9, 1995 pp. 150-157. doi:10.1145/220346.220366.
[56] Ballarin C, Paulson LC. Reasoning about Coding Theory: The Benefits We Get from Computer Algebra. In: Calmet J, Plaza J (eds.), Artificial Intelligence and Symbolic Computation: International Conference AISC’98, Proceedings. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-540-49816-2, 1998 pp. 55-66. doi:10.1007/BFb0055902.
[57] Buchberger B, Jebelean T, Kutsia T, Maletzky A, Windsteiger W. Theorema 2.0: Computer-Assisted Natural-Style Mathematics. Journal of Formal Reasoning, 2016. 9(1):149-185. URL http://dx.doi.org/10.6092/issn.1972-5787/4568.
[58] Adams A, Gottliebsen H, Linton SA, Martin U. Automated Theorem Proving in Support of Computer Algebra: Symbolic Definite Integration As a Case Study. In: Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation, ISSAC ’99. ACM, New York, NY, USA. ISBN 1-58113-073-2, 1999 pp. 253-260. doi:10.1145/309831.309949.
[59] Adams A, Dunstan M, Gottliebsen H, Kelsey T, Martin U, Owre S. Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS. In: Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, TPHOLs ’01. Springer-Verlag, London, UK, UK. 2001 pp. 27-42. ISBN-3-540-42525-X. URL http://dl.acm.org/citation.cfm?id=646528.695189.
[60] Horgan J. The Death of Proof. Scientific American, 1993. 269:93-103. doi:10.1038/scientificamerican1093-92.
[61] Grothendieck A. Récoltes et Semailles, 1986. Unpublished manuscript, downloadable from various sites on the Web, Grothendieck’s non-mathematical writings, Récoltes et Semailles, among others.
[62] Edwards DA. Response to Quinn. Notices of the AMS, 2012. 59(3):366. This is a letter in response to an earlier article: A Revolution in Mathematics? What Really Happened a Century Ago and Why It Matters Today [63].
[63] Quinn F. A Revolution in Mathematics? What Really Happened a Century Ago and Why It Matters Today. Notices of the AMS, 2012. 59(1):31-37. doi:10.1090/noti787.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).

Typ dokumentu

Bibliografia

Identyfikator YADDA

bwmeta1.element.baztech-6563a364-7074-4125-9720-47761ce9d2b4