Related papers: A Machine Checked Model of Idempotent MGU Axioms F…
Automated theorem proving in first-order logic is an active research area which is successfully supported by machine learning. While there have been various proposals for encoding logical formulas into numerical vectors -- from simple…
This paper describes a formalization of discrete real closed fields in the Coq proof assistant. This abstract structure captures for instance the theory of real algebraic numbers, a decidable subset of real numbers with good algorithmic…
In various applications the search for certificates for certain properties (e.g., stability of dynamical systems, program termination) can be formulated as a quantified constraint solving problem with quantifier prefix exists-forall. In…
We investigate here a new version of the Calculus of Inductive Constructions (CIC) on which the proof assistant Coq is based: the Calculus of Congruent Inductive Constructions, which truly extends CIC by building in arbitrary first-order…
The interplay between Machine Learning (ML) and Constrained Optimization (CO) has recently been the subject of increasing interest, leading to a new and prolific research area covering (e.g.) Decision Focused Learning and Constrained…
This extended abstract is about an effort to build a formal description of a triangulation algorithm starting with a naive description of the algorithm where triangles, edges, and triangulations are simply given as sets and the most complex…
First order formulas in a relational signature can be considered as operations on the relations of an underlying set, giving rise to multisorted algebras we call first order algebras. We present universal axioms so that an algebra satisfies…
We prove a general decomposition theorem for the modal $\mu$-calculus $L_\mu$ in the spirit of Feferman and Vaught's theorem for disjoint unions. In particular, we show that if a structure (i.e., transition system) is composed of two…
Equational unification of two terms consists of finding a substitution that, when applied to both terms, makes them equal modulo some equational properties. Equational unification is of special relevance to automated deduction, theorem…
We present a unified deductive verification framework for first-order temporal properties based on well-founded rankings, where verification conditions are discharged using SMT solvers. To that end, we introduce a novel reduction from…
Reynold's parametricity theory captures the property that parametrically polymorphic functions behave uniformly: they produce related results on related instantiations. In dependently-typed programming languages, such relations and…
We bring forward a logical system of transition algebras that enhances many-sorted first-order logic using features from dynamic logics. The sentences we consider include compositions, unions, and transitive closures of transition…
The theory of finite term algebras provides a natural framework to describe the semantics of functional languages. The ability to efficiently reason about term algebras is essential to automate program analysis and verification for…
Semi-unification is the combination of first-order unification and first-order matching. The undecidability of semi-unification has been proven by Kfoury, Tiuryn, and Urzyczyn in the 1990s by Turing reduction from Turing machine immortality…
This work addresses certain ambiguities in the Dirac approach to constrained systems. Specifically, we investigate the space of so-called ``rigging maps'' associated with Refined Algebraic Quantization, a particular realization of the Dirac…
Suppose that G is a locally compact abelian group, and write M(G) for the algebra of bounded, regular, complex-valued measures under convolution. A measure \mu in M(G) is said to be idempotent if \mu * \mu = \mu, or alternatively if the…
First-order optimization methods have attracted a lot of attention due to their practical success in many applications, including in machine learning. Obtaining convergence guarantees and worst-case performance certificates for first-order…
The uniform interpolation property in a given logic can be understood as the definability of propositional quantifiers. We mechanise the computation of these quantifiers and prove correctness in the Coq proof assistant for three modal…
A constructive proof of the Goedel-Rosser incompleteness theorem has been completed using the Coq proof assistant. Some theory of classical first-order logic over an arbitrary language is formalized. A development of primitive recursive…
For a locally compact group $G$, let $A(G)$ be its Fourier algebra, let $M_{cb}A(G)$ denote the completely bounded multipliers of $A(G)$, and let $A_{Mcb}(G)$ stand for the closure of $A(G)$ in $M_{cb}A(G)$. We characterize the norm one…