Toot

Written by Andrew Helwer on 2025-01-12 at 22:50

@jarrodu it's from page 102 of A Science of Concurrent Programs by Leslie Lamport (https://lamport.azurewebsites.net/tla/science-book.html).

It's an example of how to prove a statement in temporal logic, specifically a "leads to" statement where saying that P leads to Q is denoted P ↝ Q. Other important operators are always (□) and eventually (◇).

=> More informations about this toot | View the thread | More toots from ahelwer@discuss.systems

Mentions

=> View jarrodu@social.tchncs.de profile

Tags