Building on previous work by André Platzer, we present a formal language for Stochastic Differential Dynamic Logic, and define its semantics, axioms and inference rules. Compared to the previous effort, our account of the Stochastic Differential Dynamic Logic follows closer to and is more compatible with the traditional account of the regular Differential Dynamic Logic. We resolve an issue with the well-definedness of the original work's semantics, while showing how to make the logic more expressive by incorporating nondeterministic choice, definite descriptions and differential terms. Definite descriptions necessitate using a three-valued truth semantics. We also give the first Uniform Substitution calculus for Stochastic Differential Dynamic Logic, making it more practical to implement in proof assistants.
In a modular approach, we lift Hilbert-style proof systems for propositional, modal and first-order logic to generalized systems for their respective team-based extensions. We obtain sound and complete axiomatizations for the dependence-free fragment FO(~) of Väänänen's first-order team logic TL, for propositional team logic PTL, quantified propositional team logic QPTL, modal team logic MTL, and for the corresponding logics of dependence, independence, inclusion and exclusion. As a crucial step in the completeness proof, we show that the above logics admit, in a particular sense, a semantics-…
Manipulating logic functions via majority operators recently drew the attention of researchers in computer science. For example, circuit optimization based on majority operators enables superior results as compared to traditional logic systems. Also, the Boolean satisfiability problem finds new solving approaches when described in terms of majority decisions. To support computer logic applications based on majority a sound and complete set of axioms is required. Most of the recent advances in majority logic deal only with ternary majority (MAJ- 3) operators because the axiomatization with sole…
Standard epistemic logic studies propositional knowledge, yet many other types of knowledge such as "knowing whether", "knowing what", "knowing how" are frequently and widely used in everyday life as well as academic fields. In "Conditionally Knowing What" by Wang and Fan, an axiomatization of the epistemic logic with both regular "knowing that" operator and "conditionally knowing what" operator is given. Then the decidability and complexity of this logic command our study. In this paper, we direct our attention to the arbitrary models instead of epistemic models, thus making things clearer, a…
We consider a specific class of tree structures that can represent basic structures in linguistics and computer science such as XML documents, parse trees, and treebanks, namely, finite node-labeled sibling-ordered trees. We present axiomatizations of the monadic second-order logic (MSO), monadic transitive closure logic (FO(TC1)) and monadic least fixed-point logic (FO(LFP1)) theories of this class of structures. These logics can express important properties such as reachability. Using model-theoretic techniques, we show by a uniform argument that these axiomatizations are complete, i.e., eac…
Problems in two axiomatizations of Jaśkowski's discussive (or discursive) logic D2 are considered. A recent axiomatization of D2 and completeness proof relative to D2's intended semantics seems to be mistaken because some formulas valid according to the intended semantics turn out to be unprovable. Although no new axiomatization is offered, nor a repaired completeness proof given, the shortcomings identified here may be a step toward an improved axiomatization.
Continuous Markovian Logic (CML) is a multimodal logic that expresses quantitative and qualitative properties of continuous-time labelled Markov processes with arbitrary (analytic) state-spaces, henceforth called continuous Markov processes (CMPs). The modalities of CML evaluate the rates of the exponentially distributed random variables that characterize the duration of the labeled transitions of a CMP. In this paper we present weak and strong complete axiomatizations for CML and prove a series of metaproperties, including the finite model property and the construction of canonical models. CM…
We prove two completeness results, one for the extension of dependence logic by a monotone generalized quantifier Q with weak interpretation, weak in the meaning that the interpretation of Q varies with the structures. The second result considers the extension of dependence logic where Q is interpreted as "there exists uncountable many." Both of the axiomatizations are shown to be sound and complete for FO(Q) consequences.
This paper first shows that the popular axiomatic systems proposed by Nute for Lewis' conditional logics are not equivalent to Lewis' original systems. In particular, the axiom CA which is derivable in Lewis' systems is not derivable in Nute's systems. Then the paper proposes a new set of axiomatizations for Lewis' conditional logics, without using CSO, or RCEA, or the rule of interchange of logical equivalents. Instead, the new axiomatizations adopt two axioms which correspond to cautious monotonicity and cautious cut in nonmonotonic logics, respectively. Finally, the paper gives a simple res…
Dynamic Topological Logic (DTL) is a multimodal system for reasoning about dynamical systems. It is defined semantically and, as such, most of the work done in the field has been model-theoretic. In particular, the problem of finding a complete axiomatization for the full language of DTL over the class of all dynamical systems has proven to be quite elusive. Here we propose to enrich the language to include a polyadic topological modality, originally introduced by Dawar and Otto in a different context. We then provide a sound axiomatization for DTL over this extended language, and prove that i…
A general method is established to derive a ground-complete axiomatization for a weak semantics from such an axiomatization for its concrete counterpart, in the context of the process algebra BCCS. This transformation moreover preserves omega-completeness. It is applicable to semantics at least as coarse as impossible futures semantics. As an application, ground- and omega-complete axiomatizations are derived for weak failures, completed trace and trace semantics. We then present a finite, sound, ground-complete axiomatization for the concrete impossible futures preorder, which implies a finit…
Weighted monadic second-order logic is a weighted extension of monadic second-order logic that captures exactly the behaviour of weighted automata. Its semantics is parameterized with respect to a semiring on which the values that weighted formulas output are evaluated. Gastin and Monmege (2018) gave abstract semantics for a version of weighted monadic second-order logic to give a more general and modular proof of the equivalence of the logic with weighted automata. We focus on the abstract semantics of the logic and we give a complete axiomatization both for the full logic and for a fragment …
We generalize intuitionistic tense logics to the multi-modal case by placing grammar logics on an intuitionistic footing. We provide axiomatizations for a class of base intuitionistic grammar logics as well as provide axiomatizations for extensions with combinations of seriality axioms and what we call "intuitionistic path axioms". We show that each axiomatization is sound and complete with completeness being shown via a typical canonical model construction.
We give sound and complete Hilbert-style axiomatizations for propositional dependence logic (PD), modal dependence logic (MDL), and extended modal dependence logic (EMDL) by extending existing axiomatizations for propositional logic and modal logic. In addition, we give novel labeled tableau calculi for PD, MDL, and EMDL. We prove soundness, completeness and termination for each of the labeled calculi.
This paper revisits the multi-agent epistemic logic presented in [10], where agents and sets of agents are replaced by abstract, intensional "names". We make three contributions. First, we study its model theory, providing adequate notions of bisimulation and frame morphisms, and use them to study the logic's expressive power and definability. Second, we show that the logic has a natural neighborhood semantics, which in turn allows to show that the axiomatization in [10] does not rely on possibly controversial introspective properties of knowledge. Finally, we extend the logic with common and …
We give sound and complete axiomatizations for XPath with data tests by "equality" or "inequality", and containing the single "child" axis. This data-aware logic predicts over data trees, which are tree-like structures whose every node contains a label from a finite alphabet and a data value from an infinite domain. The language allows us to compare data values of two nodes but cannot access the data values themselves (i.e. there is no comparison by constants). Our axioms are in the style of equational logic, extending the axiomatization of data-oblivious XPath, by B. ten Cate, T. Litak and M.…
We address a fundamental mismatch between the combinations of dynamics that occur in cyber-physical systems and the limited kinds of dynamics supported in analysis. Modern applications combine communication, computation, and control. They may even form dynamic distributed networks, where neither structure nor dimension stay the same while the system follows hybrid dynamics, i.e., mixed discrete and continuous dynamics. We provide the logical foundations for closing this analytic gap. We develop a formal model for distributed hybrid systems. It combines quantified differential equations with qu…
This note proposes various axiomatizations of contingency logic under neighborhood semantics. In particular, by defining a suitable canonical neighborhood function, we give sound and complete axiomatizations of monotone contingency logic and regular contingency logic, thereby answering two open questions raised by Bakhtiari, van Ditmarsch, and Hansen. The canonical function is inspired by a function proposed by Kuhn in 1995. We show that Kuhn's function is actually equal to a related function originally given by Humberstone.
We compare different epistemic notions in the presence of awareness of propositional variables: the logics of implicit knowledge (in which explicit knowledge is definable), explicit knowledge, and speculative knowledge. Different notions of bisimulation are suitable for these logics. We provide correspondence between bisimulation and modal equivalence on image-finite models for these logics. The logic of speculative knowledge is equally expressive as the logic of explicit knowledge, and the logic of implicit knowledge is more expressive than both. We also provide axiomatizations for the three …
This article proves the completeness of an axiomatization for differential equation invariants described by Noetherian functions. First, the differential equation axioms of differential dynamic logic are shown to be complete for reasoning about analytic invariants. Completeness crucially exploits differential ghosts, which introduce additional variables that can be chosen to evolve freely along new differential equations. Cleverly chosen differential ghosts are the proof-theoretical counterpart of dark matter. They create new hypothetical state, whose relationship to the original state variabl…
In this contribution we present arbitrary arrow update model logic (AAUML). This is a dynamic epistemic logic or update logic. In update logics, static/basic modalities are interpreted on a given relational model whereas dynamic/update modalities induce transformations (updates) of relational models. In AAUML the update modalities formalize the execution of arrow update models, and there is also a modality for quantification over arrow update models. Arrow update models are an alternative to the well-known action models. We provide an axiomatization of AAUML. The axiomatization is a rewrite sy…
Dynamic evidence logics are logics for reasoning about the evidence and evidence-based beliefs of agents in a dynamic environment. In this paper, we introduce a family of logics for reasoning about relational evidence: evidence that involves an orderings of states in terms of their relative plausibility. We provide sound and complete axiomatizations for the logics. We also present several evidential actions and prove soundness and completeness for the associated dynamic logics.
Differential Linear Logic enriches Linear Logic with additional logical rules for the exponential connectives, dual to the usual rules of dereliction, weakening and contraction. We present a proof-net syntax for Differential Linear Logic and a categorical axiomatization of its denotational models. We also introduce a simple categorical condition on these models under which a general antiderivative operation becomes available. Last we briefly describe the model of sets and relations and give a more detailed account of the model of finiteness spaces and linear and continuous functions.
We study logic for reasoning with if-then formulas describing dependencies between attributes of objects which are observed in consecutive points in time. We introduce semantic entailment of the formulas, show its fixed-point characterization, investigate closure properties of model classes, present an axiomatization and prove its completeness, and investigate alternative axiomatizations and normalized proofs. We investigate decidability and complexity issues of the logic and prove that the entailment problem is NP-hard and belongs to EXPSPACE. We show that by restricting to predictive formula…
We investigate some finitely-valued generalizations of propositional dynamic logic with tests. We start by introducing the (n+1)-valued Kripke models and a corresponding language based on a modal extension of Łukasiewicz many-valued logic. We illustrate the definitions by providing a framework for an analysis of the Rényi - Ulam searching game with errors. Our main result is the axiomatization of the theory of the (n+1)-valued Kripke models. This result is obtained through filtration of the canonical model of the smallest (n+1)-valued propositional dynamic logic.
This work proposes a Dynamic Epistemic Logic with Communication Actions that can be performed concurrently. Unlike Concurrent Epistemic Action Logic introduced by Ditmarsch, Hoek and Kooi, where the concurrency mechanism is the so called true concurrency, here we use an approach based on process calculus, like CCS and CSP, and Action Models Logic. Our approach makes possible the proof of soundness, completeness and decidability, different from the others approaches. We present an axiomatization and show that the proof of soundness, completeness and decidability can be done using a reduction me…
We prove the completeness of an axiomatization for differential equation invariants. First, we show that the differential equation axioms in differential dynamic logic are complete for all algebraic invariants. Our proof exploits differential ghosts, which introduce additional variables that can be chosen to evolve freely along new differential equations. Cleverly chosen differential ghosts are the proof-theoretical counterpart of dark matter. They create new hypothetical state, whose relationship to the original state variables satisfies invariants that did not exist before. The reflection of…
Probabilistic team semantics is a framework for logical analysis of probabilistic dependencies. Our focus is on the axiomatizability, complexity, and expressivity of probabilistic inclusion logic and its extensions. We identify a natural fragment of existential second-order logic with additive real arithmetic that captures exactly the expressivity of probabilistic inclusion logic. We furthermore relate these formalisms to linear programming, and doing so obtain PTIME data complexity for the logics. Moreover, on finite structures, we show that the full existential second-order logic with additi…
The one-variable fragment of any first-order logic may be considered as a modal logic, where the universal and existential quantifiers are replaced by a box and diamond modality, respectively. In several cases, axiomatizations of algebraic semantics for these logics have been obtained: most notably, for the modal counterparts S5 and MIPC of the one-variable fragments of first-order classical logic and intuitionistic logic, respectively. Outside the setting of first-order intermediate logics, however, a general approach is lacking. This paper provides the basis for such an approach in the setti…
Dynamic topological logic (DTL) is a polymodal logic designed for reasoning about {\em dynamic topological systems. These are pairs (X,f), where X is a topological space and f:X->X is continuous. DTL uses a language L which combines the topological S4 modality [] with temporal operators from linear temporal logic. Recently, I gave a sound and complete axiomatization DTL* for an extension of the logic to the language L*, where <> is allowed to act on finite sets of formulas and is interpreted as a tangled closure operator. No complete axiomatization is known over L, although one proof system, w…
We propose a multi-agent logic of knowledge, public and arbitrary announcements, that is interpreted on topological spaces in the style of subset space semantics. The arbitrary announcement modality functions similarly to the effort modality in subset space logics, however, it comes with intuitive and semantic differences. We provide axiomatizations for three logics based on this setting, and demonstrate their completeness.
Nominal logic is a variant of first-order logic that provides support for reasoning about bound names in abstract syntax. A key feature of nominal logic is the new-quantifier, which quantifies over fresh names (names not appearing in any values considered so far). Previous attempts have been made to develop convenient rules for reasoning with the new-quantifier, but we argue that none of these attempts is completely satisfactory. In this article we develop a new sequent calculus for nominal logic in which the rules for the new- quantifier are much simpler than in previous attempts. We also pro…
This paper presents a uniform substitution calculus for differential game logic (dGL). Church's uniform substitutions substitute a term or formula for a function or predicate symbol everywhere. After generalizing them to differential game logic and allowing for the substitution of hybrid games for game symbols, uniform substitutions make it possible to only use axioms instead of axiom schemata, thereby substantially simplifying implementations. Instead of subtle schema variables and soundness-critical side conditions on the occurrence patterns of logical variables to restrict infinitely many a…
Berlin University of Applied Sciences（柏林应用科学大学）；King’s College（国王学院）
The article proposes a formal semantics of happiness and sadness modalities in imperfect information setting. It shows that these modalities are not definable through each other and gives a sound and complete axiomatization of their properties.
Recent authors have proposed analyzing conditional reasoning through a notion of intervention on a simulation program, and have found a sound and complete axiomatization of the logic of conditionals in this setting. Here we extend this setting to the case of probabilistic simulation models. We give a natural definition of probability on formulas of the conditional language, allowing for the expression of counterfactuals, and prove foundational results about this definition. We also find an axiomatization for reasoning about linear inequalities involving probabilities in this setting. We prove …
Covariant-contravariant simulation and conformance simulation generalize plain simulation and try to capture the fact that it is not always the case that "the larger the number of behaviors, the better". We have previously studied their logical characterizations and in this paper we present the axiomatizations of the preorders defined by the new simulation relations and their induced equivalences. The interest of our results lies in the fact that the axiomatizations help us to know the new simulations better, understanding in particular the role of the contravariant characteristics and their i…
We introduce a new semantics for a logic of explicit and implicit beliefs based on the concept of multi-agent belief base. Differently from existing Kripke-style semantics for epistemic logic in which the notions of possible world and doxastic/epistemic alternative are primitive, in our semantics they are non-primitive but are defined from the concept of belief base. We provide a complete axiomatization and prove decidability for our logic via a finite model argument. We also provide a polynomial embedding of our logic into Fagin & Halpern's logic of general awareness and establish a complexit…
In this paper, we propose a new neighborhood semantics for contingency logic, by introducing a simple property in standard neighborhood models. This simplifies the neighborhood semantics given in (Fan and van Ditmarsch, 2015), but does not change the set of valid formulas. Under this perspective, among various notions of bisimulation and respective Hennessy-Milner Theorems, we show that $c$-bisimulation is equivalent to nbh-$Δ$-bisimulation in the literature, which guides us to understand the essence of the latter notion. This perspective also provides various frame definability and axiomatiza…
