Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userSeparating the Expressive Power of Propositional Dynamic and Modal Fixpoint Logics
205
0
0.0
(
0
)
Added by
EPTCS
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We investigate the expressive power of the two main kinds of program logics for complex, non-regular program properties found in the literature: those extending propositional dynamic logic (PDL), and those extending the modal mu-calculus. This is inspired by the recent discovery of a decidable program logic called Visibly Pushdown Fixpoint Logic with Chop which extends both the modal mu-calculus and PDL over visibly pushdown languages, which, so far, constituted the ends of two pillars of decidable program logics. Here we show that this logic is not only more expressive than either of its two fragments, but in fact even more expressive than their union. Hence, the decidability border amongst program logics has been properly pushed up. We complete the picture by providing results separating all the PDL-based and modal fixpoint logics with regular, visibly pushdown and arbitrary context-free constructions.
rate research
Read More
This paper exhibits a general and uniform method to prove completeness for certain modal fixpoint logics. Given a set Gamma of modal formulas of the form gamma(x, p1, . . ., pn), where x occurs only positively in gamma, the language Lsharp (Gamma) is obtained by adding to the language of polymodal logic a connective sharp_gamma for each gamma epsilon. The term sharp_gamma (varphi1, . . ., varphin) is meant to be interpreted as the least fixed point of the functional interpretation of the term gamma(x, varphi 1, . . ., varphi n). We consider the following problem: given Gamma, construct an axiom system which is sound and complete with respect to the concrete interpretation of the language Lsharp (Gamma) on Kripke frames. We prove two results that solve this problem. First, let Ksharp (Gamma) be the logic obtained from the basic polymodal K by adding a Kozen-Park style fixpoint axiom and a least fixpoint rule, for each fixpoint connective sharp_gamma. Provided that each indexing formula gamma satisfies the syntactic criterion of being untied in x, we prove this axiom system to be complete. Second, addressing the general case, we prove the soundness and completeness of an extension K+ (Gamma) of K_sharp (Gamma). This extension is obtained via an effective procedure that, given an indexing formula gamma as input, returns a finite set of axioms and derivation rules for sharp_gamma, of size bounded by the length of gamma. Thus the axiom system K+ (Gamma) is finite whenever Gamma is finite.
In 1979 Richard Statman proved, using proof-theory, that the purely implicational fragment of Intuitionistic Logic (M-imply) is PSPACE-complete. He showed a polynomially bounded translation from full Intuitionistic Propositional Logic into its implicational fragment. By the PSPACE-completeness of S4, proved by Ladner, and the Goedel translation from S4 into Intuitionistic Logic, the PSPACE- completeness of M-imply is drawn. The sub-formula principle for a deductive system for a logic L states that whenever F1,...,Fk proves A, there is a proof in which each formula occurrence is either a sub-formula of A or of some of Fi. In this work we extend Statman result and show that any propositional (possibly modal) structural logic satisfying a particular formulation of the sub-formula principle is in PSPACE. If the logic includes the minimal purely implicational logic then it is PSPACE-complete. As a consequence, EXPTIME-complete propositional logics, such as PDL and the common-knowledge epistemic logic with at least 2 agents satisfy this particular sub-formula principle, if and only if, PSPACE=EXPTIME. We also show how our technique can be used to prove that any finitely many-valued logic has the set of its tautologies in PSPACE.
Data streams occur widely in various real world applications. The research on streaming data mainly focuses on the data management, query evaluation and optimization on these data, however the work on reasoning procedures for streaming knowledge bases on both the assertional and terminological levels is very limited. Typically reasoning services on large knowledge bases are very expensive, and need to be applied continuously when the data is received as a stream. Hence new techniques for optimizing this continuous process is needed for developing efficient reasoners on streaming data. In this paper, we survey the related research on reasoning on expressive logics that can be applied to this setting, and point to further research directions in this area.
We study quantified propositional logics from the complexity theoretic point of view. First we introduce alternating dependency quantified boolean formulae (ADQBF) which generalize both quantified and dependency quantified boolean formulae. We show that the truth evaluation for ADQBF is AEXPTIME(poly)-complete. We also identify fragments for which the problem is complete for the levels of the exponential hierarchy. Second we study propositional team-based logics. We show that DQBF formulae correspond naturally to quantified propositional dependence logic and present a general NEXPTIME upper bound for quantified propositional logic with a large class of generalized dependence atoms. Moreover we show AEXPTIME(poly)-completeness for extensions of propositional team logic with generalized dependence atoms.
We study query containment in three closely related formalisms: monadic disjunctive Datalog (MDDLog), MMSNP (a logical generalization of constraint satisfaction problems), and ontology-mediated queries (OMQs) based on expressive description logics and unions of conjunctive queries. Containment in MMSNP was known to be decidable due to a result by Feder and Vardi, but its exact complexity has remained open. We prove 2NEXPTIME-completeness and extend this result to monadic disjunctive Datalog and to OMQs.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
