Inferenz-Systeme (Beispiel 3)

• Grundbereich: endliche Folgen von ganzen Zahlen
• Axiome: jede konstante Folge (Bsp. [3, 3, 3, 3])
• Schlußregeln:
  • swap_k: $${\frac{{[\ldots,x_k,x_{k+1},\ldots]}}{{[\ldots,x_{k+1}+1,x_k-1,\ldots]}}}$$
  • rotate: $${\frac{{[x_1,\ldots,x_n]}}{{[x_2,\ldots,x_n,x_1]}}}$$

Aufgaben: • Ableitungen für [5, 3, 1, 3],[7, 7, 1]

• jede Folge der Form [z, 0,…, 0] ist ableitbar
• Invarianten, [5, 3, 3] ist nicht ableitbar

praktische Realisierung: http://www.siteswap.org/ und HTWK-Hochschulsport