On the Decidability of Propositional Algorithmic Logic

✍ Scribed by Bogdan S. Chlebus

• Publisher: John Wiley and Sons
• Year: 1982
• Tongue: English
• Weight: 802 KB
• Volume: 28
• Category: Article
• ISSN: 0044-3050
• DOI: 10.1002/malq.19820281409

✦ Synopsis

ON THE DECIDABILITY OF PROPOSITIONAL ALGORITHMIC LOGIC by BOGDAN S. CHLEBIJS in Warsaw (Po1and)l) 0. Introduction Let PAL be a n abbreviation for propositional algorithmic logic. The investigation of PAL is a continuation of earlier works on algorithmic logic (GRABOWSKI [3], KRECZMAR [5], SALWICKI [7]). PAL is a formal system in which formulas and programs can be build out of propositional and program variables and logical and program connectives. The connectives are the same as in algorithmic logic. So this system may be called a propositional part of algorithmic logic. The semantics of PAL is similar to the semantics of PDL (see FISCHER, LADNER [Z], HAREL, MEYER, PRATT [4],

PRATT [6] for an exposition of dynamic logic), but in models for PAL programs are interpreted deterministically. This enables us to introduce certain methods of constructing models for PAL. One of them is based on the notion of a consistency property and can he used in constructing models of a set of formulas (CHLEBUS [l]). This notion is borrowed from the model theory of infinitary logic. I n this paper we describe and use another method. It belongs to proof theory and uses the notion of a tree of sequents of formulas as a basic tool. It can be helpful in constructing a model of a given formula. A decihion method described here is based on a suitable Gentzen-type axiomatization of PAL. This axiomatization is finitary and a n algorithm can be find which decides wheather a given formula has a proof or not. VALIEV [8] has sketched a completeness proof for deterministic PDL.