Automated theorem proving

Conference: AI and Theorem Proving (AITP)

Systems

  • IMPS: An Interactive Mathematical Proof System
    • Based on simple type theory, a typed lambda calculus with expressivity of HOL
    • Farmer, Guttman, Thayer, 1993: IMPS (doi, pdf)
    • Farmer, 2008: The seven virtues of simple type theory (doi, pdf)

Literature

Books

  • Robinson & Voronov, 2001: Handbook of Automated Reasoning
  • Harrison, 2009: Handbook of Practical Logic and Automated Reasoning