SCL(EQ): Simple clause learning in first-order logic with equality

Abstract

I propose the SCL(EQ) calculus that lifts SCL for first-order logic to first-order logic with equality. SCL(EQ) learns non-redundant clauses only. It builds a trail of annotated ground literals, representing the model assumption for non-ground input clauses. The trail includes propagations (inferred literals) and decisions (guessed literals). When a clause is false under the model assumption, SCL(EQ) derives a new non-ground clause via paramodulation. The new clause is non-redundant under a dynamic ordering, which, along with a maximum term, limits ground literals and ensures termination. I prove SCL(EQ) to be sound and refutationally complete. SCL(EQ) may use congruence closure (CC) to identify propagations and conflicts efficiently. However, exhaustive propagation of unit clauses already causes a worst case exponential blowup in ground instances. To address this, I propose CC(X), a generalization of CC with variables. It creates an explicit representation of constrained congruence classes of the whole ground input space smaller than the maximum term. I prove CC(X) sound and complete, implement it, and evaluate its performance against state-of-the-art CC. Joint work with Yasmine Briefs integrates Knuth-Bendix ordering into CC(X).

Ich schlage den SCL(EQ) Kalkül vor, der SCL für die Prädikatenlogik erster Ordnung auf die Prädikatenlogik erster Ordnung mit Gleichheit erweitert. SCL(EQ) lernt ausschließlich nicht-redundante Klauseln. Es erstellt eine Folge annotierter Grundliterale, die die Modellannahme für nicht-grund Eingangsklauseln repräsentiert. Sie umfasst Propagationen (abgeleitete Literale) und Entscheidungen (geratene Literale). Wenn eine Klausel unter der Modellannahme falsch ist, leitet SCL(EQ) eine neue nicht-grund Klausel mittels Paramodulation ab. Die neue Klausel ist nicht redundant gemäß einer dynamischen Ordnung, die zusammen mit einem maximalen Term Grundliterale begrenzt und die Terminierung sicherstellt. Ich beweise, dass SCL(EQ) korrekt und widerspruchsvollständig ist. SCL(EQ) kann zur effizienten Identifikation von Propagationen und Konflikten den Kongruenzabschluss (CC) verwenden. Die vollständige Propagation von Einheitsklauseln bewirkt bereits im schlimmsten Fall ein exponentielles Anwachsen der Grundinstanzen. Um dies zu adressieren, schlage ich CC(X) vor, eine Verallgemeinerung von CC mit Variablen. CC(X) erstellt eine explizite Repräsentation eingeschränkter Kongruenzklassen des gesamten Grundeingaberaums, die kleiner als der maximale Term ist. Ich beweise, dass CC(X) korrekt und vollständig ist, implementiere es und evaluiere seine Leistung im Vergleich zu modernen CC-Methoden. In Zusammenarbeit mit Yasmine Briefs wird die Knuth-Bendix-Ordnung in CC(X) integriert.