I need to find a proof for my goal , given some assumptions. The assumptions and the goal were translated from english sentences.
John ,Mary,Helen,George are the only members of club1:
-Member(Club1,John) ∧ Member(Club1,Mary) ∧ -Member(Club1,Helen) ∧ Member(Club1,George)
John is Mary's husband.
George is Helen's brother.
The husband or the wife of each person is also a part of the same club
- (∀x)(∀y)(∀s)(Married(x,y) & Member(s,x) → Member(s,y))
Helen is not married.
With common logic we can prove that helen (being ethical and not incest) , is not married. But the above assumptions , can't prove my goal with propotitional logic. I need to add my own assumptions , so that I can prove my goal. What assumptions should I add to my KB to prove φ.
I tried the following ones , but they are not enough:
(∀x)(∀y)(Siblings(x,y) -> -Married(x,y)). (∀x)(∀y)(∀z)( Married(x,y) -> -Married(x,z) & -Married(y,z)).
The above assumptions , tells that if two atoms are siblings then they can't be marry each other and if they can't marry more than one person. I am using prover9 , to also prove my goal , but I can't find what else does it need , to prove it.
EDIT 1 So , far , what I have done enter image description here