Kripke Semantics for Intersection Formulas

We propose a notion of the Kripke-style model for intersection logic. Using a game interpretation, we prove soundness and completeness of the proposed semantics. In other words, a formula is provable (a type is inhabited) if and only if it is forced in every model. As a by-product, we obtain another proof of normalization for the Barendregt–Coppo–Dezani intersection type assignment system.

Tableaux for essence and contingency

Logic Journal of IGPL ◽

10.1093/jigpal/jzaa016 ◽

2020 ◽

Author(s):

Giorgio Venturi ◽

Pedro Teixeira Yago

Keyword(s):

Kripke Semantics ◽

Normal Operators ◽

Abstract We offer tableaux systems for logics of essence and accident and logics of non-contingency, showing their soundness and completeness for Kripke semantics. We also show an interesting parallel between these logics based on the semantic insensitivity of the two non-normal operators by which these logics are expressed.

EVERYONE KNOWS THAT SOMEONE KNOWS: QUANTIFIERS OVER EPISTEMIC AGENTS

The Review of Symbolic Logic ◽

10.1017/s1755020318000497 ◽

2019 ◽

Vol 12 (2) ◽

pp. 255-270 ◽

Cited By ~ 1

Author(s):

PAVEL NAUMOV ◽

JIA TAO

Keyword(s):

Modal Logic ◽

Epistemic Logic ◽

Possible Worlds ◽

Completeness Theorem ◽

Kripke Semantics ◽

Possible Worlds Semantics ◽

Distributed Knowledge ◽

First Order ◽

First Order Modal Logic

AbstractModal logic S5 is commonly viewed as an epistemic logic that captures the most basic properties of knowledge. Kripke proved a completeness theorem for the first-order modal logic S5 with respect to a possible worlds semantics. A multiagent version of the propositional S5 as well as a version of the propositional S5 that describes properties of distributed knowledge in multiagent systems has also been previously studied. This article proposes a version of S5-like epistemic logic of distributed knowledge with quantifiers ranging over the set of agents, and proves its soundness and completeness with respect to a Kripke semantics.

A cut-free labelled sequent calculus for dynamic epistemic logic

Journal of Logic and Computation ◽

10.1093/logcom/exaa014 ◽

2020 ◽

Vol 30 (1) ◽

pp. 321-348

Author(s):

Shoshin Nomura ◽

Hiroakira Ono ◽

Katsuhiko Sano

Keyword(s):

Modal Logic ◽

Epistemic Logic ◽

Sequent Calculus ◽

Dynamic Epistemic Logic ◽

Kripke Semantics ◽

Cut Rule ◽

Public Announcement ◽

Public Announcement Logic ◽

Labelled Sequent Calculus

Abstract Dynamic epistemic logic is a logic that is aimed at formally expressing how a person’s knowledge changes. We provide a cut-free labelled sequent calculus ($\textbf{GDEL}$) on the background of existing studies of Hilbert-style axiomatization $\textbf{HDEL}$ of dynamic epistemic logic and labelled calculi for public announcement logic. We first show that the $cut$ rule is admissible in $\textbf{GDEL}$ and show that $\textbf{GDEL}$ is sound and complete for Kripke semantics. Moreover, we show that the basis of $\textbf{GDEL}$ is extended from modal logic K to other familiar modal logics including S5 with keeping the admissibility of cut, soundness and completeness.

A Logic for Vagueness

The Australasian Journal of Logic ◽

10.26686/ajl.v8i0.1815 ◽

2010 ◽

Vol 8 ◽

Cited By ~ 1

Author(s):

John Slaney

Keyword(s):

Natural Deduction ◽

Kripke Semantics ◽

Substructural Logic ◽

Relational Semantics ◽

Deduction System ◽

First Order ◽

Natural Deduction System ◽

Propositional System

This paper presents F, substructural logic designed to treat vagueness. Weaker than Lukasiewicz’s infinitely valued logic, it is presented first in a natural deduction system, then given a Kripke semantics in the manner of Routley and Meyer's ternary relational semantics for R and related systems, but in this case, the points are motivated as degrees to which the truth could be stretched. Soundness and completeness are proved, not only for the propositional system, but also for its extension with first-order quantifiers. The first-order models allow not only objects with vague properties, but also objects whose very existence is a matter of degree.

Kripke-style Semantics and Completeness for Full Simply Typed Lambda Calculus

Journal of Logic and Computation ◽

10.1093/logcom/exaa055 ◽

2020 ◽

Vol 30 (8) ◽

pp. 1567-1608

Author(s):

Simona Kašterović ◽

Silvia Ghilezan

Keyword(s):

Lambda Calculus ◽

Canonical Model ◽

Typed Lambda Calculus ◽

Type Assignment ◽

Abstract Full simply typed lambda calculus is the simply typed lambda calculus extended with product types and sum types. We propose a Kripke-style semantics for full simply typed lambda calculus. We then prove soundness and completeness of type assignment in full simply typed lambda calculus with respect to the proposed semantics. The key point in the proof of completeness is the notion of a canonical model.

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence ◽

Intuitionistic Layered Graph Logic

10.24963/ijcai.2017/673 ◽

2017 ◽

Author(s):

Simon Docherty ◽

David Pym

Keyword(s):

Social Sciences ◽

Complex Systems ◽

Completeness Theorem ◽

Kripke Semantics ◽

Substructural Logic ◽

Graph Theoretic ◽

The Relationship ◽

Layered Graph

Models of complex systems are widely used in the physical and social sciences, and the concept of layering, typically building upon graph-theoretic structure, is a common feature. We describe an intuitionistic substructural logic that gives an account of layering. As in other bunched systems, the logic includes the usual intuitionistic connectives, together with a non-commutative, non-associative conjunction (used to capture layering) and its associated implications. We give a soundness and completeness theorem for a labelled tableaux system with respect to a Kripke semantics on graphs. To demonstrate the utility of the logic, we show how to represent systems and security examples, illuminating the relationship between services/policies and the infrastructures/architectures to which they are applied.

Dynamic Łukasiewicz logic and its application to immune system

Soft Computing ◽

10.1007/s00500-021-05955-3 ◽

2021 ◽

Author(s):

Antonio Di Nola ◽

Revaz Grigolia ◽

Nunu Mitskevich ◽

Gaetano Vitale

Keyword(s):

Immune System ◽

Scalar Multiplication ◽

Kripke Semantics ◽

Łukasiewicz Logic ◽

Lukasiewicz Logic ◽

Regular Algebras

AbstractIt is introduced an immune dynamic n-valued Łukasiewicz logic $$ID{\L }_n$$ I D Ł n on the base of n-valued Łukasiewicz logic $${\L }_n$$ Ł n and corresponding to it immune dynamic $$MV_n$$ M V n -algebra ($$IDL_n$$ I D L n -algebra), $$1< n < \omega $$ 1 < n < ω , which are algebraic counterparts of the logic, that in turn represent two-sorted algebras $$(\mathcal {M}, \mathcal {R}, \Diamond )$$ ( M , R , ◊ ) that combine the varieties of $$MV_n$$ M V n -algebras $$\mathcal {M} = (M, \oplus , \odot , \sim , 0,1)$$ M = ( M , ⊕ , ⊙ , ∼ , 0 , 1 ) and regular algebras $$\mathcal {R} = (R,\cup , ;, ^*)$$ R = ( R , ∪ , ; , ∗ ) into a single finitely axiomatized variety resembling R-module with “scalar” multiplication $$\Diamond $$ ◊ . Kripke semantics is developed for immune dynamic Łukasiewicz logic $$ID{\L }_n$$ I D Ł n with application in immune system.

Type Inference: Some Results, Some Problems1

Fundamenta Informaticae ◽

10.3233/fi-1993-191-205 ◽

1993 ◽

Vol 19 (1-2) ◽

pp. 87-125

Author(s):

Paola Giannini ◽

Furio Honsell ◽

Simona Ronchi Della Rocca

Keyword(s):

Large Class ◽

Higher Order ◽

Type Inference ◽

Principal Type ◽

Open Problems ◽

Inference Problem ◽

Type Assignment ◽

Unification Problem

In this paper we investigate the type inference problem for a large class of type assignment systems for the λ-calculus. This is the problem of determining if a term has a type in a given system. We discuss, in particular, a collection of type assignment systems which correspond to the typed systems of Barendregt’s “cube”. Type dependencies being shown redundant, we focus on the strongest of all, Fω, the type assignment version of the system Fω of Girard. In order to manipulate uniformly type inferences we give a syntax directed presentation of Fω and introduce the notions of scheme and of principal type scheme. Making essential use of them, we succeed in reducing the type inference problem for Fω to a restriction of the higher order semi-unification problem and in showing that the conditional type inference problem for Fω is undecidable. Throughout the paper we call attention to open problems and formulate some conjectures.

An Automata-Theoretic Decision Procedure for Propositional Temporal Logic with Since and Until1

Fundamenta Informaticae ◽

10.3233/fi-1992-17307 ◽

1992 ◽

Vol 17 (3) ◽

pp. 271-282

Author(s):

Y.S. Ramakrishna ◽

L.E. Moser ◽

L.K. Dillon ◽

P.M. Melliar-Smith ◽

G. Kutty

Keyword(s):

Temporal Logic ◽

Decision Procedure ◽

Linear Time ◽

Computer Systems ◽

Hierarchical Abstraction ◽

We present an automata-theoretic decision procedure for Since/Until Temporal Logic (SUTL), a linear-time propositional temporal logic with strong non-strict since and until operators. The logic, which is intended for specifying and reasoning about computer systems, employs neither next nor previous operators. Such operators obstruct the use of hierarchical abstraction and refinement and make reasoning about concurrency difficult. A proof of the soundness and completeness of the decision procedure is given, and its complexity is analyzed.

Deduction in Non-Fregean Propositional Logic SCI

Axioms ◽

10.3390/axioms8040115 ◽

2019 ◽

Vol 8 (4) ◽

pp. 115 ◽

Cited By ~ 1

Author(s):

Joanna Golińska-Pilarek ◽

Magdalena Welle

Keyword(s):

Propositional Logic ◽

Sequent Calculus ◽

Classical Propositional Logic ◽

Tableau System ◽

We study deduction systems for the weakest, extensional and two-valued non-Fregean propositional logic SCI . The language of SCI is obtained by expanding the language of classical propositional logic with a new binary connective ≡ that expresses the identity of two statements; that is, it connects two statements and forms a new one, which is true whenever the semantic correlates of the arguments are the same. On the formal side, SCI is an extension of classical propositional logic with axioms characterizing the identity connective, postulating that identity must be an equivalence and obey an extensionality principle. First, we present and discuss two types of systems for SCI known from the literature, namely sequent calculus and a dual tableau-like system. Then, we present a new dual tableau system for SCI and prove its soundness and completeness. Finally, we discuss and compare the systems presented in the paper.