Separation logic (SL) is a widely used formalism for verifying programs that manipulate dynamically allocated memory, relying on the separating conjunction ⋆ to combine disjoint heap structures. The standard approach in SL lacks the expressive power to handle overlaid data structures where multiple structures share some locations. We consider a logic that extends SL with a new separating conjunction operator , enabling the composition of heaps with shared locations that allocate distinct fields. Our fragment supports generic inductive definitions and introduces set variables to constrain the locations shared by overlapping structures. We prove that the satisfiability problem for this fragment is in Nexptime, by reducing it to the satisfiability problem in BAPA [11], a decidable logic combining Boolean algebra of sets and Presburger arithmetic.
Parametric array theories are extensions of the quantifier-free theory of arrays with relations that hold componentwise. We observe that decision procedures for the satisfiability of these theories rely on a kind of finite witnessability property. We use this insight to show the politeness of these theories with respect to the index and element sorts. Our results clarify the politeness of the theory of sets with the cardinality operator, which was left open in the literature.
Evonne is a web application primarily designed to explain Description Logic (DL) entailments using an interactive visualization approach for proofs. This paper introduces an extension of Evonne to DLs with concrete domains, which are needed for formalizing concepts whose definitions involve quantitative information. Specifically, we focus on two extensions of the DL ℰℒ_ : one with constraints formulated as linear equations and the other with difference constraints. First, we have extended Evonne to enable the generation and presentation of proofs involving these concrete domains. Then, leveraging the unique properties of each domain, we have designed and incorporated alternative visual explanations for the numerical parts of the proofs. Finally, we have assessed the effectiveness of these visual explanations through qualitative user studies and a performance benchmark. While opinions on one of these explanations varied, the other was widely recognized for its clarity and ease of understanding.
We establish a data-driven method for the assessment of the runtime complexity of first-order term rewrite systems (TRSs for short). The fully automated complexity analysis of TRSs has a long tradition in rewriting and numerous sophisticated static analysis methods have been developed. The recent success in machine learning motivates the quest for data-driven analysis techniques, which, while unsound in principle, can potentially return insightful upper bounds on the runtime complexity where traditional (static) techniques fail. We present the first such technique based on bottom-up rule unfolding, akin to a variant of backward narrowing. Further, we employ a dedicated notion of data fitting that is fine-tuned to the estimation of asymptotic complexities. We provide ample experimental data indicating the viability of the approach.
One of the most fascinating examples of the failure of Beth's definability theorem and, consequently, of Craig's interpolation theorem, is quantified S5. In this paper, we intend to establish the interpolation property for fragments of quantified S5 using a formulation of the semantics of quantified S5 as an analytic calculus in its own right. This is especially straightforward for S5, because necessity (possibility) in S5 means for all worlds (there exists a world), and we have simply to extend every predicate by a world position (worlds and objects are to be considered as separate entities).
The recently introduced dependent typed higher-order logic (DHOL) offers an interesting compromise between expressiveness and automation support. It sacrifices the decidability of its type system in order to significantly extend its expressiveness over standard HOL. Yet it retains strong automated theorem proving support via a sound and complete translation to HOL. We leverage this design to extend DHOL with refinement and quotient types. Both of these are commonly requested by practitioners but rarely provided by automated theorem provers. This is because they inherently require undecidable typing and thus are very difficult to retrofit to decidable type systems. But with DHOL already doing the heavy lifting, adding them is not only possible but elegant and simple. Concretely, we add refinement and quotient types as special cases of subtyping. This turns the associated canonical inclusion resp. projection maps into identity maps and thus avoids costly changes in representation. We present the syntax, semantics, and translation to HOL for the extended language, including the proofs of soundness and completeness.
The ℰℒ family of description logics facilitates efficient polynomial-time reasoning and has been standardized as the profile OWL 2 EL of the Web Ontology Language. ℰℒ can represent and reason not only with symbolic knowledge but also with concrete knowledge expressed by numbers, strings, and other concrete datatypes. Such concrete domains must be convex to avoid introducing disjunctions “through the backdoor.” However, existing concrete domains provide only limited utility. In order to overcome this issue, we introduce a novel form of concrete domains based on semi-lattices. They are convex by design and can thus be integrated into Horn-DLs such as ℰℒ . Moreover, they allow for FBoxes to express dependencies between concrete features. We describe four instantiations concerned with real intervals, 2D-polygons, regular languages, and graphs.
Standard Description Logics (DLs) can encode quantitative aspects of an application domain through either number restrictions, which constrain the number of individuals that are in a certain relationship with an individual, or concrete domains, which can be used to assign concrete values to individuals using so-called features. These two mechanisms have been extended towards very expressive DLs, for which reasoning nevertheless remains decidable. Number restrictions have been generalized to more powerful comparisons of sets of role successors in 𝒜ℒ𝒞𝒮𝒞𝒞 , while the comparison of feature values of different individuals in 𝒜ℒ𝒞 (𝔇) has been studied in the context of ω -admissible concrete domains 𝔇 . In this paper, we combine both formalisms and investigate the complexity of reasoning in the thus obtained DL 𝒜ℒ𝒞𝒪𝒮𝒞𝒞(𝔇) , which additionally includes the ability to refer to specific individuals by name. We show that, in spite of its high expressivity, the consistency problem for this DL is ExpTime-complete, assuming that the constraint satisfaction problem of 𝔇 is also decidable in exponential time. It is thus not higher than the complexity of the basic DL 𝒜ℒ𝒞 . At the same time, we show that many natural extensions to this DL, including a tighter integration of the concrete domain and number restrictions, lead to undecidability.
Monomorphisation can be used to extend monomorphic provers to support polymorphic logics. We describe a pragmatic iterative approach. We implemented it in the Zipperposition prover, where it is used to translate away polymorphism before invoking the monomorphic prover E as a backend. Our evaluation shows that this approach increases Zipperposition's success rate. Moreover, we find that iterative monomorphisation outperforms some native implementations of polymorphism.
We consider the reasoning problem of logical consequence between simple statements about the behaviour of continuous functions on certain intervals, representing the way that variables influence each other. Automated reasoning for such statements has applications in formal modelling of classroom experiments in natural sciences. A previous attempt, employing a simple proof system for this reasoning task, is known to be incomplete and unlikely to be extendable to obtain completeness for arbitrary experiments. Here we develop an algebraic approach in the form of an abstraction of the uncountable space of finite collections of continuous, real-valued functions, connected by a composition principle, into finitely many representatives of equivalence classes. We show that this is sufficient for the reasoning task at hand. The approach achieves completeness under very reasonable restrictions of the involved statements, extending what has previously been achieved using proof-theoretic means, and yields an upper bound of coNP.
In this paper, we consider the knowledge problems of deduction and static equivalence in the formal analysis of security protocols. We extend a recent result that developed a decision procedure for these problems in the non-disjoint combination R ∪ E , where R is a subterm E -convergent term rewrite system (TRS) and E is a restricted form of permutative theory. Here, we consider the same combination problem but replace the subterm E -convergent TRS with a superclass of subterm E -convergent, called contracting E -convergent. We show that the previous decision procedure can be extended to obtain a new algorithm for this larger class of combined theories. We also explore the gap between the contracting TRSs, for which deduction and static-equivalence are decidable, and a larger superclass called graph-embedded for which these problems are undecidable. This gap is of interest since one would like to get closer to graph-embedded and still maintain decidability of the above “knowledge problems.” We show that at least one way of weakening the restrictions of the contracting definition will not work, as it leads to undecidability results for deduction and static equivalence. We also show that a subset of the graph-embedded rules is still sufficient to obtain undecidability.
Nielsen transformation is a standard approach for solving word equations: by repeatedly splitting equations and applying simplification steps, equations are rewritten until a solution is reached. When solving a conjunction of word equations in this way, the performance of the solver will depend considerably on the order in which equations are processed. In this work, the use of Graph Neural Networks (GNNs) for ranking word equations before and during the solving process is explored. For this, a novel graph-based representation for word equations is presented, preserving global information across conjuncts, enabling the GNN to have a holistic view during ranking. To handle the variable number of conjuncts, three approaches to adapt a multi-classification task to the problem of ranking equations are proposed. The training of the GNN is done with the help of minimum unsatisfiable subsets (MUSes) of word equations. The experimental results show that, compared to state-of-the-art string solvers, the new framework solves more problems in benchmarks where each variable appears at most once in each equation.
We introduce the notion of weighted abstract reduction systems (weighted ARSs), generalising standard and relative ARSs by allowing non-uniform weights on transition steps. Weighted ARSs give rise to a theory of rewriting where quantitative properties-noteworthy complexity related properties-can be more directly studied. Unlike these standard notions, weighted ARSs permit the study of quantitative properties of reduction systems of non-uniform weight, such as the analysis of expectation-based properties of probabilistic systems. We establish ranking functions as a means to analyse (strong) boundedness of weighted ARSs, i.e., the property that weights of reductions are bounded from above. We showcase their applicability by instantiating them to weighted term rewrite systems and probabilistic reduction systems, the latter generalising Lyapunov ranking functions to reason about expected derivation heights.
When humans evaluate the validity of a logical conclusion, they naturally consider its meaning and its context, allowing them to focus on relevant information and to avoid unnecessary inferences. For example, when asked to prove that all hammocks are also beds, they will certainly not draw conclusions about vehicles or weapons. In contrast, automated theorem provers typically do not account for the contextual meaning of a conclusion when selecting inference steps. Existing heuristics for selecting the clause for the next inference step usually ignore the meaning of symbol names, overlooking valuable contextual information. As a result, in the example above, clauses with symbol names such as weapon or vehicle could well be found in the processed clauses. However, since these clauses are not required for the actual proof, they are not helpful to the prover and tend to distract from the actual proof task. In this paper, we present an approach that uses natural language processing techniques to align the selection of the clause for the next inference step with the meaning of the proof goal. Our implementation and experimental results show that this method not only increases the number of successful proofs but also reduces the number of clauses processed during proof search.
Modern SMT solvers can generate proofs of unsatisfiability so that the result can be checked independently. A dependable approach to verify these proofs is to reconstruct them within a proof assistant. In previous work, the SMT checker Carcara was extended to reconstruct SMT proofs in Lambdapi-a proof assistant designed for interoperability, supporting the import and export of proofs for integration with other proof assistants such as Rocq, Lean, or HOL- Light. Whereas that work was limited to SMT theories without arithmetic, we here present an extension that enables the reconstruction of SMT proofs involving linear integer arithmetic.
SAT-based model checking has become a prominent approach to the verification of temporal properties. However, while invariant model checking can produce simple proofs based on induction, proof generation for SAT-based model checking of liveness properties is much more complex. In this paper, we focus on a recently developed algorithm, called rlive, which has been proved quite effective in practice. rlive tries to find a counterexample with a series of reachability checks, while iteratively blocking shoals, i.e., set of states that cannot be extended with fair paths. Despite the complexity of the algorithm, we show that the shoals are sufficient to generate a proof in a deductive system for temporal properties. We implement the approach in an existing certifying model checking framework based on the PVS theorem prover, and we experimentally evaluate it on liveness verification problems from the hardware model checking competition, generating proofs using the nuXmv model checker and checking them with PVS.
Shininess and strong politeness are properties related to theory combination procedures. In a paper titled "Many-sorted equivalence of shiny and strongly polite theories", Casal and Rasga proved that for decidable theories, these properties are equivalent. We refine their result by showing that: (i) shiny theories are always decidable, and therefore strongly polite; and (ii) there are (undecidable) strongly polite theories that are not shiny. This line of research is tightly related to a recent series of papers that have sought to classify all the relations between theory combination properties. We finally complete this project, resolving all of the remaining problems that were previously left open.
Considering patterns as sets of their instances, a difference operator over patterns computes a finite set of two given patterns, which represents the difference between the dividend pattern and the divisor pattern. A complement of a pattern is a pattern set, the ground constructor instances of which comprise the complement of the ground constructor instances of the former pattern. Given finitely many unconstrained linear patterns, using a difference operator over linear patterns, a complement algorithm returns a finite set of linear patterns as a complement of the given patterns. In this paper, we extend the difference operator and complement algorithm to constrained linear patterns used in logically constrained term rewrite systems (LCTRSs, for short) that have no user-defined constructor term with a sort for built-in values. Then, as for left-linear term rewrite systems, using the complement algorithm, we show that quasi-reducibility is decidable for such LCTRSs with decidable built-in theories. For the single use of the difference operator over constrained patterns, only divisor patterns are required to be linear.
Much of the current research and development in the field of automated reasoning builds on the infrastructure provided by the TPTP World. The TPTP language for logical formulae is central to the far-reaching adoption of the TPTP World. This paper introduces the Dependently Typed higher-order Form (DHF) of the TPTP language. It takes advantage of already established binders in the syntax, and is thus a minimally intrusive extension to the Typed Higher-order Form (THF). A starting set of over 100 problems is provided to exhibit the usefulness and incite interest in DHF. Some tools that are already able to reason about problems in the DHF language are discussed.
The study of theory combination in Satisfiability Modulo Theories (SMT) involves various model theoretic properties (e.g., stable infiniteness, smoothness, etc.). We show that such properties can be partly captured by the natural density of the spectrum of the studied theories, which is the set of sizes of their finite models. This enriches the toolbox of the theory combination researcher, by providing new tools to determine the possibility of combining theories. It also reveals interesting and surprising connections between theory combination and number theory.
