Some Two-Sided Clausal Tableaux

The following images show two-sided clausal tableaux proofs underlying interpolation for a simple synthesis problem, obtained by different provers or prover configurations.

Input: Two Programs and a Vocabulary

P = [(p(X) <-- q(X))],
Q = [(r(X) <-- p(X)),
     (r(X) <-- q(X))],
V = [p, r].
Output: The Synthesized Program
R = [(r(A)<--p(A))]
Input of the Underlying Craig-Lyndon Interpolation, as Implication
all(x, ((~q0(x);p0(x)),
        (~q1(x);p1(x)),
        (~p0(x);r0(x)),
        (~p1(x);r1(x)),
        (~q0(x);r0(x)),
        (~q1(x);r1(x)))),
all(x, ((~p0(x);p1(x)),(~q0(x);q1(x)),(~r0(x);r1(x))))
->
(ex(x, (p0(x),~p1(x);
        q_prime_0(x),~q_prime_1(x);
        r0(x),~r1(x)));
 ex(x, (q_prime_0(x),~p0(x);q_prime_1(x),~p1(x)));
 all(x, ((~p0(x);r0(x)),
         (~p1(x);r1(x)),
         (~q_prime_0(x);r0(x)),
         (~q_prime_1(x);r1(x)))))
Some Clausal Tableaux Proofs of the Implication Underlying Interpolation
Proof by CMProver.
Proof by CMProver.
Proof by CMProver, hyper form
Proof by CMProver, transformed to hyper form.
Converted proof by Prover9.
Resolution proof by Prover9, converted to a clausal tableau with the hyper property.

Contact: info@christophwernhard.com