A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic

05/15/2019
by   Simon Docherty, et al.
0

We define a infinitary labelled sequent calculus for PDL, G3PDL^∞. A finitarily representable cyclic system, G3PDL^ω, is then given. We show that both are sound and complete with respect to standard models of PDL and, further, that G3PDL^∞ is cut-free complete. We additionally investigate proof-search strategies in the cyclic system for the fragment of PDL without tests.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset

Sign in with Google

×

Use your Google Account to sign in to DeepAI

×

Consider DeepAI Pro