Predicate Anti-unification in (Constraint) Logic Programming
summary
Defines predicate-level most-specific generalization (MSG) for logic programs, formalizes argument/ clause mapping and a τ quality function (term-size norm) to rank generalizations, and implements a greedy matrix selection algorithm that builds two sparse matrices scoring argument and literal anti-unifications. Exact term/literal MSG is linear, but predicate-level search is combinatorial; algorithm yields an efficient approximation with backtracking on tied cells, handles recursive clauses abstractly, and produces concrete generalized predicates (variables and mappings) useful for semantic clone detection.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 2:55Why predicate anti-unification matters
- 7:17Formalizing anti-unification
- 13:00Most specific generalization
- 17:18Computing anti-unification
- 20:52Extending to goals and clauses
- 24:27Generalizing predicates
- 26:36Greedy algorithm
- 31:59Predicate generalization example
- 32:43Future directions
- 33:05Questions and discussion
related talks
01h 02mLogic, Optimization, and Constraint Programming: A Fruitful Collaboration
30mRelatively Complete Verification of Probabilistic Programs
47mLogic Programming à la Carte
27mSM-based Semantics for Answer Set Programs Containing Conditional Literals and Arithmetic
22mMechanised Semantics for Gated Static Single Assignment
18mEquivalence and Similarity Refutation for Probabilistic Programs
22mCan Logic Programming Be Liberated from Predicates and Backtracking? (Lightning talk)
19mType Inference Logics