Cyclic proofs for the first-order mu-calculus

• We introduce a path-based cyclic proof system for first-order mu-calculus, the extension of first-order logic by second-order quantifiers for least and greatest fixed points of definable monotone functions. We prove soundness of the system and demonstrate it to be as expressive as the known trace-based cyclic systems of Dam and Sprenger. Furthermore, we establish cut-free completeness of our system for the fragment corresponding to the modal mu-calculus.

Ämnesord

NATURVETENSKAP  -- Matematik (hsv//swe)

NATURAL SCIENCES  -- Mathematics (hsv//eng)

NATURVETENSKAP  -- Matematik -- Algebra och logik (hsv//swe)

NATURAL SCIENCES  -- Mathematics -- Algebra and Logic (hsv//eng)

Nyckelord

Cyclic proofs

first-order mu-calculus

modal mu-calculus

sequent

calculus

completeness

sequent calculi

induction

Mathematics

Science & Technology - Other Topics

Cyclic proofs

Publikations- och innehållstyp

ref (ämneskategori)

art (ämneskategori)