In this paper we show that it is possible to eliminate the "converse" operator from the propositional dynamic logic CPDL (Converse PDL), without compromising the soundness and completeness of inference for it. Specifically we present an encoding of CPDL formulae into PDL that eliminates the converse programs from a CPDL formula, but adds enough information so as not to destroy its original meaning with respect to satisfiability, validity, and logical implication. Notably, the resulting PDL formula is polynomially related to the original one. This fact allows one to build inference procedures for CPDL, by encoding CPDL formulae into PDL, and then running an inference procedure for PDL. © 1996 Kluwer Academic Publishers.
Eliminating "converse" from converse PDL / DE GIACOMO, Giuseppe. - In: JOURNAL OF LOGIC, LANGUAGE, AND INFORMATION. - ISSN 0925-8531. - 5:2(1996), pp. 193-208.
Eliminating "converse" from converse PDL
DE GIACOMO, Giuseppe
1996
Abstract
In this paper we show that it is possible to eliminate the "converse" operator from the propositional dynamic logic CPDL (Converse PDL), without compromising the soundness and completeness of inference for it. Specifically we present an encoding of CPDL formulae into PDL that eliminates the converse programs from a CPDL formula, but adds enough information so as not to destroy its original meaning with respect to satisfiability, validity, and logical implication. Notably, the resulting PDL formula is polynomially related to the original one. This fact allows one to build inference procedures for CPDL, by encoding CPDL formulae into PDL, and then running an inference procedure for PDL. © 1996 Kluwer Academic Publishers.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
