Propositional KLM Logic P

This is a prover for KLM ( Kraus, Lehmann and Magidor ) logic P as defined in:
L Gordano, V Gliozzi, N Olivetti, G Pozzato
"Analytic tableaux for KLM Preferential and Cummulative Logic"
Proceedings of LPAR 2005 LNAI 3835:666-681, Springer, 2005.

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 it is not a theorem because the tableau for ~ A is open.

Results
Query
Info