The Online Books Page

Automatic theorem proving

See also what's at Wikipedia, your library, or elsewhere.

• Artificial intelligence
• Proof theory

• Automatic theorem proving -- Computer programs
• Nuprl (Computer system)

• Automated theorem proving
• Theorem proving, Automated
• Theorem proving, Automatic

• Concrete Semantics with Isabelle/HOL (2018), by Tobias Nipkow and Gerwin Klein (PDF with commentary at concrete-semantics.org)
• Implementing Mathematics with the Nuprl Proof Development System (1985), ed. by R. L. Constable (illustrated HTML at Cornell)
• Isabelle/HOL: A Proof Assistant for Higher-Order Logic (2018), by Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel (PDF in Germany)
• Logic for Computer Science: Foundations of Automatic Theorem Proving (revised edition, 2003, with errata for the original edition and other papers), by Jean H. Gallier (PDF and Postscript files here at Penn)

• Certified Programming with Dependent Types (latest electronic edition), by Adam Chlipala (PDF and HTML with commentary at chlipala.net)

• Implementing Mathematics with the Nuprl Proof Development System (1985), ed. by R. L. Constable (illustrated HTML at Cornell)

Items below (if any) are from related and broader terms.

• Practical Artificial Intelligence Programming With Java (third edition, c2008), by Mark Watson (PDF at markwatson.com)
• Artificial Intelligence and Responsive Optimization (second edition, 2003), by Mohammad Khosnevisan, Sukanto Bhattacharya, and Florentin Smarandache (PDF at UNM)
• Are We Spiritual Machines? Ray Kurzweil vs. the Critics of Strong A.I. (c2002), ed. by Jay W. Richards, contrib. by Ray Kurzweil, John R. Searle, Michael J. Denton, William A. Dembski, Thomas S. Ray, and George F. Gilder (at kurzweilai.net)
• Artificial Intelligence (third edition, reprinted with corrections; Reading, MA et al.: Addison-Wesley Pub. Co., 1993), by Patrick Henry Winston (PDF at MIT)
• The Age of Intelligent Machines (c1992), by Ray Kurzweil (at kurzweilai.net)
• Artificial Intelligence and Games (2018), by Georgios N. Yannakakis and Julian Togelius (PDF with commentary at gameaibook.org)
• The Boundaries of Humanity: Humans, Animals, Machines (Berkeley: University of California Press, 1991), ed. by James J. Sheehan and Morton Sosna (HTML at UC Press)
• Artificial Intelligence Through Prolog (1988), by Neil C. Rowe (HTML at nps.edu)
• How Mobile Robots can Self-Organise a Vocabulary (Berlin: Language Science Press, c2015), by Paul Vogt
  • PDF wih commentary at langsci-press.org
  • PDF at OAPEN
• Applications of Robotics and Artificial Intelligence to Reduce Risk and Improve Effectiveness: A Study for the United States Army (1983), by National Research Council Commission on Engineering and Technical Systems (page images with commentary at NAP)
• When Things Start to Think (c1999), by Neil A. Gershenfeld (HTML with commentary at kurzweilai.net)
• Elements of Robotics (Cham: Springer Open, c2018), by M. Ben-Ari and Francesco Mondada (PDF and EPub with commentary at EPFL and Springer)
• Paradigms of Artificial Intelligence Programming: Case Studies in Common Lisp (c1992), by Peter Norvig (multiple formats with commentary at Github)
• From Bricks to Brains: The Embodied Cognitive Science of LEGO Robots (Edmonton: AU Press, c2010), by Michael Robert William Dawson, Brian Dupuis, and Michael Wilson (PDF with commentary at AU Press)
• The Computer Revolution in Philosophy: Philosophy, Science and Models of Mind (1978, with added notes and corrections), by Aaron Sloman (HTML and PDF with commentary in the UK)
• The Origin and Its Meaning, by Roger Ellman (PDF files at the-origin.org)

• The Future Computed: Artificial Intelligence and its Role in Society (2018), by Microsoft Corporation (PDF with commentary at microsoft.com)

• Accelerando (2005), by Charles Stross (multiple formats with commentary at antipope.org)
• Old Soldiers (included on a Baen CD image; c2005), by David Weber
  • zipped CD ISO at thefifthimperium.com; 183 MB
  • zipped CD files at thefifthimperium.com; 185 MB
• Bolo! (included on a CD image), by David Weber, contrib. by Keith Laumer
  • zipped CD ISO at thefifthimperium.com; 151 MB
  • zipped CD files at thefifthimperium.com; 152 MB
• The Fourth "R", by George O. Smith
  • Gutenberg text
  • page images at durendal.org
• Halo, by Tom Maddox (HTML at dthomasmaddox.com)

• This Could Be Important: My Life and Times with the Artificial Intelligentsia (Pittsburgh: ETC Press, c2019), by Pamela McCorduck (HTML with commentary at pressbooks.com)

• The Future Computed: Artificial Intelligence and its Role in Society (2018), by Microsoft Corporation (PDF with commentary at microsoft.com)

• Journal of Artificial Intelligence Research (1993-) (full serial archives)

• Can We Trust AI? (Baltimore: Johns Hopkins University Press, c2022), by Rama Chellappa, contrib. by Eric Niiler (multiple formats with commentary at Project MUSE)
• The Future Computed: Artificial Intelligence and its Role in Society (2018), by Microsoft Corporation (PDF with commentary at microsoft.com)

• Defending AI Research: A Collection of Essays and Reviews (c1996), by John McCarthy (PDF at Stanford)

• Artificial Communication: How Algorithms Produce Social Intelligence (Cambridge, MA and London: MIT Press, c2022), by Elena Esposito (PDF files with commentary at MIT Press)
• The Future Computed: Artificial Intelligence and its Role in Society (2018), by Microsoft Corporation (PDF with commentary at microsoft.com)

• Artificial Intelligence: Foundations of Computational Agents (second edition, 2017), by David L. Poole and Alan K. Mackworth (illustrated HTML with commentary at artintinfo)

• Adaptive Control: Stability, Convergence, and Robustness (c1994), by Shankar Sastry and Marc Bodson (PDF files with commentary at Utah)

• The Elements of Statistical Learning: Data Mining, Inference, and Prediction (second edition, 2009), by Trevor Hastie, Robert Tibshirani, and J. H. Friedman (PDF with commentary at Stanford)

• Programming Computer Vision with Python (prepublication draft, 2012), by Jan Erik Solem (PDF with commentary at programmingconputervision.com)
• Computer Vision: Algorithms and Applications (prepublication draft, c2010), by Richard Szeliski (PDF with commentary at szeliski.org)

• Artificial Intelligence and Responsive Optimization (second edition, 2003), by Mohammad Khosnevisan, Sukanto Bhattacharya, and Florentin Smarandache (PDF at UNM)
• Expert Systems in Prolog, by Dennis Merritt (HTML with commentary at amzi.com)

• Graph Representation Learning (prepublication version, 2020), by William L. Hamilton (PDF at McGill)
• Probabilistic Machine Learning for Civil Engineers (prepublication version; 2020), by James-A. Goulet (PDF files with commentary at polymtl.ca)
• Foundations of Machine Learning (second edition; Cambridge, MA and London: MIT Press, c2018), by Mehryar Mohri, Afshin Rostamizadeh, and Ameet Talwalkar (HTML at ublish.com)
• Elements of Causal Inference: Foundations and Learning Algorithms (Cambridge, MA and London: MIT Press, c2017), by Jonas Peters, Dominik Janzing, and Bernhard Schölkopf (PDF with commentary at MIT Press)
• Machine Learning (main text c1997; additional chapters c2017), by Tom M. Mitchell (PDF with commentary at CMU)
• Deep Learning (prepublication version; 2016), by Ian Goodfellow, Yoshua Bengio, and Aaron Courville (illustrated HTML with commentary at deeplearningbook.org)
• Bayesian Reasoning and Machine Learning (free online edition, c2014), by David Barber (PDF with commentary in the UK)
• The Elements of Statistical Learning: Data Mining, Inference, and Prediction (second edition, 2009), by Trevor Hastie, Robert Tibshirani, and J. H. Friedman (PDF with commentary at Stanford)
• Reinforcement Learning: An Introduction (first and second editions, 1998 and 2018), by Richard S. Sutton and Andrew G. Barto (HTML and PDF at incompleteideas.net)
• Pattern Recognition and Machine Learning (c2006), by Christopher M. Bishop (PDF at microsoft.com)
• Ethics and Data Science (c2019), by Michael Kosta Loukides, Hilary Mason, and DJ Patil (HTML at oreilly.com)
• A Course in Machine Learning, by Hal Daumé (PDF with commentary at ciml.info)
• Machine Learning, Neural and Statistical Classification, ed. by Donald Michie, D. J. Spiegelhalter, and Charles C. Taylor (PDF and gzipped Postscript in the UK)

More items available under broader and related terms at left.