Gentzen-type axiomatization for PAL

The aim of propositional algorithmic logic (PAL) is to investigate the properties of simple nondeterministic while-program schemes on propositional level. We present finite, cut-free, Gentzen-type axiomatization of PAL. As a corollary from completeness theorem, we obtain the small-model theorem and algorithm for checking the validity of PAL formulas.

Authors

• Igor Walukiewicz

Keywords

No keywords are indexed for this paper.