# Resolution Theorem Prover

```>>> from nltk.inference.resolution import *
>>> from nltk.sem import logic
>>> from nltk.sem.logic import *
>>> logic._counter._value = 0
```
```>>> P = read_expr('P')
```

# Test most_general_unification()

```>>> print(most_general_unification(x, x))
{}
>>> print(most_general_unification(A, A))
{}
>>> print(most_general_unification(A, x))
{x: A}
>>> print(most_general_unification(x, A))
{x: A}
>>> print(most_general_unification(x, y))
{x: y}
>>> print(most_general_unification(P(x), P(A)))
{x: A}
>>> print(most_general_unification(P(x,B), P(A,y)))
{x: A, y: B}
>>> print(most_general_unification(P(x,B), P(B,x)))
{x: B}
>>> print(most_general_unification(P(x,y), P(A,x)))
{x: A, y: x}
>>> print(most_general_unification(P(Q(x)), P(y)))
{y: Q(x)}
```

# Test unify()

```>>> print(Clause([]).unify(Clause([])))
[]
>>> print(Clause([P(x)]).unify(Clause([-P(A)])))
[{}]
>>> print(Clause([P(A), Q(x)]).unify(Clause([-P(x), R(x)])))
[{R(A), Q(A)}]
>>> print(Clause([P(A), Q(x), R(x,y)]).unify(Clause([-P(x), Q(y)])))
[{Q(y), Q(A), R(A,y)}]
>>> print(Clause([P(A), -Q(y)]).unify(Clause([-P(x), Q(B)])))
[{}]
>>> print(Clause([P(x), Q(x)]).unify(Clause([-P(A), -Q(B)])))
[{-Q(B), Q(A)}, {-P(A), P(B)}]
>>> print(Clause([P(x,x), Q(x), R(x)]).unify(Clause([-P(A,z), -Q(B)])))
[{-Q(B), Q(A), R(A)}, {-P(A,z), R(B), P(B,B)}]
```
```>>> a = clausify(read_expr('P(A)'))
>>> print(a[0].unify(b[0]))
[{P(B)}]
```

# Test is_tautology()

```>>> print(Clause([P(A), -P(A)]).is_tautology())
True
>>> print(Clause([-P(A), P(A)]).is_tautology())
True
>>> print(Clause([P(x), -P(A)]).is_tautology())
False
>>> print(Clause([Q(B), -P(A), P(A)]).is_tautology())
True
>>> print(Clause([-Q(A), P(R(A)), -P(R(A)), Q(x), -R(y)]).is_tautology())
True
>>> print(Clause([P(x), -Q(A)]).is_tautology())
False
```

# Test subsumes()

```>>> print(Clause([P(A), Q(B)]).subsumes(Clause([P(A), Q(B)])))
True
>>> print(Clause([-P(A)]).subsumes(Clause([P(A)])))
False
>>> print(Clause([P(A), Q(B)]).subsumes(Clause([Q(B), P(A)])))
True
>>> print(Clause([P(A), Q(B)]).subsumes(Clause([Q(B), R(A), P(A)])))
True
>>> print(Clause([P(A), R(A), Q(B)]).subsumes(Clause([Q(B), P(A)])))
False
>>> print(Clause([P(x)]).subsumes(Clause([P(A)])))
True
>>> print(Clause([P(A)]).subsumes(Clause([P(x)])))
True
```

# Test prove()

```>>> print(ResolutionProverCommand(read_expr('man(x)')).prove())
False
True
True
True
True
True
True
True
True
True
True
False
>>> print(ResolutionProverCommand(read_expr('-all x.some y.F(x,y) & some x.all y.(-F(x,y))')).prove())
False
False
```
```>>> p1 = read_expr('all x.(man(x) -> mortal(x))')
>>> ResolutionProverCommand(c, [p1,p2]).prove()
True
```
```>>> p1 = read_expr('all x.(man(x) -> walks(x))')
>>> ResolutionProverCommand(c, [p1,p2]).prove()
True
```
```>>> p = read_expr('some e1.some e2.(believe(e1,john,e2) & walk(e2,mary))')
>>> ResolutionProverCommand(c, [p]).prove()
True
```

# Test proof()

```>>> p1 = read_expr('all x.(man(x) -> mortal(x))')
>>> logic._counter._value = 0
>>> tp = ResolutionProverCommand(c, [p1,p2])
>>> tp.prove()
True
>>> print(tp.proof())
[1] {-mortal(Socrates)}     A
[2] {-man(z2), mortal(z2)}  A
[3] {man(Socrates)}         A
[4] {-man(Socrates)}        (1, 2)
[5] {mortal(Socrates)}      (2, 3)
[6] {}                      (1, 5)
<BLANKLINE>
```

```>>> p1 = read_expr('father_of(art,john)')
>>> p3 = read_expr('all x.all y.(father_of(x,y) -> parent_of(x,y))')
>>> logic._counter._value = 0
>>> tp = ResolutionProverCommand(None, [p1,p2,p3,c])
[<ConstantExpression art>]
>>> print(tp.proof()) # doctest: +SKIP
[1] {father_of(art,john)}                  A
[2] {father_of(bob,kim)}                   A
[3] {-father_of(z3,z4), parent_of(z3,z4)}  A
[5] {parent_of(art,john)}                  (1, 3)
[6] {parent_of(bob,kim)}                   (2, 3)
<BLANKLINE>
```
```>>> p1 = read_expr('father_of(art,john)')
>>> p3 = read_expr('all x.all y.(father_of(x,y) -> parent_of(x,y))')
>>> p4 = read_expr('all x.all y.(mother_of(x,y) -> parent_of(x,y))')
>>> logic._counter._value = 0
>>> tp = ResolutionProverCommand(None, [p1,p2,p3,p4,c])
[<ConstantExpression ann>, <ConstantExpression art>]
>>> print(tp.proof()) # doctest: +SKIP
[ 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