计算机科学中的逻辑

Common knowledge and only knowing capture two intuitive and natural notions that have proven to be useful in a variety of settings, for example to reason about coordination or agreement between agents, or to analyse the knowledge of…

Fixpoint operators are tools to reason on recursive programs and data types obtained by induction (e.g. lists, trees) or coinduction (e.g. streams). They were given a categorical treatment with the notion of categories with fixpoints. A…

Ext groups are fundamental objects from homological algebra which underlie important computations in homotopy theory. We formalise the theory of Yoneda Ext groups in homotopy type theory (HoTT) using the Coq-HoTT library. This is an…

In this paper we define and study a multi-agent extension of autoepistemic logic (AEL) called distributed autoepistemic logic (dAEL). We define the semantics of dAEL using approximation fixpoint theory, an abstract algebraic framework that…

Public observation logic (POL) reasons about agent expectations and agent observations in various real world situations. The expectations of agents take shape based on certain protocols about the world around and they remove those possible…

Chase algorithms are indispensable in the domain of knowledge base querying, which enable the extraction of implicit knowledge from a given database via applications of rules from a given ontology. Such algorithms have proved beneficial in…

There are many techniques and tools to prove termination of C programs, but up to now these tools were not very powerful for fully automated termination proofs of programs whose termination depends on recursive data structures like lists.…

Dependency pairs are one of the most powerful techniques to analyze termination of term rewrite systems (TRSs) automatically. We adapt the dependency pair framework to the probabilistic setting in order to prove almost-sure innermost…

We describe the categorical semantics for a simply typed variant and a simplified dependently typed variant of Cocon, a contextual modal type theory where the box modality mediates between the weak function space that is used to represent…

The higher order matching problem is the problem of determining whether a term is an instance of another in the simply typed $\lambda$-calculus, i.e. to solve the equation a = b where a and b are simply typed $\lambda$-terms and b is…

In this short note, we are concerned with the fairness condition "A and B hold almost equally often", which is important for specifying and verifying the correctness of non-terminating processes and protocols. We introduce the logic of…

Notions of iteration range from the arguably most general Elgot iteration to a very specific Kleene iteration. The fundamental nature of Elgot iteration has been extensively explored by Bloom and Esik in the form of iteration theories,…

Scalar actions are ubiquitous in mathematics, and therefore it is valuable to be able to write them succinctly when formalizing. In this paper we explore how Lean 3's typeclasses are used by mathlib for scalar actions with examples,…

A representation theorem relates different mathematical structures by providing an isomorphism between them: that is, a one-to-one correspondence preserving their original properties. Establishing that the two structures substantially…

Resolution modulo is a first-order theorem proving method that can be applied both to first-order presentations of simple type theory (also called higher-order logic) and to set theory. When it is applied to some first-order presentations…

Combining a standard proof search method, such as resolution or tableaux, and rewriting is a powerful way to cut off search space in automated theorem proving, but proving the completeness of such combined methods may be challenging. It may…

In the last decades, several objects such as grammars, economical agents, laws of physics... have been defined as algorithms. In particular, after Brouwer, Heyting, and Kolomogorov, mathematical proofs have been defined as algorithms. In…

Many tasks in statistical and causal inference can be construed as problems of \emph{entailment} in a suitable formal language. We ask whether those problems are more difficult, from a computational perspective, for \emph{causal}…

The Stratified Foundations are a restriction of naive set theory where the comprehension scheme is restricted to stratifiable propositions. It is known that this theory is consistent and that proofs strongly normalize in this theory.…

Alternating-time temporal logic (ATL) and its extensions, including the alternating-time $\mu$-calculus (AMC), serve the specification of the strategic abilities of coalitions of agents in concurrent game structures. The key ingredient of…