Prolog Proof Tree for Peano Number Conversion
This animation builds the SLD resolution (proof) tree for the query ?- g(Z1,Z2) against a small Prolog program that converts successor-notation numbers like s(s(o)) into their arithmetic value. It shows unification substitutions at each step, how the fact and recursive rule are chosen, and traces the two leftmost branches plus the first three nodes of the rightmost branch. Useful for students learning SLD resolution, backtracking, and how recursive Prolog clauses model arithmetic.
Narrated · 16:9 · Preview before teaching · automatic layout checks do not establish subject accuracy
The prompt that made it
Erstelle ein Video über K24: (Prolog-Beweisbaum) Gegeben sei folgendes Prolog-Programm P: (F) g(o,0). //1. Argument oooh, 2. Argument Null (R) g(s(X),N) :- g(X,N1), N is N1+1. a) Was berechnet P? b) Zeichnen Sie den Prolog-Beweisbaum für obiges Programm und folgender Query ?- g(Z1,Z2). Führen Sie dabei mindestens die beiden am weitesten links stehenden Äste und den am weitesten rechts stehenden Ast auf. Beim am weitesten rechts stehenden Ast sind mindestens die ersten drei Knoten aufzuführen. Lösung: Darstellung. a) Die Transformation von natürlichen Zahlen in symbolischer Darstellung in arithmetische b) ?- g(Z1,Z2). (F),[Z1/o,Z2/0] (R),[Z1/s(Z3),N/Z2,X/Z3,N1/Z4] [Z1/o,Z2/0] ?- g(Z3,Z4),Z2 is Z4+1. (F) [Z3/o,Z4/0] [Z3/s(Z5),N/Z4,X/Z5,N1/Z6] ?- Z2 is 0+1. ?- g(Z5,Z6), Z4 is Z6+1, Z2 is Z4+1. [Z2/1] [Z1/s(o),Z2/1] ...
Make the next one in this series
- Show how backtracking explores alternative branches when the leftmost proof fails
- Animate the same query but for computing the predecessor using symbolic subtraction
- Compare SLD resolution trees for append/3 with multiple list solutions
