计算机科学中的逻辑

Let ${\cal T}$ be a theory allowing a form of elimination of existential quantifiers (possibly for formulae in a certain class). We analyze possibilities of constructing (most general) solutions w.r.t.\ ${\cal T}$ for formulae of the form…

A formula of the modal mu-calculus enjoys finite convergence on a structure if there is some finite unfolding of the formula that defines the same set. A structure enjoys finite convergence if all formulas of the mu-calculus enjoy finite…

Intrinsically-typed presentations of type theory often use equality in the meta-language to represent object-language judgmental equality. In such equational syntax, proof-relevant logical relations define computability predicates on…

The LAP toolset is a set of command line tools for teaching logic in computer science. It provides implementations of standard algorithms for propositional and first order logic, including conversions to various normal forms, propositional…

High-Level Synthesis leverages loop unrolling and array partitioning, but scheduling concurrent accesses is challenging when indices contain non-affine arithmetic. Conventional polyhedral frameworks systematically over-approximate these…

We formalize in Lean 4 a complete combinatorial route from Scarf's theorem to Brouwer's fixed point theorem and to the existence of mixed Nash equilibria in finite games. The development follows Ivanov's indexed-order formulation of Scarf's…

Spot is a mature, open-source C++/Python library and toolset for Linear Temporal Logic (LTL) and $\omega$-automata manipulation. While Spot is routinely used as a research and verification back-end, its rich visualization capabilities and…

We study sets and functions definable in the three additive theories $\FO(\Z,+,\leq)$, $\FO(\R,+,\leq)$, and $\FO(\R,\Z,+,\leq)$. The Ginsburg--Spanier theorem~\cite{GS66} characterizes $\FO(\Z,+,\leq)$-definable sets as exactly the…

We solve a long standing open problem, showing that the query answering for conjunctive queries with safe negation, over DL-Lite$_{core}$ knowledge bases, is undecidable.

We investigate quantifier-free interpolation properties for several fragments generalising the extensional theory of arrays. Our results include the (general) quantifier-free interpolation properties of combinatory array logic with iterated…

Often, the easiest way to learn something is to have to use it for a purpose. This purpose can be playful: In 'Tempus fugit', the player takes on the role of a magician who has to defeat enemies by casting spells. The applicability of…

In their 2018 paper, Agotnes, van Ditmarsch, and Wang extended the notions of success and self-refutation in public announcements to true lies, impossible lies, and $\sigma$-validity in general, where $\sigma$ is a finite or infinite…

We present LogicProof, an interactive web-based theorem prover designed for educational use. The system supports natural deduction and sequent calculus for propositional and first-order logic in both classical and constructive variants. It…

Satisfiability modulo theory (SMT) solvers have significantly advanced automated reasoning due to their effectiveness in solving problems across various fields. With the advancement in SMT solvers, there is growing interest in exploring…

This paper does not address the mathematical truth of P versus NP. Instead, it identifies a structural limitation of uniform proof-generation methods in the standard Turing model. The observation is model-theoretic: it concerns the…

The first part of this paper provides an experience report, recounting the design and long-term maintenance of the Carnap proof assistant framework used cumulatively by over 45,000 students worldwide over the last decade. We cover the good,…

Time-dependent processes are often described by machines with an internal state which is updated as time evolves. An external observer cannot see this state and learns about a process only through finite observations of its inputs and…

The Model Constructing Satisfiability (MCSat) approach has shown strong performance in solving complex SMT problems, in particular in algebraic SMT theories such as non-linear integer and real arithmetic. In this paper we revisit the…

Predicate invention (PI), the creation of new predicates to extend the hypothesis space, remains a critical bottleneck in Inductive Logic Programming (ILP). Existing methods rely on domain expertise and produce semantically opaque…

We study the expressive power of the simplest modal-temporal language, obtained by adding Prior's temporal operators \(G\) and \(H\) to the basic modal language with \(\Box\). This language is the standard bimodal combination of modal and…