Eliminating ``converse from converse PDL

DOI10.1007/BF00173700zbMATH Open0923.03044OpenAlexW1995398260MaRDI QIDQ1923830FDOQ1923830

Authors: Giuseppe De Giacomo 

Publication date: 5 May 1999

Published in: Journal of Logic, Language and Information (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00173700

Recommendations

• Optimal and cut-free tableaux for propositional dynamic logic with converse
• scientific article; zbMATH DE number 3974280
• Combining deduction and model checking into tableaux and algorithms for converse-PDL.
• Tableaux and algorithms for Propositional Dynamic Logic with Converse
• PDL with intersection and converse: satisfiability and infinite-state model checking

zbMATH Keywords

converse propositional dynamic logicelimination of converse programsencoding of CPDL formulae into PDL

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70)

Cited In (5)

• The influence of the test operator on the expressive power of PDL-like logics
• Introspection as an action in relational models
• Title not available (Why is that?)
• Combining deduction and model checking into tableaux and algorithms for converse-PDL.
• Optimal and cut-free tableaux for propositional dynamic logic with converse

This page was built for publication: Eliminating ``converse from converse PDL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1923830)