Results on the propositional \(\mu\)-calculus (Q801893)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Results on the propositional \(\mu\)-calculus |
scientific article |
Statements
Results on the propositional \(\mu\)-calculus (English)
0 references
1983
0 references
In this paper we define and study a propositional \(\mu\)-calculus \(L\mu\), which consists essentially of propositional modal logic with a least fixpoint operator. \(L\mu\) is syntactically simpler yet strictly more expressive than Propositional Dynamic Logic (PDL). For a restricted version we give an exponential-time decision procedure, small model property, and complete deductive system, thereby subsuming the corresponding results for PDL.
0 references
fixed point induction
0 references
completeness
0 references
propositional mu-calculus
0 references
propositional modal logic
0 references
decision procedure
0 references
small model property
0 references
PDL
0 references
