ABSTRACT. The cvc5 SMT solver solves quantifier-free nonlinear real arithmetic problems by combining the cylindrical algebraic coverings method with incremental linearization in an abstraction-refinement loop. The result is a complete algebraic decision procedure that leverages efficient heuristics for refining candidate models. Furthermore, it can be used with quantifiers, integer variables, and in combination with other theories. We describe the overall framework, individual solving techniques, and a number of implementation details. We demonstrate its effectiveness with an evaluation on the SMT-LIB benchmarks.

ABSTRACT. We propose a new calculus SCL(EQ) for first-order logic with equality that only learns non-redundant clauses. Following the idea of CDCL (Conflict Driven Clause Learning) and SCL (Clause Learning from Simple Models) a ground literal model assumption is used to guide inferences that are then guaranteed to be non-redundant. Redundancy is defined with respect to a dynamically changing ordering derived from the ground literal model assumption. We prove SCL(EQ) sound and complete and provide examples where our calculus improves on superposition.

ABSTRACT. Theories axiomatised by unit equalities include problems in group theory, loops, lattices, and other algebraic structures are notoriously difficult for general purpose theorem provers. Provers specialised for unit equational theories (UEQ) are based on Knuth-Bendix (KB) completion in contrast to provers applicable to general equational problems which are based on the superposition calculus. Although Knuth-Bendix completion and superposition are closely related, a number of simplifications which make Knuth-Bendix completion efficient are not available in superposition.

In particular, key simplifications such as ground joinability, although known for more than 30 years, have not been extended from KB completion to superposition. In fact, all previous completeness proofs for ground joinability rely on proof orderings and proof reductions, which are not easily extensible to general clauses together with redundancy elimination. In this paper we address this limitation and extend superposition with ground joinability, and show that under an adapted notion of redundancy, simplifications based on ground joinability preserve completeness.

Another recently introduced simplification for UEQ is connectedness. We extend this notion to “ground connectedness” and show superposition is complete with both connectedness and ground connectedness.

We implemented ground joinability in a theorem prover, iProver, using a novel algorithm which we also present in this paper, and evaluated over the TPTP library with encouraging results.

ABSTRACT. We propose generalizations of reduction pairs, well-established techniques for proving termination of term rewriting, in order to prove unsatisfiability of reachability (infeasibility) in plain and conditional term rewriting. We adapt the weighted path order, a merger of the Knuth-Bendix order and the lexicographic path order, into the proposed framework. The proposed approach is implemented in the termination prover NaTT, and the strength of our approach is demonstrated through examples and experiments.

ABSTRACT. The importance of subsumption testing for redundancy elimination in first-order logic automatic reasoning is well-known. Although the problem is already NP-complete for first-order clauses, the meanwhile developed test pipelines efficiently decide subsumption in almost all practical cases. We consider subsumption between first-oder clauses of the Bernays-Schönfinkel fragment over linear, real arithmetic constraints: BS(LRA). The bottleneck in this setup is deciding implication between the LRA constraints of two clauses. Our new sample point heuristic preempts expensive implication decisions in about 94% of all cases in benchmarks. Combined with filtering techniques for the first-order BS part of clauses, it results again in an efficient subsumption test pipeline for BS(LRA) clauses.

ABSTRACT. We present new results on the application of semantic- and knowledge-based reasoning techniques to the analysis of cloud deployments. In particular, to the security of Infrastructure as Code configuration files, encoded as description logic knowledge bases. We introduce an action language to model mutating actions; that is, actions that change the structural configuration of a given deployment by adding, modifying, or deleting resources. We mainly focus on two problems: the problem of determining whether the execution of an action, no matter the parameters passed to it, will not cause the violation of some security requirement (static verification), and the problem of finding sequences of actions that would lead the deployment to a state where (un)desirable properties are (not) satisfied (plan existence and plan synthesis). For all these problems, we provide definitions, complexity results, and decision procedures.

ABSTRACT. Our goal is to develop a logic-based component for hybrid – machine learning plus logic – commonsense question answering systems. The paper presents an implementation GK of default logic for handling rules with exceptions in unrestricted first order knowledge bases. GK is built on top of our existing automated reasoning system with confidence calculation capabilities. To overcome the problem of undecidability of checking potential exceptions, GK performs delayed recursive checks with diminishing time limits. These are combined with the taxonomy-based priorities for defaults and numerical confidences.

ABSTRACT. The modal logic K is commonly used to represent and reason about necessity and possibility and its extensions with combinations of additional axioms is used to represent knowledge, belief, desires and intentions. Here we present local reductions of all propositional modal logics in the so-called modal cube, that is, extensions of K with arbitrary combinations of the axioms B, D, T, 4 and 5 to a normal form comprising a formula and the set of modal levels it occurs at. Using these reductions we can carry out reasoning for all these logics with the theorem prover KSP. We define benchmarks for these logics and experiment with the reduction approach as compared to an existing resolution calculus with specialised inference rules for the various logics.

ABSTRACT. Explanations for description logic (DL) entailments provide important support for the design and maintenance of large ontologies. The "justifications" usually employed for this purpose in ontology editors pinpoint the parts of the ontology responsible for a given entailment. Proofs for entailments make the intermediate reasoning steps explicit, and thus explain how a consequence can actually be derived. We present an interactive system for exploring description logic proofs, called Evonne, which not only visualizes proofs of consequences for ontologies written in expressive DLs, but also offers several proof generation procedures and various functions for condensing large proofs.

ABSTRACT. To give concise explanations for a conclusion obtained by reasoning over ontologies, justifications have been proposed as minimal subsets of an ontology that entail the given conclusion. Even though computing one justification can be done in polynomial time for tractable Description Logics such as EL+, computing all justifications is complicated and often challenging for real-world ontologies. In this paper, based on a graph representation of EL+-ontologies, we propose a new set of inference rules (called H-rules) and take advantage of them for providing a new method of computing all justifications for a given conclusion. The advantage of our setting is that most of the time, it reduces the number of inferences (generated by H-rules) required to derive a given conclusion. This accelerates the enumeration of justifications relying on these inferences. We validate our approach by running real-world ontology experiments. Our graph-based approach outperforms PULi, the state-of-the-art algorithm, in most of cases.

ABSTRACT. We present a decision procedure for intermediate logics relying on a modular extension of the SAT-based proof search-engine intuitR for intuitionistic propositional logic. Given the module for the intermediate logic L, our procedure iteratively searches for a Kripke countermodel for a formula A, exploiting the search engine of intuitR: whenever a countermodel for A is built, the module checks whether it is a model of the logic L. If this is the case A is not valid in L. Otherwise, the module provides an instance of an axiom of L falsified in the countermodel that is fed to the SAT-solver for a new try. We prove the partial correctness of our procedure and its termination for some well-known intermediate logics.

ABSTRACT. The propagation redundant (PR) proof system generalizes the resolution and resolution asymmetric tautology proof systems used by conflict-driven clause learning (CDCL) solvers. PR allows short proofs of unsatisfiability for some problems that are difficult for CDCL solvers. Previous attempts to automate PR clause learning used hand-crafted heuristics that work well on some highly-structured problems. For example, the solver SaDiCaL incorporates PR clause learning into the CDCL loop, but it cannot compete with modern CDCL solvers due to its fragile heuristics. We present PReLearn, a preprocessing technique that learns short PR clauses. Adding these clauses to a formula reduces the search space that the solver must explore. By performing PR clause learning as a preprocessing stage, PR clauses can be found efficiently without sacrificing the robustness of modern CDCL solvers. On a large number of SAT competition benchmarks we found that preprocessing with PReLearn significantly improves solver performance on both satisfiable and unsatisfiable formulas. PReLearn supports proof logging, giving a high level of confidence in the results.

ABSTRACT. The study of clause redundancy in Boolean satisfiability (SAT) has proven significant in various terms, from fundamental insights into preprocessing and inprocessing to the development of practical proof checkers and new types of strong proof systems. We study liftings of the recently-proposed notion of propagation redundancy---based on a semantic implication relationship between formulas---in the context of maximum satisfiability (MaxSAT), where of interest are reasoning techniques that preserve optimal cost (in contrast to preserving satisfiability in the realm of SAT). We establish that the strongest MaxSAT-lifting of propagation redundancy allows for changing in a controlled way the set of minimal correction sets in MaxSAT. This ability is key in succinctly expressing MaxSAT reasoning techniques and allows for obtaining correctness proofs in a uniform way for MaxSAT reasoning techniques very generally. Bridging theory to practice, we also provide a new MaxSAT preprocessor incorporating such extended techniques, and show through experiments its wide applicability in improving the performance of modern MaxSAT solvers.

ABSTRACT. We describe a system that detects an invariance in a problem expressed in a logical formula and simplifies it by eliminating variables utilizing the invariance. Pre-defined function and predicate symbols in the problem representation language are associated with algebraically indexed types, which signify the invariance property of them. A Hindley-Milner style type reconstruction algorithm is derived for detecting the invariance of a problem. In the experiment, the invariance-based formula simplification significantly enhanced the performance of a problem solver based on quantifier-elimination for real-closed fields, especially on the problems taken from the International Mathematical Olympiads.

ABSTRACT. Philosophers since Thales have demanded valid proofs as the litmus test for the acceptance of a mathematical conjecture as a demonstrable fact. Dually, counterexamples have served as evidence for the demonstrable falsity of a claim. Euclid's codification of the rules of geometry proofs became the paradigm for a foundation for reliable knowledge. With Ramon Llull and Gottfried Leibniz came the idea of mechanizing reason with the unreasonable expectation that this would spark religious and political harmony. The quest for the automation of mathematical reasoning came into sharp focus through the Hilbert's second and tenth problem. The Entscheidungsproblem posed by Hilbert and Ackermann was answered negatively by Church and Turing. The work of logicians in the first half of the 20th century laid the foundation for the development of early theorem-proving programs in the fifties. Skipping ahead, by the dawn of the eighties, automated reasoning had a niche position within the field of artificial intelligence but was still regarded with amusement by outsiders as a somewhat quixotic quest to discover the holy grail of problem solving. We describe the experience of sharing a ringside seat to the growth and maturation of the field of automated reasoning during the last four decades into an integral sub-discipline of computing and a vehicle for the large-scale formalization of mathematical and computational knowledge.