计算机科学中的逻辑

In this paper, we address the problem of the (reactive) realizability of specifications of theories richer than Booleans, including arithmetic theories. Our approach transforms theory specifications into purely Boolean specifications by (1)…

Logical frameworks can be used to translate proofs from a proof system to another one. For this purpose, we should be able to encode the theory of the proof system in the logical framework. The Lambda Pi calculus modulo theory is one of…

We present MsATL: the first tool for deciding the satisfiability of Alternating-time Temporal Logic (ATL) with imperfect information. MsATL combines SAT Modulo Monotonic Theories solvers with existing ATL model checkers: MCMAS and STV. The…

We introduce a novel logic for asynchronous hyperproperties with a new mechanism to identify relevant positions on traces. While the new logic is more expressive than a related logic presented recently by Bozzelli et al., we obtain the same…

Formal verification of strategic abilities is a hard problem. We propose to use the methodology of assume-guarantee reasoning in order to facilitate model checking of alternating-time temporal logic with imperfect information and imperfect…

It has been argued that reduction procedures are closely connected to the question about identity of proofs and that accepting certain reductions would lead to a trivialization of identity of proofs in the sense that every derivation of the…

The propositional product logic is one of the basic fuzzy logics with continuous t-norms, exploiting the multiplication t-norm on the unit interval [0,1]. Our aim is to combine well-established automated deduction (theorem proving) with…

We address the problem of handling provenance information in ELHr ontologies. We consider a setting recently introduced for ontology-based data access, based on semirings and extending classical data provenance, in which ontology axioms are…

We introduce the class of P-finite automata. These are a generalisation of weighted automata, in which the weights of transitions can depend polynomially on the length of the input word. P-finite automata can also be viewed as simple…

An automated resource analysis technique is introduced, targeting a Call-By-Push-Value abstract machine, with memory prediction as a practical goal. The machine has a polymorphic and linear type system enhanced with a first-order logical…

Non-fungible tokens, NFT, have been used to record ownership of real estate, art, digital assets, and more recently to serve legal notice. They provide an important and accessible non-financial use of cryptocurrency's blockchain but are…

We consider the problem of automatically inferring specifications in the branching-time logic, Computation Tree Logic (CTL), from a given system. Designing functional and usable specifications has always been one of the biggest challenges…

In a seminal work~\cite{Fine:2018}, Fine classifies several forms of ignorance, among which are Fitchean ignorance, first-order ignorance, Rumsfeld ignorance, and second-order ignorance. It is shown that there is interesting relationship…

The ellipsoid method is an algorithm that solves the (weak) feasibility and linear optimization problems for convex sets by making oracle calls to their (weak) separation problem. We observe that the previously known method for showing that…

We propose urgency programs, a new programming model with support for alternation, imperfect information, and recursion. The novelty are urgency annotations that decorate the (angelic and demonic) choice operators and control the order in…

In this paper, we explore conjunctive query rewriting, focusing on queries containing universally quantified negation within the framework of disjunctive existential rules. We address the undecidability of the existence of a finite and…

The lambda-Pi-calculus allows to express proofs of minimal predicate logic. It can be extended, in a very simple way, by adding computation rules. This leads to the lambda-Pi-calculus modulo. We show in this paper that this simple extension…

Algebraic data types (ADTs) are a construct classically found in functional programming languages that capture data structures like enumerated types, lists, and trees. In recent years, interest in ADTs has increased. For example, popular…

The need to model and analyse dynamic systems operating over complex data is ubiquitous in AI and neighboring areas, in particular business process management. Analysing such data-aware systems is a notoriously difficult problem, as they…

This paper presents meta-logical investigations based on category theory using the proof assistant Isabelle/HOL. We demonstrate the potential of a free logic based shallow semantic embedding of category theory by providing a formalization…