计算机科学中的逻辑

In this paper, we present the first fully-automated expected amortised cost analysis of self-adjusting data structures, that is, of randomised splay trees, randomised splay heaps and randomised meldable heaps, which so far have only (semi-)…

We introduce geometric consideration into the theory of formal languages. We aim to shed light on our understanding of global patterns that occur on infinite strings. We utilise methods of geometric group theory. Our emphasis is on large…

Reversible computing is motivated by both pragmatic and foundational considerations arising from a variety of disciplines. We take a particular path through the development of reversible computation, emphasizing compositional reversible…

Bigraphs are a versatile modelling formalism that allows easy expression of placement and connectivity relations in a graphical format. System evolution is user defined as a set of rewrite rules. This paper presents a practical, yet…

First-order linear temporal logic (FOLTL) is a flexible and expressive formalism capable of naturally describing complex behaviors and properties. Although the logic is in general highly undecidable, the idea of using it as a specification…

In the field of human intelligence, officers use an alphanumeric scale, known as the Admiralty System, to rate the credibility of messages and the reliability of their sources (NATO AJP-2.1, 2016). During this evaluation, they are expected…

The class of defeasible logics is only vaguely defined -- it is defined by a few exemplars and the general idea of efficient reasoning with defeasible rules. The recent definition of the defeasible logic $DL(\partial_{||})$ introduced new…

Concrete domains have been introduced in the context of Description Logics to allow references to qualitative and quantitative values. In particular, the class of $\omega$-admissible concrete domains, which includes Allen's interval…

We develop realizability models of intensional type theory, based on groupoids, wherein realizers themselves carry non-trivial (non-discrete) homotopical structure. In the spirit of realizability, this is intended to formalize a homotopical…

In homotopy type theory, a natural number type is freely generated by an element and an endomorphism. Similarly, an integer type is freely generated by an element and an automorphism. Using only dependent sums, identity types, extensional…

An "element-free" probability distribution is what remains of a probability distribution after we forget the elements to which the probabilities were assigned. These objects naturally arise in Bayesian statistics, in situations where…

SAT solvers are indispensable in formal verification for hardware and software with many important applications. CDCL is the most widely used framework for modern SAT solvers, and restart is an essential technique of CDCL. When restarting,…

We present for the first time a supermartingale certificate for $\omega$-regular specifications. We leverage the Robbins & Siegmund convergence theorem to characterize supermartingale certificates for the almost-sure acceptance of Streett…

This paper considers program synthesis in the context of computational hardness, asking the question: How hard is it to determine whether a given synthesis problem has a solution or not? To answer this question, this paper studies program…

A new family of categorial grammars is proposed, defined by enriching basic categorial grammars with a conjunction operation. It is proved that the formalism obtained in this way has the same expressive power as conjunctive grammars, that…

A preliminary test of the software package RA is presented. The main focus of this test is to assess RA`s reasoning capabilities that are based on the formal system PECR. Particular attention is given to the finite computational resources…

We propose an enhancement to inductive types and records in a dependent type theory, namely (co)conditions. With a primitive interval type, conditions generalize the cubical syntax of higher inductive types in homotopy type theory, while…

We present a number of first- and second-order extensions to SMT theories specifically aimed at representing and analyzing SQL queries with join, projection, and selection operations. We support reasoning about SQL queries with either bag…

We analyse abstract data types that model numerical structures with a concept of error. Specifically, we focus on arithmetic data types that contain an error value $\bot$ whose main purpose is to always return a value for division. To rings…

Temporal reasoning with conditionals is more complex than both classical temporal reasoning and reasoning with timeless conditionals, and can lead to some rather counter-intuitive conclusions. For instance, Aristotle's famous "Sea Battle…