[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Does Temporal Logic in TLAPS support first order logic?


    I have been learning temporal logic with TLAPS. 

    I noticed that in TLAPS, if we have \A x \in SomeSet : <> <<A(x)>>_vars => <> <<B(x)>>_vars and <> <<A(x)>>_vars in the assumption base and try to prove <> <<B(x)>>_vars from it, the prover fails. 

    However, we can prove  B(x) from \A x \in SomeSet : A(x) => B(x) and A(x).

    Since I have no prior experience with temporal logic, I was wondering whether this is a limitation of temporal logic itself (if it is, then why?) or a limitation of TLAPS.

    Any clarification will be appreciated.

Thank you

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/57b23d4e-d771-4e5d-acd1-cc61b5b15000%40googlegroups.com.