Campus Event Calendar
Event Entry
What and Who
SCL(EQ): Simple Clause Learning in First-Order Logic with Equality
Hendrik Leidinger
Max-Planck-Institut für Informatik - RG 1
Promotionskolloquium
AG 1, AG 2, INET, AG 4, AG 5, D6, SWS, RG1
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 21 May 2025
12:00
90 Minutes
E1 4
024
Saarbrücken
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 nonredundant
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 evalu-ate its performance
against state-of-the-art CC. Joint work with Yasmine Briefs integrates
Knuth-Bendix ordering into CC(X).
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 nonredundant
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 evalu-ate its performance
against state-of-the-art CC. Joint work with Yasmine Briefs integrates
Knuth-Bendix ordering into CC(X).
Contact
Jennifer Müller
+49 681 9325 2900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 05/12/2025 10:45 -- Created document.