arXiv subjects
Publications and source records attributed to Igor Sedlár.
Motivated by relevant epistemic logic, we extend Dunn's simple Kripke-style binary relational semantics for the semi-relevant logic RM to fit a modal extension of RM. It is shown that the modal axioms and rules that need to be added to RM to obtain a sound and complete axiomatisation of its modal extension give an axiomatisation of modal extensions of all logics in the family of generalised Nelson logics, also studied by Dunn.
Topological Evidence Logic (TEL) is a recent approach to epistemic logic that uses topological tools to model coherent epistemic justification. Specifically, a hypothesis is coherently justified if and only if it is entailed by a dense open set. In its simplest form, TEL can be formulated as an extension of S4 with a global modality. All currently studied forms of TEL are based on classical propositional logic, which has been heavily criticised for misrepresenting the way in which ordinary agents reason. In this article, we show that the TEL approach is robust under modifications to the propositional base. We show that an extension of the intuitionistic modal framework recently introduced by de Groot and Shillito, incorporating a global modality, enables coherent justification to be expressed in an intuitionistic setting. Furthermore, we adapt the recent work of Standefer et al., which extends relevant logic with a global modality, to show that coherent justification can be expressed in a relevant setting if an interior-of-complement operator is added to the language. Our main technical result is a soundness and completeness theorem for relevant TEL based on the weak relevant modal logic BS4.
We explore a fuzzy modal logic that can formalise probabilistic reasoning about actions and knowledge. In particular, we deal with contexts involving statements about events expressed via modal formulas, e.g., "after doing $a$, the probability of $A$ knowing that $p$ holds increases / decreases / is equal to $0.25$", "according to $A$, $p$ is equally likely to happen after doing $a$ or $b$", etc. We define the semantics of the logic on Kripke frames equipped with probability measures. We analyse the complexity of deciding the satisfiability of formulas of our logic over finitely branching models, for the full language and its fragments of varying expressivity. In particular, we identify several fragments of our logic where satisfiability is decidable in polynomial time.
In various computational systems, accessing information incurs time, memory or energy costs. However, standard epistemic logics usually model the acquisition of evidence as a cost-free process, which restricts their applicability in environments with limited resources. In this paper, we bridge the gap between qualitative epistemic reasoning and quantitative resource constraints by introducing semiring-annotated topological spaces (seats). Building on Topological Evidence Logic (TEL), we extend the representation of evidence as open sets, adding an annotation function that maps evidence to semiring ideals, representing the resource budgets sufficient for observation. This framework allows us to reason not only about what is observable in principle, but also about what is affordable given a specific budget. We develop a family of seat-based epistemic logics with resource-indexed modalities and provide sound, strongly complete axiomatisations for these logics. Furthermore, we introduce suitable notions of bisimulation and disjoint union to delineate the expressive power of our framework.
Modal probabilistic logics provide a framework for reasoning about probability in modal contexts, involving notions such as knowledge, belief, time, and action. In this paper, we study a particular family of these logics, extending the modal Łukasiewicz many-valued logic. These logics are shown to be capable of expressing nuanced probabilistic concepts, including upper and lower probabilities. Our main contribution is a PSPACE-completeness result for two variants of the local consequence problem, providing a precise computational characterisation.
Building on Ésik and Kuich's completeness result for finitely weighted Kleene algebra, we establish relational and language completeness results for finitely weighted Kleene algebra with tests. Similarly as Ésik and Kuich, we assume that the finite semiring of weights is commutative, partially ordered and zero-bounded, but we also assume that it is integral. We argue that finitely weighted Kleene algebra with tests is a natural framework for equational reasoning about weighted programs in cases where an upper bound on admissible weights is assumed.
We study versions of Kleene algebra with dynamic tests, that is, extensions of Kleene algebra with domain and antidomain operators. We show that Kleene algebras with tests and Propositional dynamic logic correspond to special cases of the dynamic test framework. In particular, we establish completeness results with respect to relational models and guarded-language models, and we show that two prominent classes of Kleene algebras with dynamic tests have an EXPTIME-complete equational theory.
Epistemic logics of intensional groups lift the assumption that membership in a group of agents is common knowledge. Instead of being represented directly as a set of agents, intensional groups are represented by a property that may change its extension from world to world. Several authors have considered versions of the intensional group framework where group-specifying properties are articulated using structured terms of a language, such as the language of Boolean algebras or of description logic. In this paper we formulate a general semantic framework for epistemic logics of structured intensional groups, develop the basic theory leading to completeness-via-canonicity results, and show that several frameworks presented in the literature correspond to special cases of the general framework.
Weighted programs generalize probabilistic programs and offer a framework for specifying and encoding mathematical models by means of an algorithmic representation. Kleene algebra with tests is an algebraic formalism based on regular expressions with applications in proving program equivalence. We extend the language of Kleene algebra with tests so that it is sufficient to formalize reasoning about a simplified version weighted programs. We introduce relational semantics for the extended language, and we generalize the relational semantics to an appropriate extension of Kleene algebra with tests, called Kleene algebra with weights and tests. We demonstrate by means of an example that Kleene algebra with weights and tests offers a simple algebraic framework for reasoning about equivalence and optimal runs of weighted programs.
Kozen and Tiuryn have introduced the substructural logic $\mathsf{S}$ for reasoning about correctness of while programs (ACM TOCL, 2003). The logic $\mathsf{S}$ distinguishes between tests and partial correctness assertions, representing the latter by special implicational formulas. Kozen and Tiuryn's logic extends Kleene altebra with tests, where partial correctness assertions are represented by equations, not terms. Kleene algebra with codomain, $\mathsf{KAC}$, is a one-sorted alternative to Kleene algebra with tests that expands Kleene algebra with an operator that allows to construct a Boolean subalgebra of tests. In this paper we show that Kozen and Tiuryn's logic embeds into the equational theory of the expansion of $\mathsf{KAC}$ with residuals of Kleene algebra multiplication and the upper adjoint of the codomain operator.
We develop a framework for epistemic logic that combines relevant modal logic with classical propositional logic. In our framework the agent is modeled as reasoning in accordance with a relevant modal logic while the propositional fragment of our logics is classical. In order to achieve this feature, we modify the relational semantics for relevant modal logics so that validity in a model is defined as satisfaction throughout a set of designated states that, as far as propositional connectives are concerned, behave like classical possible worlds. The main technical result of the paper is a modular completeness theorem parametrized by the relevant modal logic formalizing the agent's reasoning.
Kleene algebra with tests, KAT, provides a simple two-sorted algebraic framework for verifying properties of propositional while programs. Kleene algebra with domain, KAD, is a one-sorted alternative to KAT. The equational theory of KAT embeds into KAD, but KAD lacks some natural properties of KAT. For instance, not each Kleene algebra expands to a KAD, and the subalgebra of tests in each KAD is forced to be the maximal Boolean subalgebra of the negative cone. In this paper we propose a generalization of KAD that avoids these features while still embedding the equational theory of KAT. We show that several natural properties of the domain operator of KAD can be added to the generalized framework without affecting the results. We consider a variant of the framework where test complementation is defined using a residual of the Kleene algebra multiplication.
It is common in various non-classical logics, especially in relevant logics, to characterize negation semantically via the operation known as Routley star. This operation works well within relational semantic frameworks based on prime theories. We study this operation in the context of "information-based" semantics for which it is characteristic that sets of formulas supported by individual information states are theories that do not have to be prime. We will show that, somewhat surprisingly, the incorporation of Routley star into the information-based semantics does not lead to a collapse or a trivialization of the whole semantic system. On the contrary, it leads to a technically elegant though quite restricted semantic framework that determines a particular logic. We study some basic properties of this semantics. For example, we show that within this framework double negation law is valid only in involutive linear frames. We characterize axiomatically the logic of all linear frames and show that the logic of involutive linear frames coincides with a system that Mike Dunn coined Kalman logic. This logic is the fragment (for the language restricted to conjunction, disjunction and negation) of the "semi-relevant" logic known as R-mingle. Finally, we characterize by a deductive system the logic of all information frames equipped with Routley star.
We study a many-valued generalization of Propositional Dynamic Logic where formulas in states and accessibility relations between states of a Kripke model are evaluated in a finite FL-algebra. One natural interpretation of this framework is related to reasoning about costs of performing structured actions. We prove that PDL over any finite FL-algebra is decidable. We also establish a general completeness result for a class of PDLs based on commutative integral FL-algebras with canonical constants.
We study an extension of the Distributive Full Non-associative Lambek Calculus with iterative division operators. The iterative operators can be seen as representing iterative composition of linguistic resources or of actions. A complete axiomatization of the logic is provided and decidability is established via a proof of the finite model property.
We extend the epistemic logic with De Morgan negation by Fagin et al. (Artif. Intell. 79, 203-240, 1995) by adding operators for universal and common knowledge in a group of agents, and with a formalization of information update using a generalized version of the left division connective of the non-associative Lambek calculus. We provide sound and complete axiomatizations of the basic logic with the group operators and the basic logic with group operators and updates. Both logics are shown to be decidable.
We introduce BPDL, a combination of propositional dynamic logic PDL with the basic four-valued modal logic BK studied by Odintsov and Wansing (`Modal logics with Belnapian truth values', J. Appl. Non-Class. Log. 20, 279--301 (2010)). We modify the standard arguments based on canonical models and filtration to suit the four-valued context and prove weak completeness and decidability of BPDL.