计算机科学中的逻辑

The Weighted Path Order of Yamada is a powerful technique for proving termination. It is also supported by CeTA, a certifier for checking untrusted termination proofs. To be more precise, CeTA contains a verified function that computes for…

In this paper we consider systems which consist of binary components with known reliabilities. We discuss their algebraic properties and define the corresponding algebraic structure, which we call the reliability algebra. We prove that the…

We establish a formal correspondence between resource calculi an appropriate linear multicategories. We consider the cases of (symmetric) representable, symmetric closed and autonomous multicategories. For all these structures, we prove…

Smart contracts are small but highly error-prone programs that implement agreements between multiple parties. We present a reactive synthesis approach for the automatic construction of smart contract state machines. Towards this end, we…

We provide a critical assessment of the current set of benchmarks for relative SRS termination in the Termination Problems Database (TPDB): most of the benchmarks in Waldmann_19 and ICFP_10_relative are, in fact, strictly terminating (i.…

As for term rewrite systems, the dependency pair (DP, for short) framework with several kinds of DP processors is useful for proving termination of logically constrained term rewrite systems (LCTRSs, for short). However, the polynomial…

We show that weighted path orders are special instances of a variant of semantic path orders. Exploiting this fact, we introduce a generalization of weighted path orders that goes beyond the realm of simple termination. Experimental data…

Logically constrained term rewriting systems (LCTRSs) are a program analyzing formalism with native support for data types which are not (co)inductively defined. As a first-order formalism, LCTRSs have accommodated only analysis of…

In this short paper, we consider a form of higher-order rewriting with a call-by-value evaluation strategy so as to model call-by-value programs. We briefly present a cost-size semantics to call-by-value rewriting: a class of algebraic…

Gentzen designed his natural deduction proof system to ``come as close as possible to actual reasoning.'' Indeed, natural deduction proofs closely resemble the static structure of logical reasoning in mathematical arguments. However,…

Modal logics are widely used in multi-agent systems to reason about actions, abilities, norms, or epistemic states. Combined with description logic languages, they are also a powerful tool to formalise modal aspects of ontology-based…

Teaching college students how to write rigorous proofs is a critical objective in courses that introduce formal reasoning. Over the course of several years, we have developed a mechanically-checkable style of calculational reasoning that we…

Proof formats for SAT solvers have diversified over the last decade, enabling new features such as extended resolution-like capabilities, very general extension-free rules, inclusion of proof hints, and pseudo-boolean reasoning.…

Safety and liveness are elementary concepts of computation, and the foundation of many verification paradigms. The safety-liveness classification of boolean properties characterizes whether a given property can be falsified by observing a…

We investigate mathematical structures that provide natural semantics for families of (quantified) non-classical logics featuring special unary connectives, known as recovery operators, that allow us to 'recover' the properties of classical…

We study the system IFP of intuitionistic fixed point logic, an extension of intuitionistic first-order logic by strictly positive inductive and coinductive definitions. We define a realizability interpretation of IFP and use it to extract…

We present a new syntactic criterion for the automatic detection of non-termination in an abstract setting that encompasses a simplified form of term rewriting and logic programming.

In a previous work we introduced a non-associative non-commutative logic extended by multimodalities, called subexponentials, licensing local application of structural rules. Here, we further explore this system, considering a classical…

Abstract algebra provides a large hierarchy of properties that a collection of objects can satisfy, such as forming an abelian group or a semiring. These classifications can arranged into a broad and typically acyclic directed graph. This…

There are many techniques and tools for termination of C programs, but up to now they were not very powerful for termination proofs of programs whose termination depends on recursive data structures like lists. We present the first approach…