Inferenzregel

Eine Inferenzregel, auch Regel der Folgerung genannt, ist eine syntaktische Regel in einem Beweissystem, die festlegt, wie aus bestimmten Premissen eine Folgerung abgeleitet wird. Formal wird sie oft als Schema geschrieben: Aus A1, A2, ..., An folgt B. In vielen Systemen wird eine Ableitung durch eine Folge von Anwendnungen solcher Regeln aufgebaut, wobei jede Zeile der Ableitung entweder eine Hypothese oder eine durch eine Inferenzregel hergeleitete Formel ist.

Gängige Beispiele sind Modus ponens: Aus p → q und p folgt q. Modus tollens: Aus p → q und ¬q folgt ¬p. Und-Elimination: Aus p ∧ q folgt p (und auch q). Oder-Einführung: Aus p folgt p ∨ q. In natürlichen Deduktion–Systemen gibt es üblicherweise Einführung- und Eliminierungsregeln, z. B. ∧-E, ∨-I, →-I, sowie Quantorregeln wie ∀-I und ∃-I. In Hilbert-Systemen dominieren axiomatische Schemata, während der Schluss mit Modus Ponens erfolgt; dort dienen Inferenzregeln als einzige Methode, aus bereits bewiesenen Formeln neue abzuleiten.

Eigenschaften solcher Regeln umfassen Soundness (Korrektheit): Aus wahren Premissen folgt in der Regel auch die Folgerung, d. h. nur wahre Schlüsse können gezogen werden. Completeness (Vollständigkeit) beschreibt, dass alle semantisch gültigen Folgerungen durch eine Folge von Inferenzregeln ableitbar sind. Inferenzregeln bilden die Grundlage formaler Logik, der Beweistheorie, der automatisierten Theorembeweisung, logischer Programmierung, formalen Verifikationsmethoden und typbasierter Programmierparadigmen.