Related papers: Classical BI: Its Semantics and Proof Theory
The present paper provides an analysis of the existing proof systems for dynamic epistemic logic from the viewpoint of proof-theoretic semantics. Dynamic epistemic logic is one of the best known members of a family of logical systems which…
Modelling and reasoning about dynamic memory allocation is one of the well-established strands of theoretical computer science, which is particularly well-known as a source of notorious challenges in semantics, reasoning, and proof theory.…
The work is devoted to Computability Logic (CoL) -- the philosophical/mathematical platform and long-term project for redeveloping classical logic after replacing truth} by computability in its underlying semantics (see…
We propose a model of the substructural logic of Bunched Implications (BI) that is suitable for reasoning about quantum states. In our model, the separating conjunction of BI describes separable quantum states. We develop a program logic…
We develop a classical propositional logic for reasoning about combinatory logic. We define its syntax, axiomatic system and semantics. The syntax and axiomatic system are presented based on classical propositional logic, with typed…
The logic of Dependence and Independence Bunched Implications (DIBI) is a logic to reason about conditional independence (CI); for instance, DIBI formulas can characterise CI in probability distributions and relational databases, using the…
Combinatory logic shows that bound variables can be eliminated without loss of expressiveness. It has applications both in the foundations of mathematics and in the implementation of functional programming languages. The original…
We define an extension of predicate logic, called Binding Logic, where variables can be bound in terms and in propositions. We introduce a notion of model for this logic and prove a soundness and completeness theorem for it. This theorem is…
We present a process semantics for the purely additive fragment of linear logic in which formulas denote protocols and (equivalence classes of) proofs denote multi-channel concurrent processes. The polycategorical model induced by this…
This paper represents classical propositional proofs as *combinatorial proofs*, which are more abstract than proof nets: superposition (contraction/weakening) is modelled mathematically, as a lax form of fibration, rather than syntactically…
Curved Boolean Logic (CBL) generalizes propositional logic by allowing local truth assignments that do not extend to a single global valuation, analogous to curvature in geometry. We give equivalent sheaf and exclusivity-graph semantics and…
Concept Bottleneck Models (CBMs) provide a basis for semantic abstractions within a neural network architecture. Such models have primarily been seen through the lens of interpretability so far, wherein they offer transparency by inferring…
Abstract separation logics are a family of extensions of Hoare logic for reasoning about programs that manipulate resources such as memory locations. These logics are "abstract" because they are independent of any particular concrete…
The paper is a contribution both to the theoretical foundations and to the actual construction of efficient automatizable proof procedures for non-classical logics. We focus here on the case of finite-valued logics, and exhibit: (i) a…
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…
Uniform proofs are sequent calculus proofs with the following characteristic: the last step in the derivation of a complex formula at any stage in the proof is always the introduction of the top-level logical symbol of that formula. We…
We present a substructural epistemic logic, based on Boolean BI, in which the epistemic modalities are parametrized on agents' local resources. The new modalities can be seen as generalizations of the usual epistemic modalities. The logic…
We extend classical Propositional Logic (PL) by adding a new primitive binary connective $\varphi|\psi$, intended to represent the "superposition" of sentences $\varphi$ and $\psi$, an operation motivated by the corresponding notion of…
Recent work proposed the computation of so-called PI-explanations of Naive Bayes Classifiers (NBCs). PI-explanations are subset-minimal sets of feature-value pairs that are sufficient for the prediction, and have been computed with…
We introduce a functional calculus with simple syntax and operational semantics in which the calculi introduced so far in the Curry-Howard correspondence for Classical Logic can be faithfully encoded. Our calculus enjoys confluence without…