Reasoner for Aconjunctive Fragment decides formula incorrectly
The following nearly identical formulas are both unsatisfiable (even in the classical sense), but COOL's reasoner for the aconjunctive fragment classifies the second formula as satisfiable.
f1 := ~(( ( νx.µy. ((q1 => []x) & (q2 => []y)) ) <=> ( νx.µy. ((q1 => []x) & (q2 => []y)) ) ))
f2 := ~(( ( νx.µy. ((q1 => []y) & (q2 => []x)) ) <=> ( νx.µy. ((q1 => []y) & (q2 => []x)) ) ))
COOL (f1
):
$ cool-coalg sat K --fragment altfreeaconj <<< "~(( ( νx.µy. ((q1 => []x) & (q2 => []y)) ) <=> ( νx.µy. ((q1 => []x) & (q2 => []y)) ) ))"
Formula 1:
Both onestep and tableau implementation available
unsatisfiable
COOL (f2
):
$ cool-coalg sat K --fragment altfreeaconj <<< "~(( ( νx.µy. ((q1 => []y) & (q2 => []x)) ) <=> ( νx.µy. ((q1 => []y) & (q2 => []x)) ) ))"
Formula 1:
Both onestep and tableau implementation available
satisfiable
Their NNFs, which are the formulas the reasoner actually works on, are identical, except for the order of appearance of fixpoint literals:
NNF (f1
):
(νx.(μw.(~(q1) | [ ](x)) & (~(q2) | [ ](w)))) & (μy.(νz.q1 & < >(y) | q2 & < >(z))) | (νy.(μz.(~(q1) | [ ](y)) & (~(q2) | [ ](z)))) & (μx.(νw.q1 & < >(x) | q2 & < >(w)))
NNF (f2
):
(νx.(μw.(~(q1) | [ ](w)) & (~(q2) | [ ](x)))) & (μy.(νz.q1 & < >(z) | q2 & < >(y))) | (νy.(μz.(~(q1) | [ ](z)) & (~(q2) | [ ](y)))) & (μx.(νw.q1 & < >(w) | q2 & < >(x)))
The second formula is decided wrongly only by the permutation-game reasoner; the more general Safra-tree-based reasoner correctly classifies both as unsatisfiable.