Observation (from AI research)

• Constructive theorem provers can compute results as a side-effect of proving theorems.
• To prove a theorem of the form \(\exists x: P(x)\), construct a value for \(x\) that satisfies \(P\).
• \(P\) can be a specification of what we need to compute.
• Therefore, to compute a value satisfying any given specification, prove that such a value exists!

Core idea

Use logic specifications for a higher-level approach to programming.

• Specify what conditions need to be satisfied, but not how to satisfy them.
• A declarative approach versus a procedural one.

Example: Sorting

1. Logical specification: \(y\) is a sorted version of \(x\) if \(y\) is a permutation of \(x\) and \(y\) is ordered. Prolog syntax:

sorted(X, Y) :- permutation(X, Y), ordered(Y).

2. Theorem proving as execution:

• To sort a list \(a\) using a logical specification, ask a theorem prover to constructively prove that a sorted version of \(a\) exists.
• That is prove: \(\exists b: \mathrm{sorted}(a, b)\)
• We haven't specified how to sort a lists; that is up to the theorem prover to discover from the logical specification of sorted.
• Many standard theorem-provinig techniques for first-order logic are constructive.
• Example: resolution proof procedure, which is the basis of Prolog.