William M. Farmer

Professor
Department of Computing and Software
McMaster University


Publications (and some selected technical reports and tutorials)

A. MathScheme Project

  1. Formalizing mathematical knowledge as a biform theory graph: A case study Abstract PDF
    J. Carette and W. M. Farmer
    In: H. Geuvers et al., eds., Intelligent Computer Mathematics, Lecture Notes in Computer Science (LNCS), 10383:9–24, 2017 (without appendices).
    Preprint with appendices: arXiv:1704.02253 (43 pp.), 2017.
  2. Meaning formulas for syntax-based mathematical algorithms PDF
    W. M. Farmer
    In: T. Kutsia and A. Voronkov, eds., SCSS 2014 (6th International Symposium on Symbolic Computation in Software Science), EasyChair Proceedings in Computing (EPiC), 30:10–11, 2014.
    Extended Abstract.
  3. Mechanising mathematics PDF
    In: International Innovation North America, May 2013, pp. 20–22, Research Media, 2013.
  4. The formalization of syntax-based mathematical algorithms using quotation and evaluation Abstract PDF
    W. M. Farmer
    In: J. Carette et al., eds., Intelligent Computer Mathematics, Lecture Notes in Computer Science (LNCS), 7961:35–50, 2013.
    Preprint: arXiv:1305.6052, 2013.
  5. Frameworks for reasoning about syntax that utilize quotation and evaluation Abstract PDF
    W. M. Farmer and P. Larjani
    McSCert Report 9, 38 pp., McMaster University, 2013 (revised 2014).
    Preprint: arXiv:1308.2149, 2013 (revised 2014).
  6. MathScheme: Project description Abstract PDF
    J. Carette, W. M. Farmer, and R. O'Connor
    In: J. H. Davenport, W. M. Farmer, F. Rabe, and J. Urban, eds., Intelligent Computer Mathematics, Lecture Notes in Computer Science (LNCS), 6824:287–288, 2011.
  7. The MathScheme library: Some preliminary experiments Abstract PDF
    J. Carette, W. M. Farmer, F. Jeremic, V. Maccio, R. O'Connor, and Q. M. Tran
    In: A. Asperti, J. H. Davenport, W. M. Farmer, F. Rabe, and J. Urban, eds., Conference on Intelligent Computer Mathematics Work-in-Progress Papers Proceedings, Technical Report UBLCS-2011-04, pp. 10–22, University of Bologna, 2011.
    Preprint: arXiv:1106.1862, 2011.
  8. High-level theories Abstract PDF Online
    J. Carette and W. M. Farmer
    In: S. Autexier, J. Campbell, J. Rubio, V. Sorge, M. Suzuki, and F. Wiedijk, eds., Intelligent Computer Mathematics, Lecture Notes in Computer Science (LNCS), 5144:232–245, 2008.
  9. Biform theories in Chiron Abstract PDF Online
    W. M. Farmer
    In: M. Kauers, M. Kerber, R. R. Miner, and W. Windsteiger, eds., Towards Mechanized Mathematical Assistants, Lecture Notes in Computer Science (LNCS), 4573:66–79, 2007.
  10. A rational reconstruction of a system for experimental mathematics Abstract PDF Online
    J. Carette, W. M. Farmer, and V. Sorge
    In: M. Kauers, M. Kerber, R. R. Miner, and W. Windsteiger, eds., Towards Mechanized Mathematical Assistants, Lecture Notes in Computer Science (LNCS), 4573:13–26, 2007.
  11. A rational reconstruction of a system for experimental mathematics
    J. Carette, W. M. Farmer, and V. Sorge
    In: S. Colton, ed., Proceedings of the Fourteenth Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice, Imperial College, London, UK, April 19–20, 2007.
    Abstract.
  12. Trustable communication between mathematics systems Abstract PDF
    J. Carette, W. M. Farmer, and J. Wajs
    SQRL Report No. 41, 22 pp., McMaster University, 2004.
    This is a longer, revised version of the paper below with the same name.
  13. Trustable communication between mathematics systems Abstract PDF
    J. Carette, W. M. Farmer, and J. Wajs
    In: T. Hardin and R. Rioboo, eds., Calculemus 2003 (11th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Rome, Italy, September 2003), pp. 58–68, Aracne, Rome, Italy, 2003.
    This is a shorter, preliminary version of the paper above with the same name.
  14. An overview of a Formal Framework for Managing Mathematics Abstract PDF
    W. M. Farmer and M. v. Mohrenschildt
    In: B. Buchberger, G. Gonnet, and M. Hazewinkel, eds, Mathematical Knowledge Management, special issue of Annals of Mathematics and Artificial Intelligence, 38:165–191, 2003.
  15. A Formal Framework for Managing Mathematics Online
    W. M. Farmer and M. v. Mohrenschildt
    In: B. Buchberger and O. Caprotti, eds, Electronic Proceedings of the First International Workshop on Mathematical Knowledge Management: MKM 2001, 37 pp., RISC, Hagenburg, Austria, September 24–26, 2001.
    Preliminary version of the paper above.
  16. A proposal for the development of an interactive mathematics laboratory for mathematics education PDF
    W. M. Farmer
    In: E. Melis, ed., Proceedings of the Workshop on Deduction Systems for Mathematics Education, pp. 20–25, CADE-17, Carnegie Mellon University, Pittsburgh, Pennsylvania, June 16, 2000.
  17. Transformers for symbolic computation and formal deduction Abstract PDF
    W. M. Farmer and M. v. Mohrenschildt
    In: S. Colton, U. Martin and V. Sorge, eds., Proceedings of the Workshop on the Role of Automated Deduction in Mathematics, pp. 36–45, CADE-17, Carnegie Mellon University, Pittsburgh, Pennsylvania, June 20–21, 2000.
  18. The Interactive Mathematics Laboratory Abstract Online
    W. M. Farmer
    In: Proceedings of the 31st Annual Midwest Instruction and Computing Symposium (MICS '98), pp. 84–94, Fargo, North Dakota and Moorhead, Minnesota, April 16–18, 1998.

B. IMPS Interactive Mathematical Proof System

  1. Panoptes: An exploration tool for formal proofs Abstract PDF
    W. M. Farmer and O. Grigorov
    In: S. Autexier and C. Benzmüller, eds., Proceedings of the 8th International Workshop on User Interfaces for Theorem Provers (UITP'08) (TPHOLs 2008, Concordia University, Montréal, Québec, Canada, August 22, 2008), Electronic Notes in Theoretical Computer Science (ENTCS), 226:39–48, 2009.
  2. IMPS Abstract
    W. M. Farmer
    In: F. Wiedijk, ed., The Seventeen Provers of the World, Lecture Notes in Computer Science (LNCS), 3600:72–87, 2006.
  3. A scheme for defining partial higher-order functions by recursion Abstract PDF Online
    W. M. Farmer
    In: A. Butterfield, ed., 3rd Irish Workshop on Formal Methods, 13 pp., electronic Workshops in Computing, Springer-Verlag, 1999.
  4. IMPS: An updated system description PDF
    W. M. Farmer, J. D. Guttman, and F. J. Thayer Fábrega
    In: M. McRobbie and J. Slaney, eds., Automated Deduction—CADE-13, Lecture Notes in Computer Science (LNCS), 1104:298–302, 1996.
  5. Contexts in mathematical reasoning and computation Abstract
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    Journal of Symbolic Computation, 19:201–216, 1995.
  6. Proof script pragmatics in IMPS Abstract PDF
    W. M. Farmer, J. D. Guttman, M. E. Nadel, and F. J. Thayer
    In: A. Bundy, ed., Automated Deduction—CADE-12, Lecture Notes in Computer Science (LNCS), 814:356–370, 1994.
  7. Reasoning with contexts
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    In: A. Miola, ed., Design and Implementation of Symbolic Computation Systems, Lecture Notes in Computer Science (LNCS), 722:216–228, 1993.
    Preliminary version of Contexts in mathematical reasoning and computation.
  8. The IMPS user's manual HTML PDF
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    Technical Report M-93B138, 289 pp., The MITRE Corporation, November 1993.
  9. IMPS: An Interactive Mathematical Proof System Abstract PDF
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    Journal of Automated Reasoning, 11:213–248, 1993.
  10. IMPS: System description PDF
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    In: D. Kapur, ed., Automated Deduction—CADE-11, Lecture Notes in Computer Science (LNCS), 607:701–705, 1992.
  11. Two computer-supported proofs in metric space topology PDF
    W. M. Farmer and F. J. Thayer
    Notices of the American Mathematical Society, 38:1133–1138, 1991.
  12. IMPS: An Interactive Mathematical Proof System (system description)
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    In: M. E. Stickel, ed., 10th International Conference on Automated Deduction, Lecture Notes in Computer Science (LNCS), 449:653–654, 1990.
    Extended Abstract.

C. Logics and Set Theories for Mechanized Mathematics

  1. Theory Morphisms in Church's Type Theory with Quotation and Evaluation Abstract PDF
    W. M. Farmer
    In: H. Geuvers et al., eds., Intelligent Computer Mathematics, Lecture Notes in Computer Science (LNCS), 10383:147–162, 2017.
    Preprint: arXiv:1703.02117 (17 pp.), 2017.
  2. Incorporating quotation and evaluation into Church's type theory Abstract PDF
    W. M. Farmer
    Preprint: arXiv:1612.02785 (72 pp.), 2016 (revised 2017).
    This is a greatly extended version of the paper below.
  3. Incorporating quotation and evaluation into Church's type theory: Syntax and semantics Abstract PDF
    W. M. Farmer
    In: M. Kohlhase et al., eds., Intelligent Computer Mathematics, Lecture Notes in Computer Science (LNCS), 9791:83–98, 2016.
    Preprint: arXiv:1605.07068, 2016.
  4. Simple type theory with undefinedness, quotation, and evaluation Abstract PDF
    W. M. Farmer
    McSCert Report 13, 87 pp., McMaster University, 2014 (revised 2016).
    Preprint: arXiv:1406.6706, 2014 (revised 2016).
  5. Logics with undefinedness PDF
    W. M. Farmer
    Tutorial given at CADE-22, McGill University, Montreal, Quebec, Canada, August 2, 2009.
  6. Andrews' type system with undefinedness Abstract PDF
    W. M. Farmer
    In: C. Benzmueller, C. Brown J. Siekmann, and R. Statman, eds., Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on his 70th Birthday, Studies in Logic, pp. 223–242, College Publications, 2008.
    Preprint: arXiv:1406.7492, 2014.
  7. The seven virtues of simple type theory Abstract PDF Online
    W. M. Farmer
    Journal of Applied Logic, 6:267–286, 2008.
  8. Chiron: A set theory with types, undefinedness, quotation, and evaluation Abstract PDF
    W. M. Farmer
    SQRL Report No. 38, 154 pp., McMaster University, 2007 (revised 2012).
    Preprint: arXiv:1305.6206, 2013.
  9. Chiron: A multi-paradigm logic Abstract PDF
    W. M. Farmer
    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.
  10. Formalizing undefinedness arising in calculus Abstract PDF Online
    W. M. Farmer
    In: D. Basin and M. Rusinowitch, eds., Automated Reasoning, Lecture Notes in Computer Science (LNCS), 3097:475–489, 2004.
  11. A basic extended simple type theory Abstract PDF
    W. M. Farmer
    SQRL Report No. 14, 12 pp., McMaster University, 2003 (revised 2004).
  12. STMM: A Set Theory for Mechanized Mathematics Abstract PDF
    W. M. Farmer
    Journal of Automated Reasoning, 26:269–289, 2001.
  13. A set theory with support for partial functions Abstract PDF
    W. M. Farmer and J. D. Guttman
    In: E. Thijsse, F. Lepage, and H. Wansing, eds, Partiality and Modality, special issue of Studia Logica, 66:59–78, 2000.
  14. STMM and partial functions
    W. M. Farmer
    In: M. Kerber, ed., Proceedings of the Workshop on the Mechanization of Partial Functions, pp. 3–14, CADE-15, Lindau, Germany, July 5, 1998.
    Preliminary version of STMM: A Set Theory for Mechanized Mathematics.
  15. A set theory for mechanized mathematics
    W. M. Farmer
    926th AMS Meeting Program (Southeast Sectional Meeting, Georgia Institute of Technology), p. 481, American Mathematical Society, October 17–19, 1997.
    Abstract.
  16. Mechanizing the traditional approach to partial functions Abstract PDF
    W. M. Farmer
    In: W. Farmer, M. Kerber, and M. Kohlhase, eds., Proceedings of the Workshop on the Mechanization of Partial Functions, pp. 27–32, CADE-13, Rutgers University, New Brunswick, New Jersey, July 30, 1996.
    Abbreviated version of Reasoning about partial functions with the aid of a computer.
  17. Reasoning about partial functions with the aid of a computer Abstract
    W. M. Farmer
    Erkenntnis, 43:279–294, 1995.
  18. A simple type theory with partial functions and subtypes Abstract
    W. M. Farmer
    Annals of Pure and Applied Logic, 64:211–240, 1993.
  19. A simple theory of types with partial functions and subtypes
    W. M. Farmer and J. D. Guttman
    Journal of Symbolic Logic 58:754, 1993.
    Abstract.
  20. A partial functions version of Church's simple theory of types Abstract
    W. M. Farmer
    Journal of Symbolic Logic, 55:1269–1291, 1990.

D. Little Theories Method

  1. Realms: A structure for consolidating knowledge about mathematical theories Abstract PDF
    J. Carette, W. M. Farmer, and M. Kohlhase
    In: S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban, eds., Intelligent Computer Mathematics, Lecture Notes in Computer Science (LNCS), 8543:252–266, 2014.
    Preprint: arXiv:1405.5956, 2014.
  2. Modules for a large library of formalized mathematics
    W. M. Farmer
    AMS Special Session on Formal Mathematics for Mathematicians: Developing Large Repositories of Advanced Mathematics, JMM 2011, JMM abstract 1067-03-1782, 2011.
    Abstract.
  3. An infrastructure for intertheory reasoning Abstract PDF Online
    W. M. Farmer
    In: D. McAllester, ed., Automated Deduction—CADE-17, Lecture Notes in Computer Science (LNCS), 1831:115–131, 2000.
  4. Perspective switching using theories and interpretations PDF
    W. M. Farmer
    In: J. Albus, A. Meystel, and R. Quintero, eds., Intelligent Systems: A Semiotic Perspective, Vol. I, pp. 206–207, National Institute of Standards and Technology, Gaithersburg, MD, October 20–23, 1996.
    Extended Abstract.
  5. Theory interpretation in simple type theory Abstract PDF
    W. M. Farmer
    In: J. Heering et al., eds., Higher-Order Algebra, Logic, and Term Rewriting, Lecture Notes in Computer Science (LNCS), 816:96–123, 1994.
  6. A general method for safely overwriting theories in mechanized mathematics systems Abstract PDF
    W. M. Farmer
    Technical Report, 21 pp., The MITRE Corporation, 1994.
  7. A general method for safely overwriting theories in mechanized mathematics systems
    W. M. Farmer
    In: D. Basin, F. Giunchiglia, and M. Kaufmann, eds., Proceedings of the Workshop on the Correctness and Metatheoretical Extensibility of Automated Reasoning Systems, pp. 46–48, CADE-12, Nancy, France, June 26, 1994.
    Extended Abstract.
  8. Little theories Abstract PDF
    W. M. Farmer, J. D. Guttman, and F. J. Thayer
    In: D. Kapur, ed., Automated Deduction—CADE-11, Lecture Notes in Computer Science (LNCS), 607:567–581, 1992.
  9. Theory interpretations in computerized mathematics
    W. M. Farmer
    Journal of Symbolic Logic, 57:356, 1992.
    Abstract.
  10. Abstract data types in many-sorted second-order logic
    W. M. Farmer
    Technical Report M87-64, 29 pp., The MITRE Corporation, October 1987.

E. Mathematical Knowledge Management (MKM)

  1. A review of Mathematical Knowledge Management Abstract PDF
    J. Carette and W. M. Farmer
    In: J. Carette, L. Dixon, C. Sacerdoti Coen, and S. M. Watt, eds., Intelligent Computer Mathematics, Lecture Notes in Computer Science (LNCS), 5625:233–246, 2009.
  2. Mathematical knowledge management Abstract
    W. M. Farmer
    In: D. G. Schwartz, ed., Encyclopedia of Knowledge Management, pp. 599–604, Information Science Reference, 2005. Online
    Also in: M. E. Jennex, ed., Knowledge Management: Concepts, Methodologies, Tools and Applications, Chapter 7.3, pp. 2976–2983, Information Science Reference, 2007. Online
  3. MKM: A new interdisciplinary field of research Abstract PDF
    W. M. Farmer
    ACM SIGSAM Bulletin, 38:47–52, 2004.

F. Formal Methods

  1. FCL: A formal language for writing contracts Abstract PDF
    W. M. Farmer and Q. Hu
    In: S. H. Rubin and T. Bouabana Tebibel, eds., Quality Software Through Reuse and Integration, 19 pp., Springer, 2017 (forthcoming). This is a extended version of the paper below.
  2. A formal language for writing contracts Abstract PDF
    W. M. Farmer and Q. Hu
    In: 2016 IEEE International Conference on Information Reuse and Integration, 8 pp., IEEE, 2016.
  3. A verified compiler for Multithreaded PreScheme Abstract Online
    W. M. Farmer and J. D. Ramsdell
    Technical Report, 180 pp., The MITRE Corporation, 1996.
  4. Formal numerical program analysis Abstract PDF
    W. M. Farmer and F. J. Thayer
    Technical Report, 52 pp., The MITRE Corporation, 1994.
  5. 8 papers on the VLISP verified programming language implementation Online
    W. M. Farmer, J. D. Guttman, L. G. Monk, J. D. Ramsdell, and V. Swarup
    Technical Reports M-92B91, ..., M-92B98, 487 pp., The MITRE Corporation, September 1992.
  6. Towards a discipline for developing verified software Abstract PDF
    W. M. Farmer, D. M. Johnson, and F. J. Thayer
    In: J. H. Burrows and P. R. Gallagher, Jr., eds., Proceedings of the 9th National Computer Security Conference, pp. 91–98, National Bureau of Standards, Gaithersburg, Maryland, September 15–18, 1986.
    Also in: R. Turn, ed., Advances in Computer System Security, Vol. III, Artech House, Norwood, Massachusetts, pp. 176–183, 1988.

G. Security of Mobile Agents

  1. Security for mobile agents: Issues and requirements Abstract PDF
    W. M. Farmer, J. D. Guttman, and V. Swarup
    In: S. Wakid and J. Davis, eds., Proceedings of the 19th National Information Systems Security Conference, Vol. 2, pp. 591–597, Baltimore Convention Center, Baltimore, Maryland, October 22–25, 1996.
  2. Security for mobile agents: Authentication and state appraisal Abstract PDF
    W. M. Farmer, J. D. Guttman, and V. Swarup
    In: E. Bertino et al., eds., Computer Security—ESORICS 96, Lecture Notes in Computer Science (LNCS), 1146:118–130, 1996.

H. Graph Rewriting and Combinatory Algebra

  1. Redex capturing in term graph rewriting (concise version)
    W. M. Farmer and R. J. Watro
    In: R. V. Book, ed., Rewriting Techniques and Applications, Lecture Notes in Computer Science (LNCS), 488:13–24, 1991.
  2. Redex capturing in term graph rewriting Abstract
    W. M. Farmer and R. J. Watro
    International Journal of the Foundations of Computer Science, 1:369–386, 1990.
  3. A correctness proof for combinator reduction with cycles Abstract
    W. M. Farmer, J. D. Ramsdell, and R. J. Watro
    ACM Transactions on Programming Languages and Systems, 12:123–134, 1990.
  4. A correctness proof for combinator reduction with cycles
    W. M. Farmer, J. D. Ramsdell, and R. J. Watro
    Journal of Symbolic Logic, 55:373–374, 1990.
    Abstract.
  5. Computing with the Curry Chip Abstract
    W. M. Farmer, J. D. Ramsdell, and R. J. Watro
    Technical Report M89-59, 89 pp., The MITRE Corporation, September 1989.

I. Higher-Order Unification

  1. Simple second-order languages for which unification is undecidable Abstract
    W. M. Farmer
    Theoretical Computer Science, 87:25–41, 1991.
  2. A unification algorithm for second-order monadic terms Abstract
    W. M. Farmer
    Annals of Pure and Applied Logic, 39:131–174, 1988.
  3. An algorithm for the unification of second-order monadic terms
    W. M. Farmer
    Journal of Symbolic Logic, 51:841–842, 1986.
    Abstract.

J. Length of Proofs

  1. The Kreisel length-of-proof problem Abstract
    W. M. Farmer
    In: Logic and Combinatorics, eds. J. Franco, J. M. Dunn, and W. H. Wheeler, special issue of Annals of Mathematics and Artificial Intelligence, 6:27–55, 1992.
  2. A unification-theoretic method for investigating the k-provability problem Abstract
    W. M. Farmer
    Annals of Pure and Applied Logic, 51:173–214, 1991.
  3. The k-provability problem for Gentzen-style sequent systems Abstract
    W. M. Farmer
    Technical Report M89-20, 13 pp., The MITRE Corporation, February 1989.
  4. Some results on the k-provability problem
    W. M. Farmer
    Journal of Symbolic Logic, 53:1003, 1988.
    Abstract.
  5. Length of Proofs and Unification Theory Abstract
    W. M. Farmer
    Ph.D. Thesis, University of Wisconsin-Madison, 1984.

K. Education

  1. The use of formal reasoning technology in mathematics education: Opportunities and challenges Abstract
    W. M. Farmer
    In: P. Courtieu and H. Geuvers, eds., Proceedings of the Workshop on Proof Assistants and Types in Education (PATE 2007), Paris, France, June 25, 2007.
    Abstract.
  2. Simple type theory: Simple steps towards a formal specification Abstract Online
    W. M. Farmer and M. v. Mohrenschildt
    In: Proceedings of the 34th Annual Frontiers in Education (FIE 2004), CD-ROM, IEEE, pp. F1C-1–F1C-6, 2004.
  3. Network instructional units Online
    W. M. Farmer and R. E. Mowe
    In: Proceedings of the 32st Annual Midwest Instruction and Computing Symposium (MICS '99), 9 pp., La Crosse, Wisconsin, April 15–17, 1999.

L. Miscellaneous

  1. A simple framework for contracts in federated database systems Abstract PDF
    W. M. Farmer and M. E. Nadel
    Technical Report, 22 pp., The MITRE Corporation, 1995.

M. Edited Conference Proceedings

  1. Intelligent Computer Mathematics (18th Symposium, Calculemus 2011 and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011, Proceedings) Online
    J. H. Davenport, W. M. Farmer, F. Rabe, and J. Urban, eds.
    Lecture Notes in Computer Science (LNCS), 6824:1–312, 2011.
  2. Conference on Intelligent Computer Mathematics Work-in-Progress Papers Proceedings
    A. Asperti, J. H. Davenport, W. M. Farmer, F. Rabe, and J. Urban, eds.
    Technical Report UBLCS-2011-04, University of Bologna, 2011.
  3. Mathematical Knowledge Management (5th International Conference, MKM 2006, Wokingham, UK, August 2006, Proceedings) Online
    J. M. Borwein and W. M. Farmer, eds.
    Lecture Notes in Computer Science (LNCS), 4108:1–295, 2006.
  4. Proceeding of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus 2005) Online
    J. Carette and W. M. Farmer, eds.
    Electronic Notes in Theoretical Computer Science (ENTCS), 151:1–178, 2006.
  5. Proceedings of the Workshop on the Mechanization of Partial Functions Online
    W. Farmer, M. Kerber, and M. Kohlhase, eds.
    CADE-13, Rutgers University, New Brunswick, New Jersey, USA, July 30, 1996.

N. Reviews

  1. Review of Jan Krajícek, On the number of steps in proofs, Annals of Pure and Applied Logic, 41:153–178, 1989.
    W. M. Farmer, Journal of Symbolic Logic, 56:334–335, 1991.
  2. Review of Jan Krajícek, The number of proof lines and the size of proofs in first order logic, Archive for Mathematical Logic, 27:69–84, 1988.
    W. M. Farmer, Journal of Symbolic Logic, 54:1107–1108, 1989.
  3. Review of Larry Wos, Automated Reasoning: 33 Basic Research Problems, Prentice Hall, Englewood Cliffs, New Jersey, 1988.
    W. M. Farmer, Journal of Symbolic Logic, 53:1258–1259, 1988.