Computing and Software 701
Logic and Discrete Mathematics In Software Engineering
Fall 2002

Instructor: William M. Farmer

References

01 The Nature of Mathematics

  1. D. M. Bressoud, Proofs and Confirmations: The Story of the Alternating-Sign Matrix Conjecture, Cambridge University Press, 1999.
  2. I. Lakatos, Proofs and Refutations, Cambridge University Press, 1976.
  3. Biographical Sketch of I. Lakatos.

02 Mathematical Models

  1. D. Dummit, R. Foote, and B. Holland, Abstract Algebra, Second Edition, Wiley, 1999.
  2. P. R. Halmos, Abstract Naive Set Theory, Springer-Verlag, 1987.
  3. J. Hopcraft, R. Motwani, and J. Ullman, Introduction to Automata Theory, Languages, and Computation, Second Edition, Addison Wesley, 2001.
  4. E. Mendelson, Schaum's Outline of Boolean Algebra and Switching Circuits, McGraw-Hill, 1970.

03 Review of Logic

  1. C. C. Chang and H. J. Keisler, Model Theory, North Holland, 1990.
  2. H. B. Enderton, A Mathematical Introduction to Logic, Academic Press, 1972.

04 Simple Type Theory

  1. P. B. Andrews, "An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof", Academic Press, 1986.
  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", Technical Report, 12 pp., McMaster University, 2001. PostScript PDF

05 Partial Functions and Undefined Terms

  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. PostScript PDF

06 Equational Logic and Algebraic Reasoning

  1. V. Sperschneider and G. Antoniou, Logic: A Foundation for Computer Science , Addison Wesley, 1991.

07 Recursive Definition and Inductive Proof

  1. W. M. Farmer, "A scheme for defining partial higher-order functions by recursion", In: A. Butterfield, ed., 3rd Irish Workshop on Formal Methods, 13 pp., electronic Workshops in Computing, Springer-Verlag, 1999. PostScript PDF

08 Practical Application of the Axiomatic Method

  1. J. Barwise and J. Seligman, Information Flow : The Logic of Distributed Systems, Cambridge University Press, 1997.
  2. N. Bourbaki, Eléments de mathématique, mid 1900s.
  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. Euclid, The Elements, 300 BC.
  5. 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. PostScript PDF
  6. 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. PostScript PDF
  7. R. Nakajima and T. Yuasa (eds.), The IOTA Programming System, LNCS, Vol. 160, 1982.
  8. Noneuclidean Geometry.
  9. D. Sannella and A. Tarlecki, "Towards formal development of programs from algebraic specifications: Implementations revisited", Acta Informatica, 25:233-281, 1988.
  10. D. Smith and M. Lowry, "Algorithmic theories and design tactics", Science of Computer Programming, 14:305-321, 1990
  11. W. Turski and T. Maibaum, The Specification of Computer Programs, Addison-Wesley, 1987.
  12. A. N. Whitehead and B. Russell, Principia Mathematica, Cambridge University Press, 1910-1913.

Computer Theorem Proving Systems

  1. ACL2 (A Computational Logic for Applicative Common Lisp).
  2. Alfa proof editor.
  3. Coq proof assistant.
  4. Ergo interactive proof tool.
  5. EVES tool.
  6. HOL (Higher Order Logic) theorem prover.
  7. IMPS Interactive Mathematical Proof System.
  8. INKA inductive theorem prover.
  9. Isabelle generic theorem prover.
  10. Jape (Just Another Proof Editor).
  11. LEGO proof assistant.
  12. LP (Larch Prover).
  13. Metamath Proof Explorer.
  14. Mizar tool.
  15. Nqthm (Boyer-Moore prover).
  16. Nuprl tool.
  17. Omega theorem proving system.
  18. Otter automated deduction system tool.
  19. PhoX proof assistant.
  20. PVS specification and verification system.
  21. RRL Rewrite Rule Laboratory.
  22. Theorema theorem prover.
  23. TPS Theorem Proving System.

Computer Algebra Systems

  1. Maple.
  2. Mathematica.

Miscellaneous References

  1. Formal Methods.
  2. The Mathematics Section of the Wikipedia