SearcharxivSearch

arXiv subjects

Daniil Kozhemiachenko

Publications and source records attributed to Daniil Kozhemiachenko.

At least 19 recordsLinked to original sources

Reasoning About Probabilities, Actions, and Knowledge in Fuzzy Modal Logic

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.

cs.LO

Probabilistic Abduction in a Fuzzy Logic Framework

We study the problem of explaining observations about the probabilities of events, such as "it rains $20\%$ of the time", "rain and snow are equally likely", etc. We explain these statements with a probability distribution or a statement about probabilities of (other) events that are consistent with our knowledge and entail the observation. We formalise this problem in a fuzzy probabilistic logic $\mathsf{FP}$. We define and motivate the notions of abduction problems and their solutions. Our main technical contribution is a comprehensive study of the complexity of solution recognition and existence for a given abduction problem in $\mathsf{FP}$ for the case of full language and its disjunctive-clause fragments. We also obtain a translation of classical probabilistic abduction (finding the most likely explanation of a given event) to $\mathsf{FP}$.

cs.LO

Modal Logic for Reasoning About Uncertainty and Confusion

We consider a modal logic that can formalise statements about uncertainty and beliefs such as `I think that my wallet is in the drawer rather than elsewhere' or `I am confused whether my appointment is on Monday or Tuesday'. To do that, we expand Gödel modal logic KG with the involutive negation ~ defined as v(~A,w)=1-v(A,w). We provide semantics with the finite model property for our new logic that we call KG_inv and show its equivalence to the standard semantics over [0,1]-valued Kripke models. Namely, we show that a formula is valid in the standard semantics of KG_inv iff it is valid in the new semantics. Using this new semantics, we construct a constraint tableaux calculus for KG_inv that allows for an explicit extraction of countermodels from complete open branches and then employ the tableaux calculus to obtain the PSPACE-completeness of the validity in KG_inv.

math.LO

Complexity of Łukasiewicz Modal Probabilistic Logics

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.

cs.LO

Tableaux for epistemic Gödel logic

We propose a multi-agent epistemic logic capturing reasoning with degrees of plausibility that agents can assign to a given statement, with $1$ interpreted as "entirely plausible for the agent" and $0$ as "completely implausible" (i.e., the agent knows that the statement is false). We formalise such reasoning in an expansion of Gödel fuzzy logic with an involutive negation and multiple $\mathbf{S5}$-like modalities. As already Gödel single-modal logics are known to lack the finite model property w.r.t. their standard $[0,1]$-valued Kripke semantics, we provide an alternative semantics that allows for the finite model property. For this semantics, we construct a strongly terminating tableaux calculus that allows us to produce finite counter-models of non-valid formulas. We then use the tableaux to show that the validity problem in our logic is $\mathsf{PSpace}$-complete when there are two or more agents, and $\mathsf{coNP}$-complete for the single-agent case.

math.LO

Paraconsistent Constructive Modal Logic

We present a family of paraconsistent counterparts of the constructive modal logic CK. These logics aim to formalise reasoning about contradictory but non-trivial propositional attitudes like beliefs or obligations. We define their Kripke-style semantics based on intuitionistic frames with two valuations which provide independent support for truth and falsity; they are connected by strong negation as defined in Nelson's logic. A family of systems is obtained depending on whether both modal operators are defined using the same or by different accessibility relations for their positive and negative support. We propose Hilbert-style axiomatisations for all logics determined by this semantic framework. We also propose a~family of modular cut-free sequent calculi that we use to establish decidability.

cs.LO

Complexity of Abduction in Łukasiewicz Logic

We explore the problem of explaining observations in contexts involving statements with truth degrees such as `the lift is loaded', `the symptoms are severe', etc. To formalise these contexts, we consider infinitely-valued Łukasiewicz fuzzy logic. We define and motivate the notions of abduction problems and explanations in the language of Łukasiewicz logic expanded with `interval literals' of the form $p\geq\mathbf{c}$, $p\leq\mathbf{c}$, and their negations that express the set of values a variable can have. We analyse the complexity of standard abductive reasoning tasks (solution recognition, solution existence, and relevance / necessity of hypotheses) in Łukasiewicz logic for the case of the full language and for the case of theories containing only disjunctive clauses and show that in contrast to classical propositional logic, the abduction in the clausal fragment has lower complexity than in the general case.

cs.LO

Filter-induced entailment relations in paraconsistent Gödel logics

We consider two expansions of Gödel logic $\mathsf{G}$ with two versions of paraconsistent negation. The first one is $\mathsf{G_{inv}}$ -- the expansion of $\mathsf{G}$ with an involuitive negation ${\sim_\mathsf{i}}$ defined via $v({\sim_\mathsf{i}}ϕ)=1-v(ϕ)$. The second one is $\mathsf{G}^2_{(\rightarrow,-\!<)}$ -- an expansion with a so-called strong negation $\neg$. This logic utilises two independent valuations on $[0,1]$ -- $v_1$ (support of truth or positive support) and $v_2$ (support of falsity or negative support) that are connected with $\neg$. Two valuations in $\mathsf{G}^2_{(\rightarrow,-\!<)}$ can be combined into one valuation $v$ on $[0,1]^{\Join}$ -- the twisted product of $[0,1]$ with itself -- with two components $v_1$ and $v_2$. The two logics are closely connected as ${\sim_\mathsf{i}}$ and $\neg$ allow for similar definitions of co-implication -- $ϕ-\!<χ:={\sim_\mathsf{i}}({\sim_\mathsf{i}}χ\rightarrow{\sim_\mathsf{i}}ϕ)$ and $ϕ-\!<χ:=\neg(\negχ\rightarrow\negϕ)$ -- but do not coincide since the set of values of $\mathsf{G}^2_{(\rightarrow,-\!<)}$ is not ordered linearly. Our main goal is to study different entailment relations in $\mathsf{G_{inv}}$ and $\mathsf{G}^2_{(\rightarrow,-\!<)}$ that are induced by filters on $[0,1]$ and $[0,1]^{\Join}$, respectively. In particular, we determine the exact number of such relations in both cases, establish whether any of them coincide with the entailment defined via the order on $[0,1]$ and $[0,1]^{\Join}$, and obtain their hierarchy. We also construct reductions of filter-induced entailment relations to the ones defined via the order.

math.LO

Two-layered logics for probabilities and belief functions over Belnap--Dunn logic

This paper is an extended version of an earlier submission to WoLLIC 2023. We discuss two-layered logics formalising reasoning with probabilities and belief functions that combine the Lukasiewicz $[0,1]$-valued logic with Baaz $\triangle$ operator and the Belnap--Dunn logic. We consider two probabilistic logics that present two perspectives on the probabilities in the Belnap--Dunn logic: $\pm$-probabilities and $\mathbf{4}$-probabilities. In the first case, every event $ϕ$ has independent positive and negative measures that denote the likelihoods of $ϕ$ and $\negϕ$, respectively. In the second case, the measures of the events are treated as partitions of the sample into four exhaustive and mutually exclusive parts corresponding to pure belief, pure disbelief, conflict and uncertainty of an agent in $ϕ$. In addition to that, we discuss two logics for the paraconsistent reasoning with belief and plausibility functions. They equip events with two measures (positive and negative) with their main difference being whether the negative measure of $ϕ$ is defined as the belief in $\negϕ$ or treated independently as the plausibility of $\negϕ$. We provide a sound and complete Hilbert-style axiomatisation of the logic of $\mathbf{4}$-probabilities and establish faithful translations between it and the logic of $\pm$-probabilities. We also show that the satisfiability problem in all logics is $\mathsf{NP}$-complete.

math.LO

Abductive Reasoning in a Paraconsistent Framework

We explore the problem of explaining observations starting from a classically inconsistent theory by adopting a paraconsistent framework. We consider two expansions of the well-known Belnap--Dunn paraconsistent four-valued logic $\mathsf{BD}$: $\mathsf{BD}_\circ$ introduces formulas of the form $\circϕ$ (the information on $ϕ$ is reliable), while $\mathsf{BD}_\triangle$ augments the language with $\triangleϕ$'s (there is information that $ϕ$ is true). We define and motivate the notions of abduction problems and explanations in $\mathsf{BD}_\circ$ and $\mathsf{BD}_\triangle$ and show that they are not reducible to one another. We analyse the complexity of standard abductive reasoning tasks (solution recognition, solution existence, and relevance / necessity of hypotheses) in both logics. Finally, we show how to reduce abduction in $\mathsf{BD}_\circ$ and $\mathsf{BD}_\triangle$ to abduction in classical propositional logic, thereby enabling the reuse of existing abductive reasoning procedures.

cs.LO

Queries With Exact Truth Values in Paraconsistent Description Logics

We present a novel approach to querying classical inconsistent description logic (DL) knowledge bases by adopting a~paraconsistent semantics with the four Belnapian values: exactly true ($\mathbf{T}$), exactly false ($\mathbf{F}$), both ($\mathbf{B}$), and neither ($\mathbf{N}$). In contrast to prior studies on paraconsistent DLs, we allow truth value operators in the query language, which can be used to differentiate between answers having contradictory evidence and those having only positive evidence. We present a reduction to classical DL query answering that allows us to pinpoint the precise combined and data complexity of answering queries with values in paraconsistent $\mathcal{ALCHI}$ and its sublogics. Notably, we show that tractable data complexity is retained for Horn DLs. We present a comparison with repair-based inconsistency-tolerant semantics, showing that the two approaches are incomparable.

cs.LO

Qualitative reasoning in a two-layered framework

The reasoning with qualitative uncertainty measures involves comparative statements about events in terms of their likeliness without necessarily assigning an exact numerical value to these events. The paper is divided into two parts. In the first part, we formalise reasoning with the qualitative counterparts of capacities, belief functions, and probabilities, within the framework of two-layered logics. Namely, we provide two-layered logics built over the classical propositional logic using a unary belief modality $\Be$ that connects the inner layer to the outer one where the reasoning is formalised by means of Gödel logic. We design their Hilbert-style axiomatisations and prove their completeness. In the second part, we discuss the paraconsistent generalisations of the logics for qualitative uncertainty that take into account the case of the available information being contradictory or inconclusive.

math.LO

Non-distributive relatives of ETL and NFL

In this paper, we devise non-distributive relatives of Exactly True Logic (ETL) by Pietz and Riveccio and its dual (NFL) Non-Falsity Logic by Shramko, Zaitsev and Belikov. We consider two pre-orders which are algebraic counterparts of the ETL's and NFL's entailment relations on the De Morgan lattice $\mathbf{4}$. We generalise these pre-orders and determine which distributive properties that hold on $\mathbf{4}$ are not forced by either of the pre-orders. We then construct relatives of ETL and NFL but lack such distributive properties. For these logics, we also devise a truth table semantics which uses non-distributive lattice $\mathbf{M3}$ as their lattice of truth values. We also provide analytic tableaux systems that work with sequents of the form $ϕ\vdashχ$. We also prove the correctness and completeness results for these proof systems and provide a neat generalisation for non-distributive ETL- and NFL-like logics built over a certain family of non-distributive modular lattices.

math.LO

Generalisation of proof simulation procedures for Frege systems by M.L.~Bonet and S.R.~Buss

In this paper, we present a~generalisation of proof simulation procedures for Frege systems by Bonet and Buss to some logics for which the deduction theorem does not hold. In particular, we study the case of finite-valued Łukasiewicz logics. To this end, we provide proof systems that augment Avron's Frege system for Łukasiewicz three-valued logic with nested and general versions of the disjunction elimination rule, respectively. For these systems we provide upper bounds on speed-ups w.r.t.\ both the number of steps in proofs and the length of proofs. We also consider Tamminga's natural deduction and Avron's hypersequent calculus for 3-valued Łukasiewicz logic and generalise our results considering the disjunction elimination rule to all finite-valued Łukasiewicz logics.

math.LO

Fuzzy bi-Gödel modal logic and its paraconsistent relatives

We present the axiomatisation of the fuzzy bi-Gödel modal logic (formulated in the language containing $\triangle$ and treating the coimplication as a defined connective) and establish its PSpace-completeness. We also consider its paraconsistent relatives defined on fuzzy frames with two valuations $e_1$ and $e_2$ standing for the support of truth and falsity, respectively, and equipped with \emph{two fuzzy relations} $R^+$ and $R^-$ used to determine supports of truth and falsity of modal formulas. We establish embeddings of these paraconsistent logics into the fuzzy bi-Gödel modal logic and use them to prove their PSpace-completeness and obtain the characterisation of definable frames.

math.LO

Non-contingecy in a paraconsistent setting

We study an extension of First Degree Entailment (FDE) by Dunn and Belnap with a non-contingency operator $\blacktriangleϕ$ which is construed as "$ϕ$ has the same value in all accessible states" or "all sources give the same information on the truth value of $ϕ$". We equip this logic dubbed $\mathbf{K}^\blacktriangle_\mathbf{FDE}$ with frame semantics and show how the bi-valued models can be interpreted as interconnected networks of Belnapian databases with the $\blacktriangle$ operator modelling search for inconsistencies in the provided information. We construct an analytic cut system for the logic and show its soundness and completeness. We prove that $\blacktriangle$ is not definable via the necessity modality $\Box$ of $\mathbf{K_{FDE}}$. Furthermore, we prove that in contrast to the classical non-contingency logic, reflexive, $\mathbf{S4}$, and $\mathbf{S5}$ (among others) frames \emph{are definable}.

math.LO

Simple tableaux for two expansions of Gödel modal logic

This paper considers two logics. The first one, $\mathbf{K}\mathsf{G}_\mathsf{inv}$, is an expansion of the Gödel modal logic $\mathbf{K}\mathsf{G}$ with the involutive negation $\sim_\mathsf{i}$ defined as $v({\sim_\mathsf{i}}ϕ,w)=1-v(ϕ,w)$. The second one, $\mathbf{K}\mathsf{G}_\mathsf{bl}$, is the expansion of $\mathbf{K}\mathsf{G}_\mathsf{inv}$ with the bi-lattice connectives and modalities. We explore their semantical properties w.r.t. the standard semantics on $[0,1]$-valued Kripke frames and define a unified tableaux calculus that allows for the explicit countermodel construction. For this, we use an alternative semantics with the finite model property. Using the tableaux calculus, we construct a decision algorithm and show that satisfiability and validity in $\mathbf{K}\mathsf{G}_\mathsf{inv}$ and $\mathbf{K}\mathsf{G}_\mathsf{bl}$ are PSpace-complete.

math.LO

Knowledge and ignorance in Belnap--Dunn logic

In this paper, we argue that the usual approach to modelling knowledge and belief with the necessity modality $\Box$ does not produce intuitive outcomes in the framework of the Belnap--Dunn logic ($\mathsf{BD}$, alias $\mathsf{FDE}$ -- first-degree entailment). We then motivate and introduce a non\-standard modality $\blacksquare$ that formalises knowledge and belief in $\mathsf{BD}$ and use $\blacksquare$ to define $\bullet$ and $\blacktriangledown$ that formalise the \emph{unknown truth} and ignorance as \emph{not knowing whether}, respectively. Moreover, we introduce another modality $\mathbf{I}$ that stands for \emph{factive ignorance} and show its connection with $\blacksquare$. We equip these modalities with Kripke-frame-based semantics and construct a sound and complete analytic cut system for $\mathsf{BD}^\blacksquare$ and $\mathsf{BD}^\mathbf{I}$ -- the expansions of $\mathsf{BD}$ with $\blacksquare$ and $\mathbf{I}$. In addition, we show that $\Box$ as it is customarily defined in $\mathsf{BD}$ cannot define any of the introduced modalities, nor, conversely, neither $\blacksquare$ nor $\mathbf{I}$ can define $\Box$. We also demonstrate that $\blacksquare$ and $\mathbf{I}$ are not interdefinable and establish the definability of several important classes of frames using $\blacksquare$.

math.LO