Abstract

When analysing a logic, one property of interest is its’ completeness. A logic is complete iff every valid formula is provable, and by proof we mean every formula is derivable from a deductive system which comprises axioms and rules of inference.

In 1983 Kozen presented $\mu$-calculus in the form we know it today and gave a complete deductive system for a restricted version. It wasn’t until 1995 when Walukiewicz proved completeness for the full language with a stronger deductive system then with Kozen’s original axiomatization in 2000. In this report, we present an implementation of Walukiewicz original proof procedure.

Report

The full report can be found here.

Examples

Note, some of these images are extremely large and may not display properly within a web browser, use an image viewer such as FEH.

Formula Tableau Automaton Unwinding Assignment
$\mu X_0. (p_0 \land \neg p_0) \lor \langle a_0 \rangle X_0$ view view view view
$\mu X_0. (p_1) \land (\langle a_0 \rangle ((\langle a1 \rangle (((X_0) \lor (X_0)) \lor (p_0))) \land (\langle a_0 \rangle (X_0))))$ view view view view
$\nu X_0. \mu X_1. \nu X_2. \nu X_3. (\langle a1 \rangle (\langle a_1 \rangle (X_1))) \land ((\langle a1 \rangle([a_1] (((p_1) \langle ((p_1) \lor ((X_1) \lor (X_2)))) \land (p_0)))) \lor ((\langle a0 \rangle (X_0)) \land ((p_1) \land (\langle a0 \rangle(X_3)))))$ view view view view
$\mu X_0. \mu X_1. \nu X_2. \langle a_0 \rangle(([a_1] (((X_1) \land (X_0)) \land (X_1))) \land (([a_1] (X_2)) \land (\langle a_1 \rangle(X_0))))$ view view view view