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