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

*From*: Saswata Paul <paulsaswata1@xxxxxxxxx>*Date*: Thu, 17 Oct 2019 07:39:29 -0700 (PDT)

HI,

-- 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.

**Follow-Ups**:**Re: [tlaplus] Does Temporal Logic in TLAPS support first order logic?***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Beginner Question: Working with the Prisoners Example** - Next by Date:
**Re: [tlaplus] Does Temporal Logic in TLAPS support first order logic?** - Previous by thread:
**Re: [tlaplus] Beginner Question: Working with the Prisoners Example** - Next by thread:
**Re: [tlaplus] Does Temporal Logic in TLAPS support first order logic?** - Index(es):