Resolution Theorem Prover

  
>>> from nltk.inference import inference
>>> from nltk.sem import logic
>>> from nltk.sem.logic import *
>>> from nltk.inference.nonmonotonic import *
>>> logic._counter._value = 0
>>> lp = LogicParser()

1
   Closed Domain Assumption

  
>>> p1 = lp.parse(r'all x.(man(x) -> mortal(x))')
>>> p2 = lp.parse(r'man(Socrates)')
>>> c = lp.parse(r'mortal(Socrates)')
>>> prover = inference.get_prover(c, [p1,p2])
>>> prover.prove()
True
>>> cdp = ClosedDomainProver(prover)
>>> for a in cdp.assumptions(): print a
man(Socrates)
(man(Socrates) -> mortal(Socrates))
>>> cdp.prove()
True
  
>>> p1 = lp.parse(r'exists x.walk(x)')
>>> p2 = lp.parse(r'man(Socrates)')
>>> c = lp.parse(r'walk(Socrates)')
>>> prover = inference.get_prover(c, [p1,p2])
>>> prover.prove()
False
>>> cdp = ClosedDomainProver(prover)
>>> for a in cdp.assumptions(): print a
walk(Socrates)
man(Socrates)
>>> cdp.prove()
True
  
>>> p1 = lp.parse(r'exists x.walk(x)')
>>> p2 = lp.parse(r'man(Socrates)')
>>> p3 = lp.parse(r'man(Bill)')
>>> c = lp.parse(r'walk(Socrates)')
>>> prover = inference.get_prover(c, [p1,p2,p3])
>>> prover.prove()
False
>>> cdp = ClosedDomainProver(prover)
>>> for a in cdp.assumptions(): print a
man(Socrates)
(walk(Socrates) | walk(Bill))
man(Bill)
>>> cdp.prove()
False

2   Unique Names Assumption

  
>>> p1 = lp.parse(r'all x.(man(x) -> mortal(x))')
>>> p2 = lp.parse(r'man(Socrates)')
>>> c = lp.parse(r'mortal(Socrates)')
>>> prover = inference.get_prover(c, [p1,p2])
>>> prover.prove()
True
>>> unp = UniqueNamesProver(prover)
>>> for a in unp.assumptions(): print a
all x.(man(x) -> mortal(x))
man(Socrates)
>>> unp.prove()
True
  
>>> p1 = lp.parse(r'man(Socrates)')
>>> p2 = lp.parse(r'man(Bill)')
>>> c = lp.parse(r'exists x.exists y.-(x = y)')
>>> prover = inference.get_prover(c, [p1,p2])
>>> prover.prove()
False
>>> unp = UniqueNamesProver(prover)
>>> for a in unp.assumptions(): print a
man(Socrates)
man(Bill)
-(Bill = Socrates)
>>> unp.prove()
True
  
>>> p1 = lp.parse(r'all x.(walk(x) -> (x = Socrates))')
>>> p2 = lp.parse(r'Bill = William')
>>> p3 = lp.parse(r'Bill = Billy')
>>> c = lp.parse(r'-walk(William)')
>>> prover = inference.get_prover(c, [p1,p2,p3])
>>> prover.prove()
False
>>> unp = UniqueNamesProver(prover)
>>> for a in unp.assumptions(): print a
all x.(walk(x) -> (x = Socrates))
(Bill = William)
(Bill = Billy)
-(Bill = Socrates)
-(Billy = Socrates)
-(Socrates = William)
>>> unp.prove()
True

3   Closed World Assumption

  
>>> p1 = lp.parse(r'walk(Socrates)')
>>> p2 = lp.parse(r'-(Socrates = Bill)')
>>> c = lp.parse(r'-walk(Bill)')
>>> prover = inference.get_prover(c, [p1,p2])
>>> prover.prove()
False
>>> cwp = ClosedWorldProver(prover)
>>> for a in cwp.assumptions(): print a
walk(Socrates)
-(Socrates = Bill)
all z1.(walk(z1) -> (z1 = Socrates))
>>> cwp.prove()
True
  
>>> p1 = lp.parse(r'see(Socrates, John)')
>>> p2 = lp.parse(r'see(John, Mary)')
>>> p3 = lp.parse(r'-(Socrates = John)')
>>> p4 = lp.parse(r'-(John = Mary)')
>>> c = lp.parse(r'-see(Socrates, Mary)')
>>> prover = inference.get_prover(c, [p1,p2,p3,p4])
>>> prover.prove()
False
>>> cwp = ClosedWorldProver(prover)
>>> for a in cwp.assumptions(): print a
see(Socrates,John)
see(John,Mary)
-(Socrates = John)
-(John = Mary)
all z3.all z4.(see(z3,z4) -> (((z3 = Socrates) & (z4 = John)) | ((z3 = John) & (z4 = Mary))))
>>> cwp.prove()
True
  
>>> p1 = lp.parse(r'all x.(ostrich(x) -> bird(x))')
>>> p2 = lp.parse(r'bird(Tweety)')
>>> p3 = lp.parse(r'-ostrich(Sam)')
>>> p4 = lp.parse(r'Sam != Tweety')
>>> c = lp.parse(r'-bird(Sam)')
>>> prover = inference.get_prover(c, [p1,p2,p3,p4])
>>> prover.prove()
False
>>> cwp = ClosedWorldProver(prover)
>>> for a in cwp.assumptions(): print a
all x.(ostrich(x) -> bird(x))
bird(Tweety)
-ostrich(Sam)
-(Sam = Tweety)
all z7.(bird(z7) -> ((z7 = Tweety) | ostrich(z7)))
>>> print cwp.prove()
True

4   Multi-Decorator Example

  
>>> p1 = lp.parse(r'see(Socrates, John)')
>>> p2 = lp.parse(r'see(John, Mary)')
>>> c = lp.parse(r'-see(Socrates, Mary)')
>>> prover = inference.get_prover(c, [p1,p2])
>>> print prover.prove()
False
>>> cmd = ClosedDomainProver(UniqueNamesProver(ClosedWorldProver(prover)))
>>> print cmd.prove()
True