计算机科学中的逻辑

In response to a concern raised by Horty, this paper develops a two-tiered, preference-based semantic framework for modeling defeasible conditional obligations. The paper extends a Hansson-Lewis style preference semantics for dyadic deontic…

We study the problem of fitting a description logic (DL) ontology to a given set of positive and negative examples that take the form of an ABox and a Boolean query. While previous work has investigated this problem for the expressive DLs…

Token identity is semantic information for measurement-bearing expressions. Intervals, dimension tags, and token-erased syntax can say what values a measured leaf may take, but they cannot say whether two occurrences name the same…

We present a graded modal type theory, a dependent type theory with grades that can be used to enforce various properties of the code. The theory has $\Pi$-types, weak and strong $\Sigma$-types, natural numbers, an empty type, and a…

To ensure decidability and consistency of its type theory, a proof assistant should only accept terminating recursive functions and productive corecursive functions. Most proof assistants enforce this through syntactic conditions, which can…

Consider a community of scientists whose labs are each capable of conducting a different set of experiments. The scientists want to work together to confirm a new hypothesis, but to ensure blindness, their labs generally prohibit the…

Approximation semantics capture the observable behaviour of {\lambda}-terms, with B\"ohm Trees and Taylor Expansion standing as two central paradigms. Although conceptually different, these notions are related via the Commutation Theorem,…

In this paper, we show that the equational theory of relational Kleene algebra with the \emph{graph loop} operator (a.k.a.~\emph{fixset}) is \textsc{PSpace}-complete. Here, the graph loop is the unary operator that restricts a binary…

Covering spaces are a fundamental tool in algebraic topology because of the close relationship they bear with the fundamental groups of spaces. Indeed, they are in correspondence with the subgroups of the fundamental group: this is known as…

Homotopy type theory is a logical setting based on Martin-L\"of type theory in which geometric constructions and proofs can be carried out synthetically. Here, types can be interpreted as spaces up to homotopy, and proofs as…

We investigate practical algorithms for inconsistency-tolerant query answering over prioritized knowledge bases, which consist of a logical theory, a set of facts, and a priority relation between conflicting facts. We consider three…

A semantic model enjoys full definability if every semantic element in the model is a denotation of some proof or program. Full definability indicates that the model captures programs and proofs in a highly detailed manner. This paper…

Runtime verification is a lightweight verification technique that complements model checking by analyzing system executions at runtime rather than exploring a complete system model in advance. It is particularly useful for partially…

Robust Markov decision processes (RMDPs) extend standard Markov decision processes (MDPs) to account for uncertainty in the transition probabilities. RMDPs have an uncertainty set that defines a set of possible transition functions, each of…

Zero-knowledge proofs (ZKPs) are an emerging technology that has become the solution to efficiently provide security and privacy along with the transparency requirement of blockchains. ZKPs are usually expressed by means of arithmetic…

Rewriting Induction (RI) is a formal system in term rewriting to establish program equivalence. The recently defined Bounded RI for higher-order Logically Constrained Term Rewriting Systems (LCSTRSs) yields a convenient proof system for…

We study the expressive power of First-Order Logic (\FO) over (unordered) infinite trees, with the aim of identifying robust characterisations in terms of branching-time specification formalisms. While such correspondences are well…

Autonomous agents acting in realistic Multi-Agent Systems (MAS) should be able to adapt during their execution. Standard strategic logics, such as Alternating-time Temporal Logic (ATL), model agents' state- or history-dependent behaviour.…

We are interested in proving input-output properties of functions that handle infinite data such as streams or non-wellfounded trees. We provide a finitary refinement type system which is (sound and) complete for Scott-open properties…

The relational semantics of linear logic is a powerful framework for defining resource-aware models of the $\lambda$-calculus. However, its quantitative aspects are not reflected in the preorders and equational theories induced by these…