计算机科学中的逻辑

Some Magic Tricks (MT), such as many kinds of Card Magic (CM), consisting of human computational or logical actions. How to ensure the logical correctness of these MTs? In this paper, the Model Checking (MC) technique is employed to study a…

In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected logical…

We present a KE-tableau-based implementation of a reasoner for a decidable fragment of (stratified) set theory expressing the description logic $\mathcal{DL}\langle \mathsf{4LQS^{R,\!\times}}\rangle(\mathbf{D})$…

We present a KE-tableau-based procedure for the main TBox and ABox reasoning tasks for the description logic $\mathcal{DL}\langle \mathsf{4LQS^{R,\!\times}}\rangle(\mathbf{D})$, in short $\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$. The logic…

Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant {\eta}-equalities and consequently do not admit dependent eliminators. To…

We present an ongoing implementation of a KE-tableau based reasoner for a decidable fragment of stratified elementary set theory expressing the description logic $\mathcal{DL}\langle \mathsf{4LQS^{R,\!\times}}\rangle(\mathbf{D})$ (shortly…

In this paper we consider the most common ABox reasoning services for the description logic $\mathcal{DL}\langle \mathsf{4LQS^{R,\!\times}}\rangle(\mathbf{D})$ ($\mathcal{DL}_{\mathbf{D}}^{4,\!\times}$, for short) and prove their…

A pushdown vector addition system with states (PVASS) extends the model of vector addition systems with a pushdown stack. The algorithmic analysis of PVASS has applications such as static analysis of recursive programs manipulating integer…

We present the proof assistant homotopy.io for working with finitely-presented semistrict higher categories. The tool runs in the browser with a point-and-click interface, allowing direct manipulation of proof objects via a graphical…

We study the accurate and efficient computation of the expected number of times each state is visited in discrete- and continuous-time Markov chains. To obtain sound accuracy guarantees efficiently, we lift interval iteration and…

Libraries of formalized mathematics use a possibly broad range of different representations for a same mathematical concept. Yet light to major manual input from users remains most often required for obtaining the corresponding variants of…

Formal verification of smart contracts has become a hot topic in academic and industrial research, given the growing value of assets managed by decentralized applications and the consequent incentive for adversaries to tamper with them.…

We propose a new encoding of the first-order connection method as a Boolean satisfiability problem. The encoding eschews tree-like presentations of the connection method in favour of matrices, as we show that tree-like calculi have a number…

Invariants are key to formal loop verification as they capture loop properties that are valid before and after each loop iteration. Yet, generating invariants is a notorious task already for syntactically restricted classes of loops. Rather…

The need to solve non-linear arithmetic constraints presents a major obstacle to the automatic verification of smart contracts. In this case study we focus on the two overapproximation techniques used by the industry verification tool…

We investigate the `local consistency implies global consistency' principle of strict width among structures within the scope of the Bodirsky-Pinsker dichotomy conjecture for infinite-domain Constraint Satisfaction Problems (CSPs). Our main…

Indexed Linear Logic has been introduced by Ehrhard and Bucciarelli, it can be seen as a logical presentation of non-idempotent intersection types extended through the relational semantics to the full linear logic. We introduce an…

A cyclic proof system is a proof system whose proof figure is a tree with cycles. The cut-elimination in a proof system is fundamental. It is conjectured that the cut-elimination in the cyclic proof system for first-order logic with…

The constraint satisfaction problem, parameterized by a relational structure, provides a general framework for expressing computational decision problems. Already the restriction to the class of all finite structures forms an interesting…

The $\lambda$$\Pi$-calculus modulo theory is an extension of simply typed $\lambda$-calculus with dependent types and user-defined rewrite rules. We show that it is possible to replace the rewrite rules of a theory of the…