I'm reading the paper "A fixpoint semantics and an SLD-resolution calculus for modal logic programs" by L.A.Nguyen, and in the paper he asserts that certain tautologies hold, but it seems that there are counter-examples. Am I missing something, or is the paper just incorrect?
We have the logic KD5 which is a standard modal logic with additional axiom schemata (D): $\square\phi\rightarrow\phi$ and (5): $\diamond\phi\rightarrow\square\diamond\phi$. Let $\nabla$ below indicate any modal operator, $\square$ or $\diamond$.
Then in the paper it is claimed that $\nabla\nabla_1 \nabla_2\phi = \nabla_1\nabla_2\phi$. However, it seems we can construct a Kripke model satisfying KD5 but violating this claim: define worlds $w_0$,$w_1$,$w_2$,$w_3$ with accessibility relation given by $w_0\to w_1\to w_2\to w_3\to w_3$. This is a "serial" relation (every world has a reachable neighbor), so it satisfies (D). And since every world has a unique reachable neighbor, it (trivially) is a "Euclidean" relation, so it satisfies (5). This also implies that $w_0\models\square\phi\equiv\diamond\phi$ for any $\phi$, hence $w_0\models\nabla\neg\phi\equiv\neg\nabla\phi$. Now let $w_3\models\phi$ and $w_2\models\neg\phi$. Then $w_0\models\diamond\diamond\neg\phi$, hence $w_0\models\neg\diamond\diamond\phi$, but also $w_0\models\diamond\diamond\diamond\phi$. But this contradicts the claimed general relation.
There is a similar claim in the paper that $\diamond\nabla\phi\equiv\square\nabla\phi$ in KD5 with another apparent counter-example.
Your proposed counterexample does not satisfy $(5)$. Consider the valuation making $p$ true at $w_1$ and false everywhere else. Then at $w_0$, $\Diamond p$ is true but $\Box\Diamond p$ is false.
Relatedly, your claim of Euclideanness is incorrect, the issue being that the accessibility relation in your proposed counterexample is not reflexive.