Computing and Software 760
Logic for Practical Use
Winter 2010

Instructor: William M. Farmer

References

01 Review of Logic

  1. I. Lakatos, Proofs and Refutations, Cambridge University Press, 1976.
  2. Biographical Sketch of I. Lakatos.
  3. R. Burstall and J. Goguen, "Putting theories together to make specifications", Proceedings of the Fifth International Joint Conference on Artificial Intelligence, pp. 1045–1058, 1977.
  4. W. M. Farmer, "Theory interpretation in simple type theory", in: J. Heering et al., eds., Higher-Order Algebra, Logic, and Term Rewriting, LNCS, 816:96–123, 1994. PDF
  5. W. M. Farmer, J. D. Guttman, and F. J. Thayer, "Little theories", in: D. Kapur, ed., Automated Deduction--CADE-11, LNCS, 607:567–581, 1992. PDF
  6. J. Xu, Mei — A Module System for Mechanized Mathematics Systems, Ph.D. Thesis, McMaster University, 2008 PDF

02 Three Traditional Logics

  1. P. B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Kluwer, 2002.
  2. A. Church, "A formulation of the simple theory of types", Journal of Symbolic Logic, 5:56–68, 1940.
  3. W. M. Farmer, "A basic extended simple type theory", SQRL Report No. 14, 12 pp., McMaster University, 2003 (revised 2004). PDF
  4. W. M. Farmer, "The seven virtues of simple type theory", Journal of Applied Logic, 6:267–286, 2008. PDF
  5. R. M. Smullyan, First-Order Logic, Dover, 1995.

03 Techniques for Enhancing Traditional Logics

  1. W. M. Farmer, "Logics with Undefinedness: How to Modify a Traditional Logic so that It handles Undefinedness in Accordance with Mathematical Practice", a half-day tutorial at the 22nd International Conference on Automated Deduction (CADE-22), McGill University, Montreal, Quebec, Canada, August 2–7, 2009. PDF

04 Practice-Oriented Logics

  1. W. M. Farmer, "A partial functions version of Church's simple theory of types", Journal of Symbolic Logic, 55:1269–1291, 1990.
  2. W. M. Farmer, "Reasoning about partial functions with the aid of a computer", Erkenntnis, 43:279–294, 1995.
  3. W. M. Farmer and J. D. Guttman, "A set theory with support for partial functions, Studia Logica, 66:59–78, 2000. PDF
  4. W. M. Farmer, "STMM: A Set Theory for Mechanized Mathematics", Journal of Automated Reasoning, 26:269–289, 2001. PDF
  5. W. M. Farmer, "Formalizing undefinedness arising in calculus", in: D. Basin and M. Rusinowitch, eds., Automated Reasoning, LNCS, 3097:475–489, 2004. PDF
  6. W. M. Farmer, "Chiron: A multi-paradigm logic", in: R. Matuszewski and A. Zalewska, eds, From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar and Rhetoric, 10(23):1–19, 2007. PDF