ABSTRACT. We propose a lazy decision procedure for the logic WSkS. It builds a term-based symbolic representation of the state space of the tree automaton (TA) constructed by the classical WSkS decision procedure. The classical decision procedure transforms the symbolic representation into a TA via a bottom-up traversal and then tests its language non-emptiness, which corresponds to satisfiability of the formula. On the other hand, we start evaluating the representation from the top, construct the state space on the fly, and utilize opportunities to prune away parts of the state space irrelevant to the language emptiness test. In order to do so, we needed to extend the notion of language terms (denoting language derivatives) used in our previous procedure for the linear fragment of the logic (the so-called WS1S) into automata terms. We implemented our decision procedure and identified classes of formulae on which our prototype implementation is significantly faster than the classical procedure implemented in the Mona tool.

ABSTRACT. In this work we introduce the notion of decisional width of a finite relational structure and the notion of regular-decisional width for regular classes of finite structures. We show that the validity prob- lem for regular-decisional classes of structures is decidable. Building on this decidability result, we show that the problem of counting satisfying assignments for a first order formula in a structure of constant width is fixed parameter tractable with respect to the width parameter and can be solved in quadratic time with respect to the size of the representation.

ABSTRACT. Several decision procedures for the Bernays-Schoenfinkel fragment of first-order logic rely on explicit model assumptions. In particular, the procedures differ in their respective model representation formalisms. We introduce a new decision procedure SCL for clause learning from simple models. Simple models are solely build on ground literals. Nevertheless, we show that SCL can learn exactly the clauses other procedures learn with respect to more complex model representation formalisms. Therefore, the overhead of complex model representation formalisms is not always needed.

ABSTRACT. We describe a large set of related theorem proving problems obtained by translating theorems from the HOL4 standard library into multiple ATP formalisms. The translations give representations in higher-order logic (with and without type variables) and first-order logic (possibly with multiple types and possibly with type variables). The problem sets allow us to run theorem provers designed for different logics on related problem sets and compare their performance. This also results in a new "grand unified" large theory benchmark that emulates the ITP/ATP hammer setting, where systems and metasystems can use multiple ATP formalisms in complementary ways and jointly learn from the accumulated knowledge.

ABSTRACT. We designed a superposition calculus for a clausal fragment of extensional polymorphic higher-order logic that includes anonymous functions but excludes Booleans. The inference rules work on βη-equivalence classes of λ-terms and rely on higher-order unification to achieve refutational completeness. We implemented the calculus in the Zipperposition prover and evaluated it on TPTP and Isabelle benchmarks. The results suggest that superposition is a suitable basis for higher-order reasoning.

ABSTRACT. First-order theorem provers are commonly utilised as back ends to interactive theorem provers. In order to improve efficiency, it is desirable that such provers can carry out some higher-order reasoning. In his 1991 paper, Dougherty proposed a combinatory unification algorithm for higher-order logic. The algorithm removes the need to deal with $\lambda$-binders and $\alpha$-renaming, making it attractive to implement in first-order provers. However, since publication it has garnered little interest due to its poor characteristics. It fails to terminate on many trivial instances and requires polymorphism. We present a restricted version of Dougherty's algorithm that is incomplete, terminating and does not require polymorphism. Further, we describe its implementation in the Vampire theorem prover, including a novel use of a substitution tree as a filtering index for higher-order unification. Finally, We analyse the performance of the algorithm on the higher-order portion of the TPTP problem library and show that it is a significant step forward.

ABSTRACT. SMT solvers have throughout the years been able to cope with increasingly expressive formulas, from ground logics to full first-order logic (FOL). Nevertheless, higher-order logic (HOL) within SMT is still little explored. We propose a pragmatic extension for SMT solvers to natively support HOL reasoning without compromising performance on FOL reasoning, thus leveraging the extensive research and implementation efforts dedicated to efficient SMT solving. We show how to generalize data structures and the ground decision procedure to support partial applications and extensionality, as well as how to reconcile instantiation techniques with functional variables. We also discuss a separate approach for redesigning an SMT solver to HOL via new data structures and algorithms. We apply the pragmatic extension to the CVC4 SMT solver and redesign the veriT solver. Our evaluation shows they are competitive with state-of-the-art HOL provers and often outperform the traditional encoding into FOL.