|
>>> p1 = lexpr('father_of(art,john)')
>>> p2 = lexpr('mother_of(ann,john)')
>>> p3 = lexpr('all x.all y.(father_of(x,y) -> parent_of(x,y))')
>>> p4 = lexpr('all x.all y.(mother_of(x,y) -> parent_of(x,y))')
>>> c = lexpr('all x.(parent_of(x,john) -> ANSWER(x))')
>>> logic._counter._value = 0
>>> tp = ResolutionProverCommand(None, [p1,p2,p3,p4,c])
>>> sorted(tp.find_answers())
[<ConstantExpression ann>, <ConstantExpression art>]
>>> print(tp.proof())
[ 1] {father_of(art,john)} A
[ 2] {mother_of(ann,john)} A
[ 3] {-father_of(z3,z4), parent_of(z3,z4)} A
[ 4] {-mother_of(z7,z8), parent_of(z7,z8)} A
[ 5] {-parent_of(z10,john), ANSWER(z10)} A
[ 6] {parent_of(art,john)} (1, 3)
[ 7] {parent_of(ann,john)} (2, 4)
[ 8] {ANSWER(z10), -father_of(z10,john)} (3, 5)
[ 9] {ANSWER(art)} (1, 8)
[10] {ANSWER(z10), -mother_of(z10,john)} (4, 5)
[11] {ANSWER(ann)} (2, 10)
[12] {ANSWER(art)} (5, 6)
[13] {ANSWER(ann)} (5, 7)
|