Fixed-point of functions
- Tower induction for coinduction
categorize everything?
fixedpoint logics
- godel-lob logic (Daniela)
- modal mu-calculus
- mu LJ
- mu LL
- mu CLP, HFL
- LID
Observation: often formalized in sequent calculus instead of natural deduction (as seen in type theory)
Natural deduction
- guarded type theory
we can see no more circular reasoning, not because it doesn’t but we currently do not know how do it think
Parity / Games / Automata
- to show decidability (of mu-calculus) we often rely on automata
- the parity condition of automata, is related to the
mu-nunotion in mu-calculus- Buchi:
nu x. mu y. ... - decide the parity index of a language ⇐> what is the nesting of the formula (algorithmic, by reducing it to the parity game)
- keyword: typeness
- Buchi:
- Games for the µ-calculus. Niwinski & Walukiewicz. TCS 163(1&2):99-116 (1996)
- There is a recent book draft explained better
- better suited for infinite systems
- cyclic proofs
Expressivity