Also known as Weak S5 (WS5) because it lacks reflexivity, this logic is often used as the basis of logics of agents where []p means "the agent knows p" or "the agent believes p".

When you enter a formula A, then "closed" means that A is a theorem because the tableau for ~ A

is closed, and "open" means that A is not a theorem because the tableau for ~ A is open.

Prover for modal logic KD45.

Based on:

Efficient Loop-Check for KD45 Logic

A Birstunas

Lithuanian Mathematics Journal 46(1):44-53 2006.

Author: Rajeev Gore 01 November 2007 (Copyright).