Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

SAT-Inspired Higher-Order Eliminations

Jasmin Blanchette, Petar Vukmirović

TL;DR

This work extends SAT preprocessing techniques to clausal higher-order logic under Henkin semantics, introducing HLBE, SPE, DPE, PPE, BCE, and a novel QLE, with a practical implementation in Zipperposition. The methods aim to simplify problems by removing literals, clauses, or predicate symbols while preserving satisfiability properties, enabling more efficient automatic proof search. The paper provides theoretical guarantees (preservation under general interpretations) and applies the techniques in a comprehensive empirical study, finding notable gains on untyped first-order benchmarks but more modest improvements for higher-order problems, though the portfolio approach can still yield benefits. Overall, the contributions advance higher-order theorem proving by transferring and adapting proven propositional and first-order preprocessing strategies, highlighting both promise and current limitations for complex higher-order benchmarks.

Abstract

We generalize several propositional preprocessing techniques to higher-order logic, building on existing first-order generalizations. These techniques eliminate literals, clauses, or predicate symbols from the problem, with the aim of making it more amenable to automatic proof search. We also introduce a new technique, which we call quasipure literal elimination, that strictly subsumes pure literal elimination. The new techniques are implemented in the Zipperposition theorem prover. Our evaluation shows that they sometimes help prove problems originating from Isabelle formalizations and the TPTP library.

SAT-Inspired Higher-Order Eliminations

TL;DR

This work extends SAT preprocessing techniques to clausal higher-order logic under Henkin semantics, introducing HLBE, SPE, DPE, PPE, BCE, and a novel QLE, with a practical implementation in Zipperposition. The methods aim to simplify problems by removing literals, clauses, or predicate symbols while preserving satisfiability properties, enabling more efficient automatic proof search. The paper provides theoretical guarantees (preservation under general interpretations) and applies the techniques in a comprehensive empirical study, finding notable gains on untyped first-order benchmarks but more modest improvements for higher-order problems, though the portfolio approach can still yield benefits. Overall, the contributions advance higher-order theorem proving by transferring and adapting proven propositional and first-order preprocessing strategies, highlighting both promise and current limitations for complex higher-order benchmarks.

Abstract

We generalize several propositional preprocessing techniques to higher-order logic, building on existing first-order generalizations. These techniques eliminate literals, clauses, or predicate symbols from the problem, with the aim of making it more amenable to automatic proof search. We also introduce a new technique, which we call quasipure literal elimination, that strictly subsumes pure literal elimination. The new techniques are implemented in the Zipperposition theorem prover. Our evaluation shows that they sometimes help prove problems originating from Isabelle formalizations and the TPTP library.
Paper Structure (19 sections, 11 theorems, 9 equations, 1 figure)

This paper contains 19 sections, 11 theorems, 9 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Clausal Higher-Order Logic
  3. Syntax
  4. Semantics
  5. Hidden-Literal-Based Elimination
  6. Predicate Elimination
  7. Singular Predicate Elimination
  8. Defined Predicate Elimination
  9. Portfolio Predicate Elimination
  10. Blocked Clause Elimination
  11. Quasipure Literal Elimination
  12. Implementation
  13. Hidden-Literal-Based Elimination
  14. Predicate Elimination
  15. Blocked Clause Elimination
  16. ...and 4 more sections

Key Result

Theorem 4.11

Let $N$ be a finite clause set that is polymorphism-safe for ${\mathsf{p}}$ and ${\mathsf{p}}$ be a singular predicate symbol for $N$. Let $N'$ be the result of applying SPE of ${\mathsf{p}}$ to $N$. Then $N'$ is satisfiable if and only if $N$ is satisfiable.

Figures (1)

  • Figure 1: Number of solved problems per benchmark set and configuration

Theorems & Definitions (53)

  • Example 1.1
  • Example 3.1
  • Definition 4.1
  • Definition 4.2
  • Definition 4.3
  • Definition 4.4
  • Definition 4.5
  • Definition 4.6
  • Definition 4.7
  • Example 4.8
  • ...and 43 more