salmans / Razor

5 stars 0 forks source link

Incorrect model when searching with limited depth #80

Open jmoy opened 7 years ago

jmoy commented 7 years ago

I have the theory


PosA(x,y) => (UnivA(x) & UnivB(y));
PosB(y,x) => (UnivA(x) & UnivB(y));
(UnivA(x) & UnivB(x)) => Falsehood;

UnivA(x) => exists y.PosA(x,y);
UnivB(y) => exists x.PosB(y,x);

UnivA('waa);
UnivB('wab);
PosA('waa,'wab) => Falsehood;

UnivA('wba);
UnivB('wbb);
PosB('wbb,'wba) => Falsehood;

UnivA('x1);
UnivB(y) => PosA('x1,y);

UnivA('x2);
(((PosA('x2,y) & PosB(y,x)) & PosA(x,w)) & UnivA(z)) => PosB(w,z);

When solving with depth 1 Razor returns the model

Domain: {e^0, e^1, e^10, e^11, e^2, e^3, e^4, e^5, e^6, e^7, e^8, e^9}
"PosA" = {(e^0,e^6), (e^2,e^7), (e^4,e^1), (e^4,e^3), (e^4,e^6), (e^4,e^7), (e^4,e^8), (e^4,e^9), (e^5,e^9)}
"PosB" = {(e^1,e^10), (e^3,e^11)}
"UnivA" = {(e^0), (e^2), (e^4), (e^5), (e^10), (e^11)}
"UnivB" = {(e^1), (e^3), (e^6), (e^7), (e^8), (e^9)}
"waa" = {e^0}
"wab" = {e^1}
"wba" = {e^2}
"wbb" = {e^3}
"x1" = {e^4}
"x2" = {e^5}
{@Incomplete_exists0,@Incomplete_exists1}

This is incorrect since the axiom

UnivA(x) => exists y.PosA(x,y);

is not satisfied for x=e^11.