Hi, I saw how the new LTL formalization (in `examples/logic/ltl`) by Simon Jantsch suddenly appeared in the past months and because more and more complete also with help of HOL maintainers. But there’s already an older LTL formalization (in `src/temporal`) since long time ago, done by Klaus Schneider et al. [1]
My first question: is there a paper (in PDF, published or unpublished)
documenting the work in `examples/logic/ltl` so that I can learn beside looking
at raw HOL scripts?
Second question: regarding the difference between two versions of LTL
formalizations, can I say the work in `examples/logic/ltl` is a *deep*
embedding? (because it has to define the LTL syntax by a datatype:
val _ = Datatype`
ltl_frml
= VAR 'a
| N_VAR 'a
| DISJ ltl_frml ltl_frml
| CONJ ltl_frml ltl_frml
| X ltl_frml
| U ltl_frml ltl_frml
| R ltl_frml ltl_frml`;
)
while the work in `src/temporal` is *shallow* embedding? (because it
embeds LTL term into HOL as ``:num -> bool`` without using any datatype)
and if so, what’s the pros and cons for choosing one of them as a
working basis (for proving further results)?
Third question: is there a way to connect the two versions of LTL, so that LTL
theorems proved from one side can be (somehow) automatically translated into
theorems on the other side?
Regards,
Chun
[1] Schneider, K., Hoffmann, D.W.: A HOL Conversion for Translating Linear Time
Temporal Logic to ω-Automata. In: Bassiliades, N., Gottlob, G., Sadri, F.,
Paschke, A., and Roman, D. (eds.) LNCS 9202 - Rule Technologies: Foundations,
Tools, and Applications. pp. 255–272. Springer Berlin Heidelberg, Berlin,
Heidelberg (1999).
signature.asc
Description: Message signed with OpenPGP
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
