Related papers: Nominal Logic with Equations Only
Consequence-based reasoning can be used to construct proofs that explain entailments of description logic (DL) ontologies. In the literature, one can find multiple consequence-based calculi for reasoning in the $\mathcal{EL}$ family of DLs,…
Our goal is a modern approach to answering questions via systematic reasoning where answers are supported by human interpretable proof trees grounded in an NL corpus of authoritative facts. Such a system would help alleviate the challenges…
Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first argument does not suffice to determine the value of the expression. In programming, short-circuit…
While there is a long tradition of reasoning about (non)termination in program analysis, specialized logics are typically needed to give different termination criteria. This includes partial correctness, where termination is not guaranteed,…
Permissive-Nominal Logic (PNL) extends first-order predicate logic with term-formers that can bind names in their arguments. It takes a semantics in (permissive-)nominal sets. In PNL, the forall-quantifier or lambda-binder are just…
The so-called light logics have been introduced as logical systems enjoying quite remarkable normalization properties. Designing a type assignment system for pure lambda calculus from these logics, however, is problematic. In this paper we…
HyLL (Hybrid Linear Logic) and SELL (Subexponential Linear Logic) are logical frameworks that have been extensively used for specifying systems that exhibit modalities such as temporal or spatial ones. Both frameworks have linear logic (LL)…
We propose a novel framework seamlessly providing key properties of both neural nets (learning) and symbolic logic (knowledge and reasoning). Every neuron has a meaning as a component of a formula in a weighted real-valued logic, yielding a…
Most non-classical logics are subclassical, that is, every inference/theorem they validate is also valid classically. A notable exception is the three-valued propositional Logic of Ordinary Discourse (OL) proposed and extensively motivated…
We present a novel unity of logic, viz., a single sequent calculus that embodies classical, intuitionistic and linear logics. Concretely, we define classical linear logic negative (CLL$^-$), a new logic that is classical and linear yet…
This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, first-order intuitionistic logic with non-constant domains and first-order intuitionistic logic with constant domains. It is…
We propose a new formalism for specifying and reasoning about problems that involve heterogeneous "pieces of information" -- large collections of data, decision procedures of any kind and complexity and connections between them. The essence…
Call a semantics for a language with variables absolute when variables map to fixed entities in the denotation. That is, a semantics is absolute when the denotation of a variable a is a copy of itself in the denotation. We give a trio of…
We show the functional completeness for the connectives of the non-trivial negation inconsistent logic C by using a well-established method implementing purely proof-theoretic notions only. Firstly, given that C contains a strong negation,…
In this paper, we delve into Notation3 Logic (N3), an extension of RDF, which empowers users to craft rules introducing fresh blank nodes to RDF graphs. This capability is pivotal in various applications such as ontology mapping, given the…
We define a model of predicate logic in which every term and predicate, open or closed, has an absolute denotation independently of a valuation of the variables. For each variable a, the domain of the model contains an element [[a]] which…
We advocate a declarative approach to proving properties of logic programs. Total correctness can be separated into correctness, completeness and clean termination; the latter includes non-floundering. Only clean termination depends on the…
Program logics for bug-finding (such as the recently introduced Incorrectness Logic) have framed correctness and incorrectness as dual concepts requiring different logical foundations. In this paper, we argue that a single unified theory…
Equational reasoning with string diagrams provides an intuitive means of proving equations between morphisms in a symmetric monoidal category. This can be extended to proofs of infinite families of equations using a simple graphical syntax…
We present a comprehensive programme analysing the decomposition of proof systems for non-classical logics into proof systems for other logics, especially classical logic, using an algebra of constraints. That is, one recovers a proof…