计算机科学中的逻辑

The problem of checking satisfiability of linear real arithmetic (LRA) and non-linear real arithmetic (NRA) formulas has broad applications, in particular, they are at the heart of logic-related applications such as logic for artificial…

Solving algebra problems (APs) continues to attract significant research interest as evidenced by the large number of algorithms and theories proposed over the past decade. Despite these important research contributions, however, the body…

Automated reasoners, such as SAT/SMT solvers and first-order provers, are becoming the backbones of rigorous systems engineering, being used for example in applications of system verification, program synthesis, and cybersecurity.…

Large knowledge graphs capture information of a large number of entities and their relations. Among the many relations they capture, class subsumption assertions are usually present and expressed using the \texttt{rdfs:subClassOf}…

We present an open-source tool for manipulating Boolean circuits. It implements efficient algorithms, both existing and novel, for a rich variety of frequently used circuit tasks such as satisfiability, synthesis, and minimization. We…

This paper presents a translation from Gospel-annotated OCaml programs into Viper, an intermediate verification language featuring Separation Logic. The practical goal is to extend Cameleer with a new back-end to prove heap-dependent OCaml…

We introduce a novel language for reasoning about agents' cognitive attitudes of both epistemic and motivational type. We interpret it by means of a computationally grounded semantics using belief bases. Our language includes five types of…

Liveness properties are traditionally proven using a ranking function that maps system states to some well-founded set. Carrying out such proofs in first-order logic enables automation by SMT solvers. However, reasoning about many natural…

Quantitative requirements play an important role in the context of multi-agent systems, where there is often a trade-off between the tasks of individual agents and the constraints that the agents must jointly adhere to. We study multi-agent…

Interactive theorem provers are complex systems that require sophisticated platform efforts - and hence systems programming environments - to manage effectively. The Isabelle platform exemplifies this with its Isabelle/Scala systems…

Recently, Miller and Wu introduced the positive $\lambda$-calculus, a call-by-value $\lambda$-calculus with sharing obtained by assigning proof terms to the positively polarized focused proofs for minimal intuitionistic logic. The positive…

It is well known that Kleisli categories provide a natural language to model side effects. For instance, in the theory of coalgebras, behavioural equivalence coincides with language equivalence (instead of bisimilarity) when…

We consider the problem of designing typed concurrent calculi with non-deterministic choice in which types leverage linearity for controlling resources, thereby ensuring strong correctness properties for processes. This problem is…

We introduce a continuous domain for function spaces over topological spaces which are not core-compact. Notable examples of such topological spaces include the real line with the upper limit topology, which is used in solution of initial…

Nominal algebra includes $\alpha$-equality and freshness constraints on nominal terms endowed with a nominal set semantics that facilitates reasoning about languages with binders. Nominal unification is decidable and unitary, however, its…

We revisit the duality between Kripke and algebraic semantics of intuitionistic and intuitionistic modal logic. We find that there is a certain mismatch between the two semantics, which means that not all algebraic models can be embedded…

Multiplicative-Additive System Virtual (MAV) is a logic that extends Multiplicative-Additive Linear Logic with a self-dual non-commutative operator expressing the concept of "before" or "sequencing". MAV is also an extenson of the the logic…

Categories and categorical structures are increasingly recognized as useful abstractions for modeling in science and engineering. To uniformly implement category-theoretic mathematical models in software, we introduce GATlab, a…

We prove a characterization of first-order string-to-string transduction via $\lambda$-terms typed in non-commutative affine logic that compute with Church encoding, extending the analogous known characterization of star-free languages. We…

Parametricity is a key metatheoretic property of type systems, which implies strong uniformity & modularity properties of the structure of types within systems possessing it. In recent years, various systems of dependent type theory have…