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

[tlaplus] Is there a decision procedure for telling whether a spec is machine-closed?

From: Andrew Helwer <andrew.helwer@xxxxxxxxx>
Date: Mon, 16 Dec 2024 07:02:43 -0800 (PST)

Like it takes as parameters the formulas S and L and it determines whether their conjunction is machine-closed; or is such a problem undecidable?

Andrew

--
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 visit https://groups.google.com/d/msgid/tlaplus/2ff9a5af-baff-4382-81c9-3328f746e57dn%40googlegroups.com.

Follow-Ups:
- Re: [tlaplus] Is there a decision procedure for telling whether a spec is machine-closed?
  - From: Stephan Merz
- [tlaplus] Re: Is there a decision procedure for telling whether a spec is machine-closed?
  - From: Andrew Helwer

Prev by Date: [tlaplus] 1st CFP CONCUR 2025
Next by Date: [tlaplus] What's the difference between `-simulate` and `-generate`?
Previous by thread: [tlaplus] 1st CFP CONCUR 2025
Next by thread: [tlaplus] Re: Is there a decision procedure for telling whether a spec is machine-closed?
Index(es):
- Date
- Thread