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

Re: [tlaplus] Curious oddity

Thus, your formula is valid if x and y are declared as CONSTANTS, but not if at least one of them is a VARIABLE.

But in a system independant of TLAPLUS? For example if LTL is built upon FOL, the individual variables declared by FOL and that can
be quantified are what: state variables or something else?