计算机科学中的逻辑

A possible path to the interpretability of neural networks is to (approximately) represent them in the regional format of piecewise linear functions, where regions of inputs are associated to linear functions computing the network outputs.…

Recently, description logic LE-ALC was introduced for reasoning in the semantic environment of enriched formal contexts, and a polynomial-time tableaux algorithm was developed to check the consistency of knowledge bases with acyclic TBoxes.…

Trace-based properties are the gold standard for program behaviour analysis. One of the domains of application of this type of analysis is cryptocurrency ledgers, both for the purpose of analyzing the behaviour of the ledger itself, and any…

Abstract interpretation offers a powerful toolset for static analysis, tackling precision, complexity and state-explosion issues. In the literature, state partitioning abstractions based on (bi)simulation and property-preserving state…

Dependency pairs are one of the most powerful techniques to analyze termination of term rewrite systems automatically. We adapt dependency pairs to the probabilistic setting and develop an annotated dependency pair framework for…

Recently, the description logic LE-ALC was introduced for reasoning in the semantic environment of the enriched formal contexts, and a tableaux algorithm was developed for checking the consistency of ABoxes in this logic. In this paper, we…

Pseudo-Boolean model counting involves computing the number of satisfying assignments of a given pseudo-Boolean (PB) formula. In recent years, PB model counting has seen increased interest partly owing to the succinctness of PB formulas…

This volume contains the post-proceedings of the 19th LSFA, which was held in Goi\^ania, the capital of Goi\'as state in Brazil, from September 18 to September 20, 2024. Logical and semantic frameworks are formal languages used to represent…

A common practice of ML systems development concerns the training of the same model under different data sets, and the use of the same (training and test) sets for different learning models. The first case is a desirable practice for…

We introduce an imperative, stack-based, and reversible computational model that characterizes Two-way Bijections both implicitly, concerning their computational complexity, and with zero-garbage.

We present POPACheck, the first model checking tool for probabilistic Pushdown Automata (pPDA) supporting temporal logic specifications. POPACheck provides a user-friendly probabilistic modeling language with recursion that automatically…

The task of inferring logical formulas from examples has garnered significant attention as a means to assist engineers in creating formal specifications used in the design, synthesis, and verification of computing systems. Among various…

We define a notion of general uniform interpolant, generalizing the notions of cover and of uniform interpolant and identify situations in which symbol elimination can be used for computing general uniform interpolants. We investigate the…

The satisfiability problem for First-order Modal Logic (\FOML) is undecidable even for simple fragments like having only unary predicates, two variables etc. Recently a new way to identify decidable fragments of \FOML has been introduced…

The semantics of alternating-time temporal logic (ATL) and the more expressive alternating-time {\mu}-calculus (AMC) is standardly given in terms of concurrent game frames (CGF). The information required to interpret AMC formulas is…

The Boolean satisfiability (SAT) problem lies at the core of many applications in combinatorial optimization, software verification, cryptography, and machine learning. While state-of-the-art solvers have demonstrated high efficiency in…

Second-order quantifier-elimination is the problem of finding, given a formula with second-order quantifiers, a logically equivalent first-order formula. While such formulas are not computable in general, there are practical algorithms and…

Deep and shallow embeddings of non-classical logics in classical higher-order logic have been explored, implemented, and used in various reasoning tools in recent years. This paper presents a method for the simultaneous deployment of deep…

We investigate the equational theory for Kleene algebra terms with variable complements and constant complements -- (language) complement where it applies only to variables or constants -- w.r.t. languages. While the equational theory…

We introduce the $k$-variable-occurrence fragment, which is the set of terms having at most $k$ occurrences of variables. We give a sufficient condition for the decidability of the equational theory of the $k$-variable-occurrence fragment…