Definition

ein Inferenz-System I besteht aus

• Regeln (besteht aus Prämissen, Konklusion)

  Schreibweise ${\frac{{P_1, \ldots, P_n}}{{K}}}$

• Axiomen (= Regeln ohne Prämissen)

eine Ableitung für F bzgl. I ist ein Baum:

• jeder Knoten ist mit einer Formel beschriftet
• jeder Knoten (mit Vorgängern) entspricht Regel von I
• Wurzel ist mit F beschriftet

Schreibweise: I $\vdash$ F