feat(Logics/LTL): LTL formula type and semantics over omega-words#649

Open

benbrastmckie wants to merge 5 commits into

leanprover:mainfrom

benbrastmckie:feat/temporal-formula-propositional

Commits on Jun 16, 2026

feat(Logics/Propositional): five-primitive formula type with primitive bot

benbrastmckie
and
claude
committed

Commits on Jun 17, 2026

doc: fix docstrings for primitive bot perspective

benbrastmckie
and
claude
committed
feat(Logics/Temporal): temporal formula type with propositional structure

benbrastmckie
and
claude
committed

Commits on Jun 18, 2026

task 233 phase 1-3: revise PR #649 to LTL-only with standard notation
benbrastmckie
committed

Commits on Jun 19, 2026

fix(LTL): use ωSequence State for satisfaction, fix docstrings

benbrastmckie
and
claude
committed