计算机科学中的逻辑

The uniform one-dimensional fragment of first-order logic was introduced a few years ago as a generalization of the two-variable fragment of first-order logic to contexts involving relations of arity greater than two. Quantifiers in this…

Trace properties, which are sets of execution traces, are often used to analyze systems, but their expressiveness is limited. Clarkson and Schneider defined hyperproperties as a generalization of trace properties to sets of sets of traces.…

In this paper, we delve into the study of epistemic logics, interpreted through similarity models based on weighted graphs. We explore eight languages that extend the traditional epistemic language by incorporating modalities of common,…

Abstract machines for strong evaluation of the $\lambda$-calculus enter into arguments and have a set of transitions for backtracking out of an evaluated argument. We study a new abstract machine which avoids backtracking by splitting the…

Neural abstractions have been recently introduced as formal approximations of complex, nonlinear dynamical models. They comprise a neural ODE and a certified upper bound on the error between the abstract neural network and the concrete…

We investigate the complexity of the satisfiability problem for a modal logic expressing `knowing how' assertions, related to an agent's abilities to achieve a certain goal. We take one of the most standard semantics for this kind of logics…

Originally introduced in the context of the algebraic approach to term graph rewriting, the notion of gs-monoidal category has surfaced a few times under different monikers in the last decades. They can be thought of as symmetric monoidal…

We study functional and concurrent calculi with non-determinism, along with type systems to control resources based on linearity. The interplay between non-determinism and linearity is delicate: careless handling of branches can discard…

In this note we compare two kinds of systems that verify the correctness of mathematical developments: roof checking and proof construction by tactics and we propose to merge them in a single system.

We develop domain theory in constructive and predicative univalent foundations (also known as homotopy type theory). That we work predicatively means that we do not assume Voevodsky's propositional resizing axioms. Our work is constructive…

It often happens that free algebras for a given theory satisfy useful reasoning principles that are not preserved under homomorphisms of algebras, and hence need not hold in an arbitrary algebra. For instance, if $M$ is the free monoid on a…

We show how variations of range-restriction and also the Horn property can be passed from inputs to outputs of Craig interpolation in first-order logic. The proof system is clausal tableaux, which stems from first-order ATP. Our results are…

IC3 is a famous bit-level framework for safety verification. By incorporating datapath abstraction, a notable enhancement in the efficiency of hardware verification can be achieved. However, datapath abstraction entails a coarse level of…

A question we can ask of multi-agent systems is whether the agents' collective interaction satisfies particular goals or specifications, which can be either individual or collective. When a collaborative goal is not reached, or a…

We introduce the probabilistic two-agent justification logic IPJ, a logic in which we can reason about agents that perform interactive proofs. In order to study the growth rate of the probabilities in IPJ, we present a new method of…

In this work-in-progress paper we explore using the recently introduced VLSM formalism to define and reason about the dynamics of agent-based systems. To this aim we use VLSMs to formally present several possible approaches to modeling the…

The substitution lemma is a renowned theorem within the realm of lambda-calculus theory and concerns the interactional behaviour of the metasubstitution operation. In this work, we augment the lambda-calculus's grammar with an uninterpreted…

Epistemic protocols represents a current field of interest, with numerous approaches still being studied. In this paper we formalize parallel sessions of the The Muddy Children Puzzle using Public Observation Logic, a system that allows…

In this paper, we investigate how the initial models and the final models for the polynomial functors can be uniformly specified in matching logic.

Linear logic is a substructural logic proposed as a refinement of classical and intuitionistic logics, with applications in programming languages, game semantics, and quantum physics. We present a template for Gentzen-style linear logic…