#NEWLINE# def unique_names_demo( ) : #NEWLINE# #INDENT# lexpr = Expression . fromstring #NEWLINE# p1 = lexpr ( 'man(Socrates)' ) #NEWLINE# p2 = lexpr ( 'man(Bill)' ) #NEWLINE# c = lexpr ( 'exists x.exists y.(x != y)' ) #NEWLINE# prover = Prover9Command ( c , [ p1 , p2 ] ) #NEWLINE# print ( prover . prove ( ) ) #NEWLINE# unp = UniqueNamesProver ( prover ) #NEWLINE# print ( 'assumptions:' ) #NEWLINE# for a in unp . assumptions ( ) : #NEWLINE# #INDENT# print ( '   ' , a ) #NEWLINE# #UNINDENT# print ( 'goal:' , unp . goal ( ) ) #NEWLINE# print ( unp . prove ( ) ) #NEWLINE# p1 = lexpr ( 'all x.(walk(x) -> (x = Socrates))' ) #NEWLINE# p2 = lexpr ( 'Bill = William' ) #NEWLINE# p3 = lexpr ( 'Bill = Billy' ) #NEWLINE# c = lexpr ( '-walk(William)' ) #NEWLINE# prover = Prover9Command ( c , [ p1 , p2 , p3 ] ) #NEWLINE# print ( prover . prove ( ) ) #NEWLINE# unp = UniqueNamesProver ( prover ) #NEWLINE# print ( 'assumptions:' ) #NEWLINE# for a in unp . assumptions ( ) : #NEWLINE# #INDENT# print ( '   ' , a ) #NEWLINE# #UNINDENT# print ( 'goal:' , unp . goal ( ) ) #NEWLINE# print ( unp . prove ( ) )