Hello,
I am very new, started yesterday, to HOL (in fact to theorem
proving itself). I was looking forward to use the Temporal logic
theory in HOL4, but I have a problem:
The definition of NEXT |- !P. NEXT P = \t. P (SUC t) seems a bit
odd.
According to LTL, M |= NEXT P, iff P |= s1, where s1 is the
first state in the linear path $\pi$. But, in the definition of
NEXT (in Temporal logic theory of HOL4), the "t", which I am
guessing stands for the time step (or some state in path $\pi$)
is unconstrained, i.e., if I apply NEXT P to any state sN, it
says that the successor state (sN+1) has to satisfy the
proposition P. This might look correct on a cursory glance, but,
NEXT P is only satisfied on the state s1 of the path, i.e., in
\t. P(SUC t). "t" needs to be constrained to be the very first
time-step "t0", else, to my possibly ignorant eyes, it looks
dodgy.
Please, correct me, since I don't know anything about HOL and
how this theory is being satisfied.
--
Regards,
Avinash Malik,
Department of Electrical and Computer Engineering,
University of Auckland,
NZ
------------------------------------------------------------------------------
Learn the latest--Visual Studio 2012, SharePoint 2013, SQL 2012, more!
Discover the easy way to master current and previous Microsoft technologies
and advance your career. Get an incredible 1,500+ hours of step-by-step
tutorial videos with LearnDevNow. Subscribe today and save!
http://pubads.g.doubleclick.net/gampad/clk?id=58040911&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
