Talk:Hennessy–Milner logic

Work in progress

I'm short on time right now but I will continue this article in a few days. Claim 12:20, 17 August 2007 (UTC)

wait how do they derive negation from only these??? 128.200.83.67 (talk) 18:22, 20 November 2009 (UTC)

the following equivalences hold

$\phi \equiv \phi \wedge tt\equiv \neg (\neg tt\vee \neg \phi )\equiv \neg \neg \phi$

${<}a{>}\phi \equiv \neg {[}a{]}\neg \phi$

but you are right, it is not clear how to derive it from this set.

$\neg \phi \equiv \phi \implies ff\equiv \neg \phi \vee ff\equiv \neg (\phi \wedge \neg ff)\equiv \neg (\phi \wedge tt)\equiv ???$

it should be possible to derive negation, but not clear enough. Because $[\tau ]\phi$ where $\tau$, an invisible action may be needed. But I am not sure of that. I suppose it is possible, because I saw the same definition in some articles, but assumptions like $\phi \equiv [a]\phi$ may be required, and I am not sure if it can be correct.

there is no problem if negation is introduced as it is also seen in several articles.

I am as busy as Claim was when starting this article, but I will do the needed changes when I can, and when I know more about this logic.

by now I will only fix the syntax! — Preceding unsigned comment added by 189.178.41.71 (talk) 15:41, 1 June 2013 (UTC)