# Blocked Clauses in First-Order Logic

arXiv: https://arxiv.org/abs/1702.00847 · HTML: https://mlsanity.com/paper/1702.00847/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 2 Feb 2017.

## Built on by (most cited first, 1 of 1)

- [Dynamic Blocked Clause Elimination for Projected Model Counting](https://mlsanity.com/paper/2408.06199/) (2024)

## Abstract (arXiv)

Blocked clauses provide the basis for powerful reasoning techniques used in SAT, QBF, and DQBF solving. Their definition, which relies on a simple syntactic criterion, guarantees that they are both redundant and easy to find. In this paper, we lift the notion of blocked clauses to first-order logic. We introduce two types of blocked clauses, one for first-order logic with equality and the other for first-order logic without equality, and prove their redundancy. In addition, we give a polynomial algorithm for checking whether a clause is blocked. Based on our new notions of blocking, we implemented a novel first-order preprocessing tool. Our experiments showed that many first-order problems in the TPTP library contain a large number of blocked clauses. Moreover, we observed that their elimination can improve the performance of modern theorem provers, especially on satisfiable problem instances.