Eliminating ``Converse'' from Converse PDL

Author: de Giacomo G.1

Source: Journal of Logic, Language and Information, Volume 5, Number 2, April 1996 , pp. 193-208(16)

Publisher: Springer

Key:
Free Content - Free Content
New Content - New Content
Subscribed Content - Subscribed Content
Free Trial Content - Free Trial Content

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.

Keywords: Propositional dynamic logics; logics of programs; modal logics; decision procedures

Language: English

Document Type: Regular paper

Affiliations: 1: Dipartimento di Informatica e Sistemistica, Università di Roma ``La Sapienza'', Via Salaria 113, 00198 Roma, Italy (E-mail: degiacomo@dis.uniroma1.it)

The full text electronic article is available for purchase. You will be able to download the full text electronic article after payment.

$47.00 plus tax

 

OR

Back to top

Key:
Free Content - Free Content
New Content - New Content
Subscribed Content - Subscribed Content
Free Trial Content - Free Trial Content
Page Help Click here for Page Help
Shopping cart
Tools
Sign in






Need to register?
Sign up here
Text size: A | A | A | A