计算机科学中的逻辑

Approximate model counting is the task of approximating the number of solutions to an input Boolean formula. The state-of-the-art approximate model counter for formulas in conjunctive normal form (CNF), ApproxMC, provides a scalable means…

Neural-symbolic integration aims to combine the connectionist subsymbolic with the logical symbolic approach to artificial intelligence. In this paper, we first define the answer set semantics of (boolean) neural nets and then introduce…

We present a polymorphic linear lambda-calculus as a proof language for second-order intuitionistic linear logic. The calculus includes addition and scalar multiplication, enabling the proof of a linearity result at the syntactic level.

Generalization techniques have many applications, including template construction, argument generalization, and indexing. Modern interactive provers can exploit advancement in generalization methods over expressive type theories to further…

Linear-time temporal logic on finite traces (LTLf) is rapidly becoming a de-facto standard to produce specifications in many application domains (e.g., planning, business process management, run-time monitoring, reactive synthesis). Several…

Distributed First Order Logic (DFOL) has been introduced more than ten years ago with the purpose of formalising distributed knowledge-based systems, where knowledge about heterogeneous domains is scattered into a set of interconnected…

The Resource Description Framework (RDF) is a fundamental technology in the Semantic Web, enabling the representation and interchange of structured data. However, RDF lacks the capability to express negated statements in a generic way. As a…

As well known, weak K4 and the difference logic DL do not enjoy the Craig interpolation property. Our concern here is the problem of deciding whether any given implication does have an interpolant in these logics. We show that the…

This paper focuses on succinctness results for fragments of Linear Temporal Logic with Past (LTL) devoid of binary temporal operators like until, and provides methods to establish them. We prove that there is a family of cosafety languages…

We give an adequate, concrete, categorical-based model for Lambda-S, which is a typed version of a linear-algebraic lambda calculus, extended with measurements. Lambda-S is an extension to first-order lambda calculus unifying two approaches…

To appear in Theory and Practice of Logic Programming (TPLP). Dynamic systems play a central role in fields such as planning, verification, and databases. Fragmented throughout these fields, we find a multitude of languages to formally…

Kripke models are an effective and widely used tool for representing epistemic attitudes of agents in multi-agent systems, including distributed systems. Dynamic Epistemic Logic (DEL) adds communication in the form of model transforming…

Many automated planning methods and formulations rely on suitably designed abstractions or simplifications of the constrained dynamics associated with agents to attain computational scalability. We consider formulations of temporal planning…

Recently, we showed how to use control-flow refinement (CFR) to improve automatic complexity analysis of integer programs. While up to now CFR was limited to classical programs, in this paper we extend CFR to probabilistic programs and show…

We introduce a procedure for proving safety properties. This procedure is based on a technique called Partial Quantifier Elimination (PQE). In contrast to complete quantifier elimination, in PQE, only a part of the formula is taken out of…

Previous works by Gor\'e, Postniece and Tiu have provided sound and cut-free complete proof systems for modal logics extended with path axioms using the formalism of nested sequent. Our aim is to provide (i) a constructive cut-elimination…

The basic system E of dyadic deontic logic proposed by {\AA}qvist offers a simple solution to contrary-to-duty paradoxes and allows to represent norms with exceptions. We investigate E from a proof-theoretical viewpoint. We propose a…

In 1995, McKay and Radziszowski proved that the Ramsey number R(4,5) is equal to 25. Their proof relies on a combination of high-level arguments and computational steps. The authors have performed the computational parts of the proof with…

Context: Linear temporal logic (LTL) model checking faces a significant challenge known as the state-explosion problem. The on-the-fly method is a solution that constructs and checks the state space simultaneously, avoiding generating all…

This thesis revolves around an area of computer science called "semantics". We work with operational semantics, equational theories, and denotational semantics. The first contribution of this thesis is a study of the commutativity of…