计算机科学中的逻辑

Chemical theory can be made more rigorous using the Lean theorem prover, an interactive theorem prover for complex mathematics. We formalize the Langmuir and BET theories of adsorption, making each scientific premise clear and every step of…

This research note provides algebraic characterizations of the least model, subsumption, and uniform equivalence of propositional Krom logic programs.

Logical frameworks are successful in modeling proof systems. Recently, CoLF extended the logical framework LF to support higher-order rational terms that enable adequate encoding of circular objects and derivations. In this paper, we…

This paper is a continuation of our work concerning the logical and computational foundations of multi-step fuzzy inference. We bring further results on the implementation of the Mamdani-Assilian type of fuzzy rules and inference in Goedel…

Bayesian networks (BNs) are graphical \emph{first-order} probabilistic models that allow for a compact representation of large probability distributions, and for efficient inference, both exact and approximate. We introduce a…

We report on an original formalization of measure and integration theory in the Coq proof assistant. We build the Lebesgue measure following a standard construction that had not yet been formalized in proof assistants based on dependent…

We propose a doxastic \L ukasiewicz logic \textbf{B\L} that is sound and complete with respect to the class of Kripke-based models in which atomic propositions and accessibility relations are both infinitely valued in the standard…

The algebraic properties of the combination of probabilistic choice and nondeterministic choice have long been a research topic in program semantics. This paper explains a formalization in the Coq proof assistant of a monad equipped with…

We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras…

Recently, Gavazzo has developed a relational theory of symbolic manipulation, that allows to study syntax-based rewriting systems without relying on specific notions of syntax. This theory was obtained by extending the algebra of relations…

Intersection types are a standard tool in operational and semantical studies of the lambda calculus. De Carvalho showed how multi types, a quantitative variant of intersection types providing a handy presentation of the relational…

We characterize the strength, in terms of Weihrauch degrees, of certain problems related to Ramsey-like theorems concerning colourings of the rationals and of the natural numbers. The theorems we are chiefly interested in assert the…

In recent years, circuit simulators and Boolean satisfiability (SAT) solvers have been tightly integrated to provide efficient logic synthesis and verification. Circuit simulation can generate highly expressive simulation patterns that can…

This paper addresses the logical and computational foundations of multi-step fuzzy inference using the Mamdani-Assilian type of fuzzy rules by implementing such inference in Goedel logic with truth constants. We apply the results achieved…

A graph class $\mathscr{C}$ is called monadically stable if one cannot interpret, in first-order logic, arbitrary large linear orders in colored graphs from $\mathscr{C}$. We prove that the model checking problem for first-order logic is…

In this paper, we study the composition of services so as to obtain runs satisfying a task specification in Linear Temporal Logic on finite traces (LTLf). We study the problem in the case services are nondeterministic and the LTLf…

Robotic systems used in safety-critical industrial situations often rely on modular software architectures, and increasingly include autonomous components. Verifying that these modular robotic systems behave as expected requires approaches…

We automatically verify the crucial steps in the original proof of correctness of an algorithm which, given a geometric graph satisfying certain additional properties removes edges in a systematic way for producing a connected graph in…

We study a new extension of the weak MSO logic, talking about boundedness. Instead of a previously considered quantifier U, expressing the fact that there exist arbitrarily large finite sets satisfying a given property, we consider a…

This paper discusses the formalization of proofs "by diagram chasing", a standard technique for proving properties in abelian categories. We discuss how the essence of diagram chases can be captured by a simple many-sorted first-order…