ABSTRACT. Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. In this paper, we study this particular theory of datatypes and prove that it is strongly polite, showing also how it can be combined with other arbitrary disjoint theories using polite combination. Our results cover both inductive and finite datatypes, as well as their union. The combination method uses a new, simple, and natural notion of additivity, that enables deducing strong politeness from (weak) politeness.

ABSTRACT. Uniform interpolants were largely studied in non-classical propositional logics since the nineties, and their connection to model completeness was pointed out in the literature. A successive parallel research line inside the automated reasoning community investigated uniform quantifier-free interpolants (sometimes referred to as “covers”) in first-order theories. In this paper, we investigate cover transfer to theory combinations in the disjoint signatures case. We prove that, for convex theories, cover algorithms can be transferred to theory combinations under the same hypothesis needed to transfer quantifier-free interpolation (i.e., the equality interpolating property, aka strong amalgamation property). The key feature of our algorithm relies on the extensive usage of the Beth definability property for primitive fragments to convert implicitly defined variables into their explicitly defining terms. In the non-convex case, we show by a counterexample that cover may not exist in the combined theories.

ABSTRACT. This paper is concerned with logic-based modeling and automated reasoning for estimating the current state of a system as it evolves over time. The main motivation is situational awareness, which requires to being able to understand and explain a system's current state, at any time, and at a level that matters to the user, even if only partial or incorrect information about the external events leading to that state is available.

The paper proposes to represent such states as models of a logical specification of the properties of interest and a given a set of external timestamped events up to ``now''. The underlying modeling language is a grounded in logic programming, and models are computed in a bottom-up way. It adopts notions of stratification, default negation and a possible model semantics for its (disjunctive) program rules. In order to deal with less-than-perfect event data, the modeling language features a novel model revision operator that allows the programmer to formulate conditions under which a model computation with a corrected set of events should be attempted in an otherwise inconsistent state.

Model computation and revision has a long history in the area of logic programming. The novelty of our approach lies in the specifics of the stratification employed, in terms of time and in terms of whether a fact is an external event or derived, and in the specifics of the model revision operator. Our approach deliberately compromises on generality for the benefit of low complexity and any-time reasoning capabilities as needed to support situational awareness application well.

The paper provides the technical details of the approach. The main theoretical results are soundness and completeness of the proposed model computation algorithm. On the applied side, the paper describes an implementation as a shallow embedding into the Scala programming language by means of the Scala macro mechanism. This is important in practice, as it gives the programmer built-in access to a full-fledged programming language and its associated libraries. The paper sketches the usefulness of this feature and the model revision operator with a small example for supply chain situational awareness.

ABSTRACT. SGGS (Semantically-Guided Goal-Sensitive reasoning) is a conflict-driven first-order theorem-proving method which is refutationally complete and model complete in the limit. These features make it attractive as a basis for decision procedures. In this paper we show that SGGS decides the stratified fragment which generalizes EPR, the PVD fragment, and a new fragment that we dub restrained. The new class has the small model property, as the size of SGGS-generated models can be upper-bounded, and is also decided by hyperresolution and ordered resolution. We report on experiments with a termination tool implementing a restrainedness test, and with an SGGS prototype named Koala.

ABSTRACT. We present a practical proof search procedure for Coq based on a direct search for type inhabitants in an appropriate normal form. An implementation in a Coq plugin is available. It significantly outperforms the automation natively available in Coq, proving in 30s, with no ATP input, 40.9% of 4494 theorems from a collection of Coq libraries and 17.1% of CompCert. As a reconstruction backend for CoqHammer, the procedure achieves reconstruction success rates in the range 87-97%.

For efficiency, our procedure is not complete for the Calculus of Inductive Constructions, but it is complete for a first-order fragment. Even in pure intuitionistic first-order logic, with large enough time limit our method outperforms Coq’s "firstorder" tactic, achieving a 29.5% success rate on the ILTP library of first-order intuitionistic problems.

ABSTRACT. Faces play a central role in the combinatorial and computational aspects of polyhedra. In this paper, we present the first formalization of faces of polyhedra in the proof assistant Coq. This builds on the formalization of a library providing the basic constructions and operations over polyhedra, including projections, convex hulls and images under linear maps. Moreover, we design a special mechanism which automatically introduces an appropriate representation of a polyhedron or a face, depending on the context of the proof. We demonstrate the usability of this approach by establishing some of the most important combinatorial properties of faces, namely that they constitute a family of graded atomistic and coatomistic lattices closed under sublattices.

ABSTRACT. We study finite first-order satisfiability (FSAT) in the constructive setting of dependent type theory. Employing synthetic accounts of enumerability and decidability, we give a full classification of FSAT depending on the first-order signature of non-logical symbols. On the one hand, our development focuses on Trakhtenbrot's theorem, stating that FSAT is undecidable as soon as the signature contains an at least binary relation symbol. Our proof proceeds by a many-one reduction chain starting from the Post correspondence problem. On the other hand, we establish the decidability of FSAT for monadic first-order logic, i.e. where the signature only contains at most unary function and relation symbols, as well as the enumerability of FSAT for arbitrary enumerable signatures. All our results are mechanised in the framework of a growing Coq library of synthetic undecidability proofs.

ABSTRACT. Coding conventions for naming, spacing, and other essentially stylistic properties are necessary for developers to effectively understand, review, and modify source code in large software projects. Consistent conventions in verification projects based on proof assistants, such as Coq, increase in importance as projects grow in size and scope. While conventions can be documented and enforced manually at high cost, emerging approaches automatically learn and suggest idiomatic names in Java-like languages by applying statistical language models on large code corpora. However, due to its powerful language extension facilities and fusion of type checking and computation, Coq is a challenging target for automated learning techniques. We present novel generation models for learning and suggesting lemma names for Coq projects. Our models, based on multi-input neural networks, are the first to leverage syntactic and semantic information from Coq’s lexer (tokens in lemma statements), parser (syntax trees), and kernel (elaborated terms); the key insight is that learning from elaborated terms can substantially boost model performance. We implemented our models in a toolchain, dubbed Roosterize, and applied it to learn from a large corpus of code derived from the Mathematical Components family of projects, known for its stringent coding conventions. Our results show that Roosterize substantially outperforms baselines for suggesting lemma names, highlighting the importance of using multi-input models and elaborated terms.

ABSTRACT. Sharing of notations and theories across an inheritance hierarchy of mathematical structures, e.g., groups and rings, is important for productivity when formalizing mathematics in proof assistants. The packed classes methodology is a generic design pattern to define and combine mathematical structures in a dependent type theory with records. When combined with mechanisms for implicit coercions and unification hints, packed classes enable automated structure inference and subtyping in hierarchies, e.g., that a ring can be used in place of a group. However, large hierarchies based on packed classes are challenging to implement and maintain. We identify two hierarchy invariants that ensure modularity of reasoning and predictability of inference with packed classes, and propose algorithms to check these invariants. We implement our algorithms as tools for the Coq proof assistant, and show that they significantly improve the development process of Mathematical Components, a library for formalized mathematics.

ABSTRACT. This article gives an elementary computational proof of the group law for Edwards elliptic curves. The associative law is expressed as a polynomial identity over the integers that is directly checked by polynomial division. Unlike other proofs, no preliminaries such as intersection numbers, Bezout's theorem, projective geometry, divisors, or Riemann Roch are required. The proof of the group law has been formalized in the Isabelle/HOL proof assistant.

ABSTRACT. The word problem for a finite set of ground identities is known to be decidable in polynomial time using congruence closure, and this is also the case if some of the function symbols are assumed to be commutative. We show that decidability in P is preserved if we add the assumption that certain function symbols f are extensional in the sense that f(s1,...,sn) = f(t1,...,t) implies s1 = t1,...,sn = tn. In addition, we investigate a variant of extensionality that is more appropriate for commutative function symbols, but which raises the complexity of the word problem to coNP.

ABSTRACT. In text-encoding standards such as Unicode, text strings are sequences of code points, each of which can be represented as a natural number. We present a decision procedure for a (concatenation-free) theory of strings that includes length and a conversion function from strings to integer code points. Furthermore, we show that many common string operations, such as conversions between lowercase and uppercase, can be naturally encoded using this conversion function. We implement our approach in the SMT solver CVC4, which contains a state-of-the-art string subsolver, and show that the use of a native procedure for code points significantly improves its performance with respect to other state-of-the-art string solvers.

ABSTRACT. We report on the new version of mu-term, a tool for proving termination properties of variants of rewrite systems, including conditional, context-sensitive, equational, and order-sorted rewrite systems.

ABSTRACT. Given a Conditional Term Rewriting System (CTRS) R and terms s and t, the reachability condition s ->* t is called feasible if there is a substitution σ such that σ(s) ->*_R σ(t) holds; otherwise, it is infeasible. Checking infeasibility of (sequences of) reachability conditions is important in the analysis of computational properties of CTRSs like confluence or operational termination. In this paper, we generalize this notion of feasibility to enable the use of other relations (e.g., subterm |>, context-sensitive rewriting \->, etc.) defined by first-order theories, so that more general properties can be investigated. We introduce a framework for proving feasibility/infeasibility, and a new tool, infChecker, which implements it.

ABSTRACT. N-PAT is a new model-checking tool that supports the verification of nested-models -- i.e. models whose behavior depends on the results of verification tasks. In this paper, we describe its operation and discuss mechanisms that are tailored to the efficient verification of nested-models. Further, we motivate the advantages of N-PAT over traditional model-checking tools through a network security case study.