#NEWLINE# def testResolutionProver( ) : #NEWLINE# #INDENT# resolution_test ( 'man(x)' ) #NEWLINE# resolution_test ( '(man(x) -> man(x))' ) #NEWLINE# resolution_test ( '(man(x) -> --man(x))' ) #NEWLINE# resolution_test ( '-(man(x) and -man(x))' ) #NEWLINE# resolution_test ( '(man(x) or -man(x))' ) #NEWLINE# resolution_test ( '(man(x) -> man(x))' ) #NEWLINE# resolution_test ( '-(man(x) and -man(x))' ) #NEWLINE# resolution_test ( '(man(x) or -man(x))' ) #NEWLINE# resolution_test ( '(man(x) -> man(x))' ) #NEWLINE# resolution_test ( '(man(x) iff man(x))' ) #NEWLINE# resolution_test ( '-(man(x) iff -man(x))' ) #NEWLINE# resolution_test ( 'all x.man(x)' ) #NEWLINE# resolution_test ( '-all x.some y.F(x,y) & some x.all y.(-F(x,y))' ) #NEWLINE# resolution_test ( 'some x.all y.sees(x,y)' ) #NEWLINE# p1 = Expression . fromstring ( 'all x.(man(x) -> mortal(x))' ) #NEWLINE# p2 = Expression . fromstring ( 'man(Socrates)' ) #NEWLINE# c = Expression . fromstring ( 'mortal(Socrates)' ) #NEWLINE# print ( ( '%s, %s |- %s: %s' % ( p1 , p2 , c , ResolutionProver ( ) . prove ( c , [ p1 , p2 ] ) ) ) ) #NEWLINE# p1 = Expression . fromstring ( 'all x.(man(x) -> walks(x))' ) #NEWLINE# p2 = Expression . fromstring ( 'man(John)' ) #NEWLINE# c = Expression . fromstring ( 'some y.walks(y)' ) #NEWLINE# print ( ( '%s, %s |- %s: %s' % ( p1 , p2 , c , ResolutionProver ( ) . prove ( c , [ p1 , p2 ] ) ) ) ) #NEWLINE# p = Expression . fromstring ( 'some e1.some e2.(believe(e1,john,e2) & walk(e2,mary))' ) #NEWLINE# c = Expression . fromstring ( 'some e0.walk(e0,mary)' ) #NEWLINE# print ( ( '%s |- %s: %s' % ( p , c , ResolutionProver ( ) . prove ( c , [ p ] ) ) ) )