#NEWLINE# def closed_domain_demo( ) : #NEWLINE# #INDENT# lexpr = Expression . fromstring #NEWLINE# p1 = lexpr ( 'exists x.walk(x)' ) #NEWLINE# p2 = lexpr ( 'man(Socrates)' ) #NEWLINE# c = lexpr ( 'walk(Socrates)' ) #NEWLINE# prover = Prover9Command ( c , [ p1 , p2 ] ) #NEWLINE# print ( prover . prove ( ) ) #NEWLINE# cdp = ClosedDomainProver ( prover ) #NEWLINE# print ( 'assumptions:' ) #NEWLINE# for a in cdp . assumptions ( ) : #NEWLINE# #INDENT# print ( '   ' , a ) #NEWLINE# #UNINDENT# print ( 'goal:' , cdp . goal ( ) ) #NEWLINE# print ( cdp . prove ( ) ) #NEWLINE# p1 = lexpr ( 'exists x.walk(x)' ) #NEWLINE# p2 = lexpr ( 'man(Socrates)' ) #NEWLINE# p3 = lexpr ( '-walk(Bill)' ) #NEWLINE# c = lexpr ( 'walk(Socrates)' ) #NEWLINE# prover = Prover9Command ( c , [ p1 , p2 , p3 ] ) #NEWLINE# print ( prover . prove ( ) ) #NEWLINE# cdp = ClosedDomainProver ( prover ) #NEWLINE# print ( 'assumptions:' ) #NEWLINE# for a in cdp . assumptions ( ) : #NEWLINE# #INDENT# print ( '   ' , a ) #NEWLINE# #UNINDENT# print ( 'goal:' , cdp . goal ( ) ) #NEWLINE# print ( cdp . prove ( ) ) #NEWLINE# p1 = lexpr ( 'exists x.walk(x)' ) #NEWLINE# p2 = lexpr ( 'man(Socrates)' ) #NEWLINE# p3 = lexpr ( '-walk(Bill)' ) #NEWLINE# c = lexpr ( 'walk(Socrates)' ) #NEWLINE# prover = Prover9Command ( c , [ p1 , p2 , p3 ] ) #NEWLINE# print ( prover . prove ( ) ) #NEWLINE# cdp = ClosedDomainProver ( prover ) #NEWLINE# print ( 'assumptions:' ) #NEWLINE# for a in cdp . assumptions ( ) : #NEWLINE# #INDENT# print ( '   ' , a ) #NEWLINE# #UNINDENT# print ( 'goal:' , cdp . goal ( ) ) #NEWLINE# print ( cdp . prove ( ) ) #NEWLINE# p1 = lexpr ( 'walk(Socrates)' ) #NEWLINE# p2 = lexpr ( 'walk(Bill)' ) #NEWLINE# c = lexpr ( 'all x.walk(x)' ) #NEWLINE# prover = Prover9Command ( c , [ p1 , p2 ] ) #NEWLINE# print ( prover . prove ( ) ) #NEWLINE# cdp = ClosedDomainProver ( prover ) #NEWLINE# print ( 'assumptions:' ) #NEWLINE# for a in cdp . assumptions ( ) : #NEWLINE# #INDENT# print ( '   ' , a ) #NEWLINE# #UNINDENT# print ( 'goal:' , cdp . goal ( ) ) #NEWLINE# print ( cdp . prove ( ) ) #NEWLINE# p1 = lexpr ( 'girl(mary)' ) #NEWLINE# p2 = lexpr ( 'dog(rover)' ) #NEWLINE# p3 = lexpr ( 'all x.(girl(x) -> -dog(x))' ) #NEWLINE# p4 = lexpr ( 'all x.(dog(x) -> -girl(x))' ) #NEWLINE# p5 = lexpr ( 'chase(mary, rover)' ) #NEWLINE# c = lexpr ( 'exists y.(dog(y) & all x.(girl(x) -> chase(x,y)))' ) #NEWLINE# prover = Prover9Command ( c , [ p1 , p2 , p3 , p4 , p5 ] ) #NEWLINE# print ( prover . prove ( ) ) #NEWLINE# cdp = ClosedDomainProver ( prover ) #NEWLINE# print ( 'assumptions:' ) #NEWLINE# for a in cdp . assumptions ( ) : #NEWLINE# #INDENT# print ( '   ' , a ) #NEWLINE# #UNINDENT# print ( 'goal:' , cdp . goal ( ) ) #NEWLINE# print ( cdp . prove ( ) )