计算机科学中的逻辑

While teaching untyped $\lambda$-calculus to undergraduate students, we were wondering why $\alpha$-equivalence is not directly inductively defined. In this paper, we demonstrate that this is indeed feasible. Specifically, we provide a…

Simplicial type theory extends homotopy type theory with a directed path type which internalizes the notion of a homomorphism within a type. This concept has significant applications both within mathematics -- where it allows for synthetic…

Temporal logic provided an appealing approach to specifying properties of operating systems and other "reactive" software by allowing propositions to be qualified by "when" they must be true. This paper shows how to get the same effect,…

In this paper, I discuss two logics for weighted finite structures: first-order logic with summation (FO(SUM)) and its recursive extension IFP(SUM). These logics originate from foundational work by Gr\"adel, Gurevich, and Meer in the 1990s.…

There is an imperative need to provide quality of life to a growing population of older adults living independently. Personalised solutions that focus on the person and take into consideration their preferences and context are key. In this…

The unification type of an equational theory is defined using a preorder on substitutions, called the instantiation preorder, whose scope is either restricted to the variables occurring in the unification problem, or unrestricted such that…

We consider linear single-path loops of the form \[ \textbf{while} \quad \varphi \quad \textbf{do} \quad \vec{x} \gets A \vec{x} + \vec{b} \quad \textbf{end} \] where $\vec{x}$ is a vector of variables, the loop guard $\varphi$ is a…

In this paper we study intermediate logics between the degree preserving companion of Godel fuzzy logic with an involution and classical propositional logic CPL, as well as the intermediate logics of their finite-valued counterparts.…

In this short paper, we advocate for the idea that continuation-based intermediate languages correspond to intermediate logics. The goal of intermediate languages is to serve as a basis for compiler intermediate representations, allowing to…

Iterative abstraction refinement techniques are one of the most prominent paradigms for the analysis and verification of systems with large or infinite state spaces. This paper investigates the changes of truth values of system properties…

In answer set programming, two groups of rules are considered strongly equivalent if they have the same meaning in any context. Strong equivalence of two programs can be sometimes established by deriving rules of each program from rules of…

Subgraph Isomorphism uses a small graph as a pattern to identify within a larger graph a set of vertices that have matching edges. This paper addresses a logic program written in Prolog for a specific relatively complex graph pattern for…

In the context of urban traffic control, traffic signal optimisation is the problem of determining the optimal green length for each signal in a set of traffic signals. The literature has effectively tackled such a problem, mostly with…

Probabilistic Logic Programming (PLP) under the Distribution Semantics is a leading approach to practical reasoning under uncertainty. An advantage of the Distribution Semantics is its suitability for implementation as a Prolog or Python…

Novel utility computing paradigms rely upon the deployment of multi-service applications to pervasive and highly distributed cloud-edge infrastructure resources. Deciding onto which computational nodes to place services in cloud-edge…

Anthem 2.0 is a tool to aid in the verification of logic programs written in an expressive fragment of Clingo's input language named mini-gringo, which includes arithmetic operations and simple choice rules but not aggregates. It can…

In this paper, we consider an approach introduced in term rewriting for the automatic detection of non-looping non-termination from patterns of rules. We adapt it to logic programming by defining a new unfolding technique that produces…

We present ASP Chef Mustache, an extension of ASP Chef that enhances template-based rendering of ASP solutions using a logic-less templating system inspired by Mustache. Our approach integrates data visualization frameworks such as…

We study two subclasses of the class of automatic structures: automatic structures of polynomial growth and Presburger structures. We present algebraic characterisations of the groups and the equivalence structures in these two classes.

The growing size of graph-based modeling artifacts in model-driven engineering calls for techniques that enable efficient execution of graph queries. Incremental approaches based on the RETE algorithm provide an adequate solution in many…