Stream: Beginner Questions

Topic: Syntactic Sugar for a Logic

view this post on Zulip Zili Wang (Jan 05 2025 at 12:41):

Hello, I am working on a formalization of a variant of linear temporal logic, and saw this LTL entry: https://www.isa-afp.org/sessions/ltl/#LTL
I was wondering how the syntactic sugar in this file works. In particular, how are each of the weights on the operators derived?

view this post on Zulip Mathias Fleury (Jan 05 2025 at 17:31):

I am not aware of any proper system. The question to ask yourself is: when I have several layers, how should it be parsed in the following (not LTL syntax)?

A |= not i and j Until C or D

This gives a relative order of the priority of the operations

view this post on Zulip Mathias Fleury (Jan 05 2025 at 17:33):

Starting around 70 or 80 is usually a good idea.

Last updated: Feb 01 2025 at 20:19 UTC