Title is here

Author Name etc.

email or website etc

Introduction

Item 1 Item 2 is longer Item 3 is also ...

also what? Another item of interest Last comments

A descriptive look

Theorems taste great: The proof of the technique’s “main theorem” is played out for each problem instance. (Used to implement Cooper’s algorithm; see paper.)

Theorems stay crunchy: The “main theorem” is proved once and for all, and is instantiated with each problem.

Theorems are good for you: An external tool finds a proof that can then be replayed in HOL. If proof search dominates this can be very effective.

I want slides like Michael’s

formula ::= formula∧ formula | formula∨ formula |

¬formula | ∃var. formula | ∀var. formula |

numeral | term | term relop term
term  ::= numeral | term+ term | − term |

numeral ∗ term | var

relop  ::= < | ≤ | = | ≥ | >
var  ::= x | y | z …
numeral ::= 0 | 1 | 2 …

I want slides like Michael’s

formula ::= formula∧ formula | formula∨ formula |

¬formula | ∃var. formula | ∀var. formula |

term “is divisible by” numeral numeral | term | term relop term
term  ::= numeral | term+ term | − term |

numeral ∗ term | var

relop  ::= < | ≤ | = | ≥ | >
var  ::= x | y | z …
numeral ::= 0 | 1 | 2 …

Doing it bit by bit 101

In the beginning ... there was dirt and sticks Then came

Clay tablets Blackboards Whiteboards

Then came powerpoint, slitex, foiltex etc.

Then came prosper In the beginning ... there was dirt and sticks Then came

Clay tablets Blackboards Whiteboards

Then came powerpoint, slitex, foiltex etc.

Then came prosper In the beginning ... there was dirt and sticks Then came

Clay tablets Blackboards Whiteboards

Then came powerpoint, slitex, foiltex etc.

Then came prosper In the beginning ... there was dirt and sticks Then came

Clay tablets Blackboards Whiteboards

Then came powerpoint, slitex, foiltex etc.

Then came prosper In the beginning ... there was dirt and sticks Then came

Clay tablets Blackboards Whiteboards

Then came powerpoint, slitex, foiltex etc.

Then came prosper In the beginning ... there was dirt and sticks Then came

Clay tablets Blackboards Whiteboards

Then came powerpoint, slitex, foiltex etc.

Then came prosper In the beginning ... there was dirt and sticks Then came

Clay tablets Blackboards Whiteboards

Then came powerpoint, slitex, foiltex etc.

Then came prosper In the beginning ... there was dirt and sticks Then came

Clay tablets Blackboards Whiteboards

Then came powerpoint, slitex, foiltex etc.

Then came prosper Doing it bit by bit - Real World Applications from Michael

(∃x. 3x + y ≤ 10 ∧ 20 ≤ x − y)

(re-arrange)

≡ (∃x. 3x ≤ 10 − y ∧ 20 + y ≤ x)

     (re-express with evalupper & evallower)

≡ (∃x. evalupper x [(3, 10 − y)] ∧ evallower x [(1, 20 + y)])

(apply theorem)

≡ real_shadow [(3, 10 − y)] [(1, 20 + y)]

(unfold def’n of real_shadow)

≡ 3(20 + y) ≤ (10 − y)
≡ 4y ≤ −50
≡ y ≤ −13

This message appears at the bottom of each page. – p.6/6

Doing it bit by bit - Real World Applications from Michael

(∃x. 3x + y ≤ 10 ∧ 20 ≤ x − y)

(re-arrange)

≡ (∃x. 3x ≤ 10 − y ∧ 20 + y ≤ x)

     (re-express with evalupper & evallower)

≡ (∃x. evalupper x [(3, 10 − y)] ∧ evallower x [(1, 20 + y)])

(apply theorem)

≡ real_shadow [(3, 10 − y)] [(1, 20 + y)]

(unfold def’n of real_shadow)

≡ 3(20 + y) ≤ (10 − y)
≡ 4y ≤ −50
≡ y ≤ −13

This message appears at the bottom of each page. – p.6/6

Doing it bit by bit - Real World Applications from Michael

(∃x. 3x + y ≤ 10 ∧ 20 ≤ x − y)

(re-arrange)

≡ (∃x. 3x ≤ 10 − y ∧ 20 + y ≤ x)

     (re-express with evalupper & evallower)

≡ (∃x. evalupper x [(3, 10 − y)] ∧ evallower x [(1, 20 + y)])

(apply theorem)

≡ real_shadow [(3, 10 − y)] [(1, 20 + y)]

(unfold def’n of real_shadow)

≡ 3(20 + y) ≤ (10 − y)
≡ 4y ≤ −50
≡ y ≤ −13

This message appears at the bottom of each page. – p.6/6

Doing it bit by bit - Real World Applications from Michael

(∃x. 3x + y ≤ 10 ∧ 20 ≤ x − y)

(re-arrange)

≡ (∃x. 3x ≤ 10 − y ∧ 20 + y ≤ x)

     (re-express with evalupper & evallower)

≡ (∃x. evalupper x [(3, 10 − y)] ∧ evallower x [(1, 20 + y)])

(apply theorem)

≡ real_shadow [(3, 10 − y)] [(1, 20 + y)]

(unfold def’n of real_shadow)

≡ 3(20 + y) ≤ (10 − y)
≡ 4y ≤ −50
≡ y ≤ −13

This message appears at the bottom of each page. – p.6/6

Doing it bit by bit - Real World Applications from Michael

(∃x. 3x + y ≤ 10 ∧ 20 ≤ x − y)

(re-arrange)

≡ (∃x. 3x ≤ 10 − y ∧ 20 + y ≤ x)

     (re-express with evalupper & evallower)

≡ (∃x. evalupper x [(3, 10 − y)] ∧ evallower x [(1, 20 + y)])

(apply theorem)

≡ real_shadow [(3, 10 − y)] [(1, 20 + y)]

(unfold def’n of real_shadow)

≡ 3(20 + y) ≤ (10 − y)
≡ 4y ≤ −50
≡ y ≤ −13

This message appears at the bottom of each page. – p.6/6