SCL(EQ): SCL for First-Order Logic with Equality

TL;DR

This paper introduces SCL(EQ), a new calculus for first-order logic with equality that learns only non-redundant clauses, improving inference efficiency by leveraging ground literal model assumptions.

Contribution

The paper presents SCL(EQ), a calculus combining ideas from CDCL and SCL, with a novel approach to avoiding redundant clauses in first-order logic with equality.

Findings

SCL(EQ) is sound and complete.

SCL(EQ) improves over superposition in certain cases.

The calculus effectively guides inferences using ground literal models.

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.