Model Elimination
Max time of proof
Max length of proof
Clauses
p(x),-p(x) q(x,y),-q(x,a) -q(b,y) -q(b,a) -p(f(y))
Proof
1: p(x) Hypothesis 2: q(v0, v1) [p(v0)]^0 Expansion on literal 1 with hypothesis -p(v0) q(v0, v1) by substitution x := v0 3: -q(b, v3) -q(b, a) -p(f(v3)) [q(v2, a)]^0 [p(v2)]^0 Expansion on literal 1 with hypothesis -q(v2, a) -q(b, v3) -q(b, a) -p(f(v3)) by substitution v1 := a; v0 := v2 4: -q(b, a) -p(f(a)) [q(b, a)]^0 [p(b)]^0 Reduction of the literal 4 by substitution v3 := a; v2 := b 5: -p(f(a)) [q(b, a)]^0 [p(b)]^0 Reduction of the literal 3 6: [-p(f(a))]^0 [q(b, a)]^0 [p(b)]^0 Expansion on literal 1 with hypothesis p(v0) by substitution v0 := f(a) 7: [q(b, a)]^0 [p(b)]^0 Remove 8: [p(b)]^0 Remove 9: F Remove Proof duration (in seconds): 0.000105857849121
examples
|
syntax
|
info
|
home
|
download
Last Modified : 02-Dec-2019