Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userReasoning Under the Principle of Maximum Entropy for Modal Logics K45, KD45, and S5
240
0
0.0
(
0
)
Added by
Burkhard C. Schipper
Publication date
2013
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We propose modal Markov logic as an extension of propositional Markov logic to reason under the principle of maximum entropy for modal logics K45, KD45, and S5. Analogous to propositional Markov logic, the knowledge base consists of weighted formulas, whose weights are learned from data. However, in contrast to Markov logic, in our framework we use the knowledge base to define a probability distribution over non-equivalent epistemic situations (pointed Kripke structures) rather than over atoms, and use this distribution to assign probabilities to modal formulas. As in all probabilistic representations, the central task in our framework is inference. Although the size of the state space grows doubly exponentially in the number of propositions in the domain, we provide an algorithm that scales only exponentially in the size of the knowledge base. Finally, we briefly discuss the case of languages with an infinite number of propositions.
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.
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 present tableau calculi for some logics of nonmonotonic reasoning, as defined by Kraus, Lehmann and Magidor. We give a tableau proof procedure for all KLM logics, namely preferential, loop-cumulative, cumulative and rational logics. Our calculi are obtained by introducing suitable modalities to interpret conditional assertions. We provide a decision procedure for the logics considered, and we study their complexity.
Graded modal types systems and coeffects are becoming a standard formalism to deal with context-dependent computations where code usage plays a central role. The theory of program equivalence for modal and coeffectful languages, however, is considerably underdeveloped if compared to the denotational and operational semantics of such languages. This raises the question of how much of the theory of ordinary program equivalence can be given in a modal scenario. In this work, we show that coinductive equivalences can be extended to a modal setting, and we do so by generalising Abramskys applicative bisimilarity to coeffectful behaviours. To achieve this goal, we develop a general theory of ternary program relations based on the novel notion of a comonadic lax extension, on top of which we define a modal extension of Abramskys applicative bisimilarity (which we dub modal applicative bisimilarity). We prove such a relation to be a congruence, this way obtaining a compositional technique for reasoning about modal and coeffectful behaviours. But this is not the end of the story: we also establish a correspondence between modal program relations and program distances. This correspondence shows that modal applicative bisimilarity and (a properly extended) applicative bisimilarity distance coincide, this way revealing that modal program equivalences and program distances are just two sides of the same coin.
204 -
Eric Alsmann (School of Electrical Engineering
, Computer Science
, n University of Kassel
2021
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.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
