Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

SAT-Based Subsumption Resolution

Robin Coutelier, Laura Kovács, Michael Rawson, Jakob Rath

TL;DR

This work presents a new SAT-based reasoning technique for subsumption resolution, without requiring radical changes to the underlying saturation algorithm, and implements it in the theorem prover Vampire, and shows that it is noticeably faster than the state of the art.

Abstract

Subsumption resolution is an expensive but highly effective simplifying inference for first-order saturation theorem provers. We present a new SAT-based reasoning technique for subsumption resolution, without requiring radical changes to the underlying saturation algorithm. We implemented our work in the theorem prover Vampire, and show that it is noticeably faster than the state of the art.

SAT-Based Subsumption Resolution

TL;DR

This work presents a new SAT-based reasoning technique for subsumption resolution, without requiring radical changes to the underlying saturation algorithm, and implements it in the theorem prover Vampire, and shows that it is noticeably faster than the state of the art.

Abstract

Subsumption resolution is an expensive but highly effective simplifying inference for first-order saturation theorem provers. We present a new SAT-based reasoning technique for subsumption resolution, without requiring radical changes to the underlying saturation algorithm. We implemented our work in the theorem prover Vampire, and show that it is noticeably faster than the state of the art.
Paper Structure (9 sections, 2 equations, 1 figure)

This paper contains 9 sections, 2 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Related Work.
  3. Illustrative Examples and Main Contributions
  4. Our Contributions.
  5. Preliminaries
  6. Substitutions and matches.
  7. Saturation and redundancy.
  8. Subsumption.
  9. Subsumption resolution.

Figures (1)

  • Figure 1: Illustrative examples.