Linked Lists Term Logic example proved using Resolution

Problem

Formalize linked lists and show a canonical entailment using Resolution

We use the usual setup with constants, functions, and predicates for lists:

// Signature:
//   nil                         // constant for empty list
//   cons(x, xs)                 // function: attach head x to tail xs
//   append(xs, ys, zs)          // predicate: zs is xs appended to ys
//   member(x, xs)               // predicate: x occurs in xs
//
// Axioms (Horn clauses):
// A1: append(nil, ys, ys).
// A2: append(xs, ys, zs) -> append(cons(x, xs), ys, cons(x, zs)).
// M1: member(x, cons(x, xs)).
// M2: member(x, xs) -> member(x, cons(y, xs)).

Goal we’ll prove by Resolution: append(cons(a, cons(b, nil)), cons(c, nil), cons(a, cons(b, cons(c, nil)))).

Answer

Entailed. Using Resolution on (A1–A2) with the negation of the goal derives a contradiction (empty clause), so the goal follows from the axioms.

Reason Why

Resolution justification (clausal refutation)

  1. Clausify the axioms (already Horn):
    C1: append(nil, Y, Y).
    C2: ¬append(XS, Y, Z) ∨ append(cons(H, XS), Y, cons(H, Z)).
  2. Negate the ground goal G and add it as a clause: ¬append(cons(a, cons(b, nil)), cons(c, nil), cons(a, cons(b, cons(c, nil)))).
  3. Resolve backwards using C2 repeatedly to “peel” leading cons symbols, producing:
    ¬append(cons(b, nil), cons(c, nil), cons(b, cons(c, nil))), then ¬append(nil, cons(c, nil), cons(c, nil)).
  4. Resolve the last clause with C1 (unifier Y:=cons(c,nil)) to derive ⟂ (empty clause).
  5. Therefore G is entailed by A1–A2.
Check (harness) #1

Concrete append

Verify append([a,b],[c]) = [a,b,c] using a cons/nil model.

Check (harness) #2

Randomized lists (200 trials)

Generate random arrays over {a,b,c,d,e}; convert to cons-lists; check that our logical append matches JS concatenation.

Check (harness) #3

Exhaustive small lists (alphabet ≤ {a,b}, length ≤ 2)

All pairs (xs, ys); ensure append(xs, ys) = xs ++ ys.

Check (harness) #4

Membership preservation

If x is in xs or ys then x is in append(xs, ys) (using M1, M2).

Check (harness) #5

Edge cases

Test append([], ys) = ys and append(xs, []) = xs.

Check (harness) #6

Your data (CSV)

Provide L1: a,b,c and L2: d,e. We show the cons-list result and array view.

Check (harness) #7

Automated Resolution trace for the goal

Derives ⟂ from A1–A2 plus ¬G, showing the append goal is entailed.