Browse Prior Art Database

The Deducibility Problem in Propositional Dynamic Logic

IP.com Disclosure Number: IPCOM000128136D
Original Publication Date: 1981-Dec-31
Included in the Prior Art Database: 2005-Sep-15
Document File: 8 page(s) / 27K

Publishing Venue

Software Patent Institute

Related People

Albert R. Meyer: AUTHOR [+5]

Abstract

Propositional Dynamic Logic (PDI.) [I] is an extension of propositional logic in which "before-after" assertions aboutthe behavior of reguhu program scheims can be made directly. Propositional 01CUIUS, temporal logic and the most fanifliar versions of propositional modal logic are all ernbeddable in PDL, but PDL nevertheless has a validity problem decidable in (deterministic) exponential time [4].

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 19% of the total text.

Page 1 of 8

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

The Deducibility Problem in Propositional Dynamic Logic

by Albert R. Meyer and Robert S. Streett and Grazina Mirkowska

Laboratory fo r Computer Science Massiichusetts Institute ofTcchnology Cambridge, Massachusetts USA

Institute of Mathematics Warsaw University Warsaw, Poland

January 13, 1981

Abstract: The problem of whether an arbitrary formula of Propositional Dynamic Logic (PDI,) is deducible from a fixed axiom scheme of PDL is fl,l-complete. This contrasts with the decidability of the problem when the axiom scheme is replaced by any single PDL formula.

'Uhis research wits supported in part by the National Science Foundation, Grant Nos. MCS 7719754 ' MCS 8010707, and MCS 7910261, and by a grant to the M l'I'Laboratory flor Computer Science by the I BM Corporation.

I Introduction

Propositional Dynamic Logic (PDI.) [I] is an extension of propositional logic in which "before- after" assertions aboutthe behavior of reguhu program scheims can be made directly. Propositional 01CUIUS, temporal logic and the most fanifliar versions of propositional modal logic are all ernbeddable in PDL, but PDL nevertheless has a validity problem decidable in (deterministic) exponential time [4].

In this paper we consider the deducibility problem for PDL, namely die problem of when a formula p follows from a set P of formulae. The problem comes in two versions:

(1) p is implied by F i f and only if A F - p is valid.

(2) p can be inferred from F if and only if p is valid in all structures for which A r is valid.

Note that if p is implied by r then it can be inferred from F, but the converse does not hold in general.

!~'or a finite set IF, the question whether p is implied or inferred ftom r reduces to whether a formula of PDL is valid and so is decidable. However, axioniatizations of logical languages such as the propositional calculus or PDL are often given in terms of axiom schemes, narnely, formulae whose variables may be replaced by arbitrary formulae. Thus, a single axiom scheme actually represents the infinite set of all formulae which are substitution instances of the scheme. Our main result is that

the problem of whether an arbitrary PMformuld p is deduciblefrom a singlefixed axiom scheme is ofextrentely high degree of undecidability, namely ri I 1-complete.

Massachusetts Institute of Technology Page 1 Dec 31, 1981

Page 2 of 8

The Deducibility Problem in Propositional Dynamic Logic

This result appears unexpected for at least two reasons. First, the easily recognizable infinite set of substitution instances of a single scheme seems initially to provide little more power than a single formula. For example, the problem of whether a single PDL scheme is a sound axiom,
i.e., whether all its substitution instances are valid, is equivalent to the question of whether the scheme itself regarded as a formula is valid. Hence it is decidable whether a scheme is sound.

Second, many familiar log...