计算机科学中的逻辑

Since their appearance in the 1950s, computational models capable of performing probabilistic choices have received wide attention and are nowadays pervasive in almost every areas of computer science. Their development was also inextricably…

We introduce Clerical, a programming language for exact real-number computation that combines first-order imperative-style programming with a limit operator for computation of real numbers as limits of Cauchy sequences. We address the…

The $\lambda\mu$-calculus plays a central role in the theory of programming languages as it extends the Curry-Howard correspondence to classical logic. A major drawback is that it does not satisfy B\"ohm's Theorem and it lacks the…

We prove the Stability Property for the call-by-value $\lambda$-calculus (CbV in the following). This result states necessary conditions under which the contexts of the CbV $\lambda$-calculus commute with intersections of approximants. This…

We look at the proofs of a fragment of Linear Logic as a whole: in fact, Linear Logic's coherent semantics interprets the proofs of a given formula $A$ as faces of an abstract simplicial complex, thus allowing us to see the set of the…

Preference Inference involves inferring additional user preferences from elicited or observed preferences, based on assumptions regarding the form of the user's preference relation. In this paper we consider a situation in which…

As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the challenges in this domain is to translate proofs written in…

Counting the number of models of a Boolean formula is a fundamental problem in artificial intelligence and reasoning. Minimal models of a Boolean formula are critical in various reasoning systems, making the counting of minimal models…

In this paper we propose a many-valued temporal conditional logic. We start from a many-valued logic with typicality, and extend it with the temporal operators of the Linear Time Temporal Logic (LTL), thus providing a formalism which is…

This invited paper is a passionate pitch for the significance of logic in scientific education. Logic helps focus on the essential core to identify the foundations of ideas and provides corresponding longevity with the resulting approach to…

We consider the reachability problem for higher-order functional programs and study the relationship between reachability games (i.e., the reachability problem for programs with angelic and demonic nondeterminism) and may-reachability…

The A-hierarchy is a parametric analogue of the polynomial hierarchy in the context of paramterised complexity theory. We give a new characterisation of the A-hierarchy in terms of a generalisation of the SUBSET-SUM problem.

Proof-theoretic semantics (P-tS) is the approach to meaning in logic based on 'proof' (as opposed to 'truth'). There are two major approaches to P-tS: proof-theoretic validity (P-tV) and base-extension semantics (B-eS). The former is a…

Definite descriptions, such as 'the General Chair of KR 2024', are a semantically transparent device for object identification in knowledge representation. In first-order modal logic, definite descriptions have been widely investigated for…

Clones of operations of arity omega (referred to as omega-operations) have been employed by Neumann to represent varieties of infinitary algebras defined by operations of at most arity omega. More recently, clone algebras have been…

We present efficient circuits for the addition of binary numbers. We assume that we are given arrival times for all input bits and optimize the delay of the circuits, i.e.\ the time when the last output bit is computed. This contains the…

First-order logic, and quantifiers in particular, are widely used in deductive verification. Quantifiers are essential for describing systems with unbounded domains, but prove difficult for automated solvers. Significant effort has been…

We consider the following decision problem: given two simply typed $\lambda$-terms, are they $\beta$-convertible? Equivalently, do they have the same normal form? It is famously non-elementary, but the precise complexity - namely…

We investigate a number of semantically defined fragments of Tarski's algebra of binary relations, including the function-preserving fragment. We address the question whether they are generated by a finite set of operations. We obtain…

In this paper we develop a novel mathematical formalism for the modeling of neural information networks endowed with additional structure in the form of assignments of resources, either computational or metabolic or informational. The…