I would like to use First Order Logic to express that two people are brothers when they are two different persons (two IDs of my database) who share both surnames, but not the first names. This is because occassionally I may have two records in my database with different ID but actually correspond to the same person. I am using the FOL Python code of the Artificial Intelligence: a Modern Approach (AIMA) from here and here. My clause looks like:
(everything here are variables, no constants)
my_clause = "BROTHERS(id1, id2) ==> SURNAME1(id1, x) & SURNAME1(id2, x) & SURNAME2(id1, y) & SURNAME2(id2, y) & ~(NAME(id1, z) & NAME(id2, z))"
When I do
kb = aima.logic.FolKB([aima.utils.expr(myclause)])
I am getting the error "Not a definite clause", I guess due to the ~ (negation) operator. If the antecedent is composed of positive sentences only, then it works fine, so I am not sure how I should transform this to be compliant with a definite clause and express what I need.
I am aware of the common transformations (CNF, Skolemization, ...) but they are not needed here as they are done internally (that's why it accepts an implication in the statement).