WIKI page for VTH Automated Theorem Proving

Introduction

Welcome to the Web Page for the VTH Mini-Course on Automated Theorem Proving

Course Announcement at Institute of Mathematics

Details

• Textbook: Introduction to Logic and Automated Theorem Proving, by John Harrison.

• Supplementary text: HOL Light Tutorial

• Supplementary text: Introduction to Objective CAML

Getting Set Up

To start proving theorems on a computer, you should download and install HOL Light. The HOL Light Tutorial (page 5) gives instructions on installing HOL Light. It can be installed on computers under various operating systems.

Dec 7, 2008

Here is a short essay describing the origin of Hales's interest in Automated Theorem Proving. This first lecture was an overview lecture. It described the origin of Hales's interest in formal proof. It gave a brief overview of the functional programming language OCAML and the HOL Light system.

Homework 1 HanoiATPHW1

Dec 14, 2008

• Syntax trees. Representing formulas in mathematics as syntax trees. Infix and prefix operators. Introduction to parsing and printing. Currying functions. Implementing syntax trees in OCAML. Binary number arithmetic as operations on syntax trees.

• The syntax of OCAML is parallel to the syntax of HOL Light.

• Types in OCAML and types in HOL Light. Polymorphic types. Strongly typed languages.

• The rules of logic and the axioms of HOL Light.

• Can formal proofs be reliable?

• Wolfram Blog, "Mathematics, Mathematica, and Certainty" Dec 8, 2007

• John Harrison, "Towards a Self-Verification of HOL-Light"

Dec 21, 2008

The following typics were covered.

• Limits of Reliability.

• Decision procedures for tautology checking. The method of truth tables. Simplification, negated normal form (NNF), conjunctive normal form (CNF), disjunctive normal form (DNF). Satisfiability and tautology. Satisfaction of propositional formulas is NP-complete.

• Interactive theorem proving with backwards-style proofs. Goals and tactics.

• A few comments on the Flyspeck project.

Dec 28, 2008

The following topics were covered.

• Rewriting. An extended example was provided about transforming a propositional formula into negated normal form (NNF), and disjunctive normal form (DNF) by using certain simple tautologies as rewrite rules in HOL Light. The specific example of the associative law (p <=> (q <=> r)) <=> ((p <=> q) <=> r) was used.

• Decision procedures. Harrison's book on Automated Theorem Proving has a chapter on decision procedures. Some of these procedures were mentioned. The example of complex quantifier elimination was described in detail. How quantifier elimination provides a decision procedure for sentences in the first-order language of complex numbers. Transforming a first-order formula into prenex normal form (as described on pages 135-136 of Harrison's book). Quantifier elimination for an innermost existential quantifier.

• Backwards style proof. Using the tactical "THEN" to combine two or more tactics into a single tactic. How to package a interactive proving session in HOL Light into a script that can be saved in a file.