Email Gateway (Aug 18 2022 at 10:01): Email Gateway (Aug 18 2022 at 10:01):From: Gabriele Pozzani <gabriele.pozzani@gmail.com>
Hello everybody,
in IOA logic I want to demonstrate:
a: "prob((%e. (L (SOME i. (L i e)) e)) ~> Q, q)"
knowing:
g: "FORALL i::nat. prob (%e. (L i e) ~> Q, q)"
where "~>" is the Leadsto operator of TLS, the temporal logic of step
developed in Muller's PhD thesis.
L and Q are predicates of type " 'a Seq => bool ", while prob is a function
of type " ('a Seq => bool) x fraction => bool ".
Knowing from "g" that the result is true for every natural number I'm not
able to demonstrate "a", but I think it's correct because "(SOME i. (L i
e))" is just a particular natural number.
I tried using spec theorem but it don't work.
Can someone help me?
Thanks
Gabriele Pozzani
Email Gateway (Aug 18 2022 at 10:01):From: Tjark Weber <tjark.weber@gmx.de>
Gabriele,
I'm not familiar with the IOA theory, but it seems the problem is that
"SOME i. L i e"
is a particular natural number only after e has been fixed. In your
assumption g however, i is quantified at the outermost level, and hence may
not depend on e.
One possible solution is to modify your assumption g:
g': "ALL (i'::('a Seq => bool)=>nat). prob (%e. (L (i' e) e) ~> Q, q)"
Now you can instantiate i' in g' with "%e. SOME i. L i e" to show a.
Best,
Tjark
Email Gateway (Aug 18 2022 at 10:01):From: Gabriele Pozzani <gabriele.pozzani@gmail.com>
Hello,
I'm not familiar with the IOA theory, but it seems the problem is that
"SOME i. L i e"
is a particular natural number only after e has been fixed. In your
assumption g however, i is quantified at the outermost level, and hence
may
not depend on e.
Yes, probably the problem is here!
One possible solution is to modify your assumption g:
g': "ALL (i'::('a Seq => bool)=>nat). prob (%e. (L (i' e) e) ~> Q, q)"
Now you can instantiate i' in g' with "%e. SOME i. L i e" to show a.
Ok, thank you very much for your help.
Bests
Gabriele
Last updated: May 03 2024 at 08:18 UTC