|
>>> p1 = lp.parse('father_of(art,john)')
>>> p2 = lp.parse('mother_of(ann,john)')
>>> p3 = lp.parse('all x.all y.(father_of(x,y) -> parent_of(x,y))')
>>> p4 = lp.parse('all x.all y.(mother_of(x,y) -> parent_of(x,y))')
>>> c = lp.parse('all x.(parent_of(x,john) -> ANSWER(x))')
>>> logic._counter._value = 0
>>> tp = ResolutionCommand(None, [p1,p2,p3,p4,c])
>>> print tp.find_answers()
set([<VariableExpression art>, <VariableExpression ann>])
>>> tp.show_proof()
[ 1] {father_of(art,john)} A
[ 2] {mother_of(ann,john)} A
[ 3] {-father_of(z4,z3), parent_of(z4,z3)} A
[ 4] {-mother_of(z8,z7), parent_of(z8,z7)} 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)
|