ABD: Default–Exception Abduction in Finite First-Order Worlds

Abduction in knowledge representation is often framed as “explaining away” inconsistencies between a background theory and observations by hypothesizing missing facts or exceptions. Despite decades of KR work on abduction, there are few modern benchmarks that require genuine first-order relational reasoning, admit unambiguous solver-checkable verification, and produce informative error analyses rather than binary right/wrong judgments. We introduce ABD, a family of default-exception abduction tasks over small finite relational worlds. Each instance provides a set of finite structures with observed facts and a fixed default-like first-order theory that may be violated by those observations. A model must output a first-order abnormality rule α(x) that defines an exception predicate Ab(x) ↔ α(x), restoring satisfiability while keeping exceptions sparse. We formalize three observation regimes with distinct completion semantics. ABD-Full assumes closed-world observation. ABD-Partial allows unknown atoms under existential completion: α is valid if some completion makes the repaired theory satisfiable, with cost optimized in the best case. ABD-Skeptical uses universal completion: α is valid only if the repaired theory is satisfiable under every completion, with cost measured in the worst case. Because domains are finite, validity and costs are computed via SMT (Z3), enabling exact verification and controlled difficulty. We evaluate eleven frontier LLMs on 600 instances spanning all three scenarios and seven default theories. The strongest high-validity models achieve over 90% prompt validity, but prompt-set cost gaps of about 1-1.5 extra exceptions per world remain. Holdout evaluation reveals distinct generalization profiles: in ABD-Full and ABD-Partial, the dominant failure is parsimony inflation; in ABD-Skeptical, it is validity brittleness, where rules that work on prompt worlds often break on holdouts while survivors show smaller gap inflation.