Definition

ein Inferenz-System I mathend000# besteht aus

• Regeln (besteht aus Prämissen, Konklusion)

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

• Axiomen (= mathend000# Regeln ohne Prämissen)

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

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

Schreibweise: I $\vdash$ F mathend000#