Team semantics is the mathematical basis of modern logics of dependence and independence. In contrast to classical Tarski semantics, a formula is evaluated not for a single assignment of values to the free variables, but on a set of such assignments, called a team. Team semantics is appropriate for a purely logical understanding of dependency notions, where only the presence or absence of data matters, but based on sets, it does not take into account multiple occurrences of data values. It is therefore insufficient in scenarios where such multiplicities matter, in particular for reasoning about probabilities and statistical independencies. Therefore, an extension from teams to multiteams (i.e. multisets of assignments) has been proposed by several authors.
In this paper we aim at a systematic development of logics of dependence and independence based on multiteam semantics. We study atomic dependency properties of finite multiteams and discuss the appropriate meaning of logical operators to extend the atomic dependencies to full-fledged logics for reasoning about dependence properties in a multiteam setting. We explore properties and expressive power of a wide spectrum of different multiteam logics and compare them to logics with team semantics. We also study the relationship of logics with multiteam semantics with existential second-order logic for a specific class of metafinite structures. It turns out that inclusion-exclusion logic can be characterised in a precise sense by the Presburger fragment of this logic, but for capturing independence, we need to go beyond it and add some form of multiplication. Finally we also consider multiteams with weights in the reals and study the expressive power of formulae by means of topological properties.
We define a variant of team semantics called multiteam semantics based on multisets and study the properties of various logics in this framework. In particular, we define natural probabilistic versions of inclusion and independence atoms and certain approximation operators motivated by approximate dependence atoms of Väänänen.
In 1952 P. F. Strawson proposed a logic of presuppositions. It is an interpretation of Aristotelian logic, i.e. of the logic of the traditional syllogism. In 1981 Richard Diaz published a monograph in which he presented truth-relevant logic. This paper shows that truth-relevant logic is but a propositional version of the logic of presuppositions. A semantics of the logic of presuppositions is developed using truth-relevant logic. The semantics is then further extended to polyadic logic and some consequences discussed.
Logic programming with fixed-point definitions is a useful extension of traditional logic programming. Fixed-point definitions can capture simple model checking problems and closed-world assumptions. Its operational semantics is typically based on intuitionistic provability. We extend the operational semantics of these languages with game semantics. This extended semantics has several interesting aspects: in particular, it gives a logical status to the $read$ predicate.
Logics of non-sense allow a third truth value to express propositions that are \emph{nonsense}. These logics are ideal formalisms to understand how errors are handled in programs and how they propagate throughout the programs once they appear. In this paper, we give a Hintikkan game semantics for logics of non-sense and prove its correctness. We also discuss how a known solution method in game theory, the iterated elimination of strictly dominated strategies, relates to semantic games for logics of nonsense. Finally, we extend the logics of nonsense only by means of semantic games, developing …
Inductions and game semantics are two useful extensions to traditional logic programming. To be specific, inductions can capture a wider class of provable formulas in logic programming. Adopting game semantics can make logic programming more interactive. In this paper, we propose an execution model for a logic language with these features. This execution model follows closely the reasoning process in real life.
Defeasible logic is an efficient logic for defeasible reasoning. It is defined through a proof theory and, until now, has had no model theory. In this paper a model-theoretic semantics is given for defeasible logic. The logic is sound and complete with respect to the semantics. We also briefly outline how this approach extends to a wide range of defeasible logics.
We use modal logic as a framework for coalgebraic trace semantics, and show the flexibility of the approach with concrete examples such as the language semantics of weighted, alternating and tree automata, and the trace semantics of generative probabilistic systems. We provide a sufficient condition under which a logical semantics coincides with the trace semantics obtained via a given determinization construction. Finally, we consider a condition that guarantees the existence of a canonical determinization procedure that is correct with respect to a given logical semantics. That procedure is …
Game semantics and winning strategies offer a potential conceptual bridge between semantics and proof systems of logics. We illustrate this link for hybrid logic -- an extension of modal logic that allows for explicit reference to worlds within the language. The main result is that the systematic search of winning strategies over all models can be finitized and thus reformulated as a proof system.
In this paper we introduce a new logical foundation of SAND attack trees in intuitionistic linear logic. This new foundation is based on a new logic called the Attack Tree Linear Logic (ATLL). Before introducing ATLL we given several new logical models of attack trees, the first, is a very basic model based in truth tables. Then we lift this semantics into a semantics of attack trees based on lineales which introduces implication, but this can be further lifted into a dialectica model which ATLL is based. One important feature of ATLL is that it supports full distributivity of sequential conju…
A propositional logic program $P$ may be identified with a $P_fP_f$-coalgebra on the set of atomic propositions in the program. The corresponding $C(P_fP_f)$-coalgebra, where $C(P_fP_f)$ is the cofree comonad on $P_fP_f$, describes derivations by resolution. Using lax semantics, that correspondence may be extended to a class of first-order logic programs without existential variables. The resulting extension captures the proofs by term-matching resolution in logic programming. Refining the lax approach, we further extend it to arbitrary logic programs. We also exhibit a refinement of Bonchi an…
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. Definit…
Category theory can be used to state formulas in First-Order Logic without using set membership. Several notable results in logic such as proof of the continuum hypothesis can be elegantly rewritten in category theory. We propose in this paper a reformulation of the usual set-theoretical semantics of the description logic $\mathcal{ALC}$ by using categorical language. In this setting, ALC concepts are represented as objects, concept subsumptions as arrows, and memberships as logical quantifiers over objects and arrows of categories. Such a category-theoretical semantics provides a more modular…
Team semantics is the mathematical framework of modern logics of dependence and independence in which formulae are interpreted by sets of assignments (teams) instead of single assignments as in first-order logic. In order to deepen the fruitful interplay between team semantics and database dependency theory, we define "Polyteam Semantics" in which formulae are evaluated over a family of teams. We begin by defining a novel polyteam variant of dependence atoms and give a finite axiomatisation for the associated implication problem. We relate polyteam semantics to team semantics and investigate i…
There are various interesting semantics' (extensions) designed for argumentation frameworks. They enable to assign a meaning, e.g., to odd-length cycles. Our main motivation is to transfer semantics' proposed by Baroni, Giacomin and Guida for argumetation frameworks with odd-length cycles to logic programs with odd-length cycles through default negation. The developed construction is even stronger. For a given logic program an argumentation framework is defined. The construction enables to transfer each semantics of the resulting argumentation framework to a semantics of the given logic progra…
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…
We refine HO/N game semantics with an additional notion of pointer (mu-pointers) and extend it to first-order classical logic with completeness results. We use a Church style extension of Parigot's lambda-mu-calculus to represent proofs of first-order classical logic. We present some relations with Krivine's classical realizability and applications to type isomorphisms.
Deductive verification techniques based on program logics (i.e., the family of Floyd-Hoare logics) are a powerful approach for program reasoning. Recently, there has been a trend of increasing the expressive power of such logics by augmenting their rules with additional information to reason about program side-effects. For example, general program logics have been augmented with cost analyses, logics for probabilistic computations have been augmented with estimate measures, and logics for differential privacy with indistinguishability bounds. In this work, we unify these various approaches via…
This note points out a lemma on closures of monotonic increasing functions and shows how it is applicable to decomposition and modularity for semantics defined as the least fixedpoint of some monotonic function. In particular it applies to numerous semantics of logic programs. An appendix addresses the fixedpoints of (possibly non-monotonic) functions that are sandwiched between functions with the same fixedpoints.
Bialgebrae provide an abstract framework encompassing the semantics of different kinds of computational models. In this paper we propose a bialgebraic approach to the semantics of logic programming. Our methodology is to study logic programs as reactive systems and exploit abstract techniques developed in that setting. First we use saturation to model the operational semantics of logic programs as coalgebrae on presheaves. Then, we make explicit the underlying algebraic structure by using bialgebrae on presheaves. The resulting semantics turns out to be compositional with respect to conjunctio…
This article presents a computational semantics for classical logic using constructive type theory. Such semantics seems impossible because classical logic allows the Law of Excluded Middle (LEM), not accepted in constructive logic since it does not have computational meaning. However, the apparently oracular powers expressed in the LEM, that for any proposition P either it or its negation, not P, is true can also be explained in terms of constructive evidence that does not refer to "oracles for truth." Types with virtual evidence and the constructive impossibility of negative evidence provide…
A specification given as a formula in linear temporal logic (LTL) defines a system by its set of traces. However, certain features such as information flow security constraints are rather modeled as so-called hyperproperties, which are sets of sets of traces. One logical approach to this is team logic, which is a logical framework for the specification of dependence and independence of information. LTL with team semantics has recently been discovered as a logic for hyperproperties. We study the complexity theoretic aspects of LTL with so-called synchronous team semantics and Boolean negation, …
The modal systems S1--S3 were introduced by C. I. Lewis as logics for strict implication. While there are Kripke semantics for S2 and S3, there is no known natural semantics for S1. We extend S1 by a Substitution Principle SP which generalizes a reference rule of S1. In system S1+SP, the relation of strict equivalence $φ\equivψ$ satisfies the identity axioms of R. Suszko's non-Fregean logic adapted to the language of modal logic (we call these axioms the axioms of propositional identity). This enables us to develop a framework of algebraic semantics which captures S1+SP as well as the Lewis sy…
Justification logic is a term used to identify a relatively new family of modal-like logics. There is an established literature about propositional justification logic, but incursions on the first-order case are scarce. In this paper we present a constant domain semantics for the first-order logic of proofs with the Barcan Formula (FOLPb); then we prove Soundness and Completeness Theorems. A monotonic semantics for a version of this logic without the Barcan Formula is already in the literature, but constant domains requires substantial new machinery, which may prove useful in other contexts as…
We address the problem of integrating information coming from different sources. The information consists of facts that a central server collects and tries to combine using (a) a set of logical rules, i.e. a logic program, and (b) a hypothesis representing the server's own estimates. In such a setting incomplete information from a source or contradictory information from different sources necessitate the use of many-valued logics in which programs can be evaluated and hypotheses can be tested. To carry out such activities we propose a formal framework based on bilattices such as Belnap's four-…
In this paper we provide a simplified semantics for the logic KD45(G), i.e. the many-valued Gödel counterpart of the classical modal logic KD45. More precisely, we characterize KD45(G) as the set of valid formulae of the class of possibilistic Gödel Kripke Frames $\langle W,π\rangle$, where $W$ is a non-empty set of worlds and $π: W \longrightarrow [0, 1]$ is a normalized possibility distribution on $W$.
Cathoristic logic is a multi-modal logic where negation is replaced by a novel operator allowing the expression of incompatible sentences. We present the syntax and semantics of the logic including complete proof rules, and establish a number of results such as compactness, a semantic characterisation of elementary equivalence, the existence of a quadratic-time decision procedure, and Brandom's incompatibility semantics property. We demonstrate the usefulness of the logic as a language for knowledge representation.
Verifiers and Generators: Epistemic Semantics for Intuitionistic Logic (Long Version)
Universidad Nacional de Quilmes (CONICET)（基尔梅斯国立大学（国家科学研究和技术委员会））；Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires（布宜诺斯艾利斯大学自然科学学院计算系）
Complete Heyting Algebra Semantics for an Intuitionistic Version of Matching Logic (Extended Abstract)
Research Center for Logic, Optimization and Security (LOS), University of Bucharest（布加勒斯特大学逻辑、优化与安全研究中心）；Institute for Logic and Data Science, Bucharest（布加勒斯特逻辑与数据科学研究所）
There is a growing need for abstractions in logic specification languages such as FO(.) and ASP. One technique to achieve these abstractions are templates (sometimes called macros). While the semantics of templates are virtually always described through a syntactical rewriting scheme, we present an alternative view on templates as second order definitions. To extend the existing definition construct of FO(.) to second order, we introduce a powerful compositional framework for defining logics by modular integration of logic constructs specified as pairs of one syntactical and one semantical ind…
The primary goal of this paper is to present a unified way to transform the syntax of a logic system into certain initial algebraic structure so that it can be studied algebraically. The algebraic structures which one may choose for this purpose are various clones over a full subcategory of a category. We show that the syntax of equational logic, lambda calculus and first order logic can be represented as clones or right algebras of clones over the set of positive integers. The semantics is then represented by structures derived from left algebras of these clones.
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 …
We show how to give a coherent semantics to programs that are well-specified in a version of separation logic for a language with higher types: idealized algol extended with heaps (but with immutable stack variables). In particular, we provide simple sound rules for deriving higher-order frame rules, allowing for local reasoning.
In this paper we explore a unifying approach --- that of hypotheses assumption --- as a means to provide a semantics for all Normal Logic Programs (NLPs), the Minimal Hypotheses (MH) semantics. This semantics takes a positive hypotheses assumption approach as a means to guarantee the desirable properties of model existence, relevance and cumulativity, and of generalizing the Stable Models in the process. To do so we first introduce the fundamental semantic concept of minimality of assumed positive hypotheses, define the MH semantics, and analyze the semantics' properties and applicability. Ind…
In [17], we introduced a modal logic, called $L$, which combines intuitionistic propositional logic $IPC$ and classical propositional logic $CPC$ and is complete w.r.t. an algebraic semantics. However, $L$ seems to be too weak for Kripke-style semantics. In this paper, we add positive and negative introspection and show that the resulting logic $L5$ has a Kripke semantics. For intermediate logics $I$, we consider the parametrized versions $L5(I)$ of $L5$ where $IPC$ is replaced by $I$. $L5(I)$ can be seen as a classical modal logic for the reasoning about truth in $I$. From our results, we der…
We study the data complexity of model-checking for logics with team semantics. We focus on dependence, inclusion, and independence logic formulas under both strict and lax team semantics. Our results delineate a clear tractability/intractability frontiers in data complexity of both quantifier-free and quantified formulas for each of the logics. For inclusion logic under the lax semantics, we reduce the model-checking problem to the satisfiability problem of so-called dual-Horn Boolean formulas. Via this reduction, we give an alternative proof for the known result that the data complexity of in…
Henkin, Monk and Tarski gave a compositional semantics for first-order predicate logic. We extend this work by including function symbols in the language and by giving the denotation of the atomic formula as a composition of the denotations of its predicate symbol and of its tuple of arguments. In addition we give the denotation of a term as a composition of the denotations of its function symbol and of its tuple of arguments.
In this paper, we define a multi-type calculus for inquisitive logic, which is sound, complete and enjoys Belnap-style cut-elimination and subformula property. Inquisitive logic is the logic of inquisitive semantics, a semantic framework developed by Groenendijk, Roelofsen and Ciardelli which captures both assertions and questions in natural language. Inquisitive logic is sound and complete w.r.t. the so-called state semantics (also known as team semantics). The Hilbert-style presentation of inquisitive logic is not closed under uniform substitution; indeed, some occurrences of formulas are re…
STIT (sees to it that) semantics is one of the most prominent tools in modal logic of agency, widely used among both philosophers and responsible AI scholars. STIT logic surveys the properties of agents seeing to it that some state of affairs holds without specifying concrete actions by which that state of affairs is guaranteed. In comparison with other multi-agent modal logics, the main advantage of STIT theories is expressive power. STIT logic allows to study not only statements about agents abilities to perform certain actions (as it is in variations of Coalition Logic or Propositional Dyna…
Authorization logics have been used in the theory of computer security to reason about access control decisions. In this work, a formal belief semantics for authorization logics is given. The belief semantics is proved to subsume a standard Kripke semantics. The belief semantics yields a direct representation of principals' beliefs, without resorting to the technical machinery used in Kripke semantics. A proof system is given for the logic; that system is proved sound with respect to the belief and Kripke semantics. The soundness proof for the belief semantics, and for a variant of the Kripke …
In [Ban97] a connection among rough sets (in particular, pre-rough algebras) and three-valued Łukasiewicz logic Ł3 is pointed out. In this paper we present a temporal like semantics for Nilpotent Minimum logic NM ([Fod95, EG01]), in which the logic of every instant is given by Ł3: a completeness theorem will be shown. This is the prosecution of the work initiated in [AGM08] and [ABM09], in which the authors construct a temporal semantics for the many-valued logics of Gödel ([Göd32], [Dum59]) and Basic Logic ([Háj98]).
We study the expressive power of fragments of inclusion and independence logic defined by restricting the number k of universal quantifiers in formulas. Assuming the so-called strict semantics for these logics, we relate these fragments of inclusion and independence logic to sublogics ESO_f(k\forall) of existential second-order logic, which in turn are known to capture the complexity classes NTIME_{RAM}(n^k).
Kripke frames (and models) provide a suitable semantics for sub-classical logics, for example Intuitionistic Logic (of Brouwer and Heyting) axiomatizes the reflexive and transitive Kripke frames (with persistent satisfaction relations), and the Basic Logic (of Visser) axiomatizes transitive Kripke frames (with persistent satisfaction relations). Here, we investigate whether Kripke frames/models could provide a semantics for fuzzy logics. For each axiom of the Basic Fuzzy Logic, necessary and sufficient conditions are sought for Kripke frames/models which satisfy them. It turns out that the onl…
This paper defines an argumentation semantics for extended logic programming and shows its equivalence to the well-founded semantics with explicit negation. We set up a general framework in which we extensively compare this semantics to other argumentation semantics, including those of Dung, and Prakken and Sartor. We present a general dialectical proof theory for these argumentation semantics.
