Problem Set 8

Automated theorem prover

Before you start this problem set

Please fill out a survey about the time you spent on Problem Set 7.

Download

• pset08_definitions.dfy
• pset08.dfy
• pset08_validator.dfy
• pset08_hints.dfy ← but don’t read yet

The structure here follows that of previous psets: read pset08_definitions.dfy to see our supporting definitions on an automated theorem prover for “less than” facts, complete pset08.dfy with your edits, and use pset08_validator.dfy to confirm you’re done.

See also pset08_hints.dfy for suggestions, in case you get stuck. But beware that this file may give away some of the interesting challenges.

• Please review the main proofs from class 15 in modules UnionFind and TheoremProver and the graph reachability proofs from class 16 before you look at the hints.

• For proving EntailedCorrect the hints file provides the statement and proof of some lemmas that require a bit of heavy lifting! If you’re stuck and would just like to know the idea we used without seeing our code, click here: find a topological sort that shows a contradiction.