计算机科学中的逻辑

Hyperproperties relate multiple executions of a system and are commonly used to specify security and information-flow policies. While many verification approaches for hyperproperties exist, providing a convincing certificate that the system…

Number fields and their rings of integers, which generalize the rational numbers and the integers, are foundational objects in number theory. There are several computer algebra systems and databases concerned with the computational aspects…

Within the model-theoretic framework for supervised learning introduced by Grohe and Tur\'an (TOCS 2004), we study the parameterized complexity of learning concepts definable in monadic second-order logic (MSO). We show that the problem of…

he cvc5 solver is today one of the strongest systems for solving first order problems with theories but also without them. In this work we equip its enumeration-based instantiation with a neural network that guides the choice of the…

Propositional Dynamic Logic, PDL, is a modal logic designed to formalize the reasoning about programs. By extending accessibility between states to states and state sets, concurrent propositional dynamic logic CPDL, is introduced to include…

We investigate automated model-checking of the Ethereum specification, focusing on the Accountable Safety property of the 3SF consensus protocol. We select 3SF due to its relevance and the unique challenges it poses for formal verification.…

In this paper, we establish the foundations of a novel logical framework for the {\pi}-calculus, based on the deduction-as-computation paradigm. Following the standard proof-theoretic interpretation of logic programming, we represent…

We combine linear temporal logic (with both past and future modalities) with a deontic version of justification logic to provide a framework for reasoning about time and epistemic and normative reasons. In addition to temporal modalities,…

In this paper we present various temporal justification logics involving both past and future time modalities. We combine Artemov's logic of proofs with linear temporal logic (with both past and future operators), and establish its…

In this paper we continue the study of edge-colored graphs associated with finite idempotent algebras initiated in arXiv:2006.09599. We prove stronger connectivity properties of such graphs that will allows us to demonstrate several useful…

We refine and advance the study of the local structure of idempotent finite algebras started in [A.Bulatov, The Graph of a Relational Structure and Constraint Satisfaction Problems, LICS, 2004]. We introduce a graph-like structure on an…

This paper proposes SAT-based techniques to calculate a specific normal form of a given finite mathematical structure (model). The normal form is obtained by permuting the domain elements so that the representation of the structure is…

Complete enumeration of finite models of first-order logic (FOL) formulas is pivotal to universal algebra, which studies and catalogs algebraic structures. Efficient finite model enumeration is highly challenging because the number of…

System requirements related to concepts like information flow, knowledge, and robustness cannot be judged in terms of individual system executions, but rather require an analysis of the relationship between multiple executions. Such…

One can perform equational reasoning about computational effects with a purely functional programming language thanks to monads. Even though equational reasoning for effectful programs is desirable, it is not yet mainstream. This is partly…

Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. The two most important such logics are HyperLTL and HyperCTL*, which generalise LTL and CTL* by…

Measurable cones, with linear and measurable functions as morphisms, are a model of intuitionistic linear logic and of call-by-name probabilistic PCF which accommodates "continuous data types" such as the real line. So far however, they…

We prove that the class of 3D-grids is cannot be transduced from planar graphs, and more generally, from any class of graphs of bounded Euler genus. To prove our result, we introduce a new structural tool called slice decompositions, and…

Chronological backtracking is an interesting SAT solving technique within CDCL reasoning, as it backtracks less aggressively upon conflicts. However, chronological backtracking is more difficult to maintain due to its weaker SAT solving…

Abstraction is an important and useful concept in the field of artificial intelligence. To the best of our knowledge, there is no syntactic method to compute a sound and complete abstraction from a given low-level basic action theory and a…