Interactive Proofs

The namespace tnoc.ip provides a number of functions that allow the user to step through small interactive proofs (described on pages 521+) themselves.

The conversation between Arthur and Merlin that takes place on page 524 can be recreated as follows:

(def phi '(A :x (E :y (A :z (and (or :x :y :z) (or (not :x) (not :y) (not :z)))))))

(map pprint-interaction (interact phi [3 2 5]))
=>
([(A :x) "1" "1 - x + x^2" true]
 [(E :y) "7" "3 - 11y + 6y^2" true]
 [(A :z) "5" "-1 + 8z - 12z^2" true]
 [(and (or :x :y :z) (or (not :x) (not :y) (not :z))) "-261" nil true])

The first element of each of these tuples is the part of the formula that is currently being investigated. The second element is what Merlin claims is the simplified arithmetization of this formula. The third element is the arithmetization of the body of the quantifier, which Merlin offers as proof for the foregoing claim. Note that this is nil in the last row since here Arthur requires no further proof. And the fourth element denotes whether Arthur was able to verify Merlin's claim.

Adding the reducing operators gives the following:

(def phi-R '(A :x (R :x (E :y (R :x (R :y (A :z (R :x (R :y (R :z (and (or :x :y :z) (or (not :x) (not :y) (not :z)))))))))))))

(map pprint-interaction (interact phi-R [3 2 5]))
=>
([(A :x) "1" "1" true]
 [(R :x) "1" "1 - x + x^2" true]
 [(E :y) "7" "3 - 5y" true]
 [(R :x) "-7" "2 - 3x" true]
 [(R :y) "-7" "3 - 11y + 6y^2" true]
 [(A :z) "5" "-1 - 4z" true]
 [(R :x) "-21" "-3 - 6x" true]
 [(R :y) "-21" "-7 - 7y" true]
 [(R :z) "-21" "-1 + 8z - 12z^2" true]
 [(and (or :x :y :z) (or (not :x) (not :y) (not :z))) "-261" nil true])

Also, one can go through an interactive proof step-by-step by using the function interact-manually:

(interact-manually phi)
=> [(A :x) 1 1 - x + x^2 true]
=> :x needs an assignment.
3
=> [(E :y) 7 3 - 11y + 6y^2 true]
=> :y needs an assignment.
2
=> [(A :z) 5 -1 + 8z - 12z^2 true]
=> :z needs an assignment.
5
=> [(and (or :x :y :z) (or (not :x) (not :y) (not :z))) -261 nil true]
=> nil