Sequenz (FoG)

Eine Sequenz ist von der Form

Φ ⟹ ψ

wobei $Φ = {φ_{1}, \dots, φ_{n}}$ für ein $n \in N$ eine endliche Menge von prädikatenlogischen Formeln (die Beweisannahmen) darstellt und $ψ$ eine einzelne prädikatenlogische Formel (das Beweisziel) ist.

Eine Sequenz

Φ \overset{?}{⟹} ψ

repräsentiert eine Beweisverpflichtung.

Sie gilt als erfüllt, wenn das Beweisziel $ψ$ mit einer der Annahmen in $Φ$ übereinstimmt. Wir notieren dies als

Φ \overset{\sqrt}{⟹} ψ .

Eine Sequenz gilt als beweisbar, wenn aus ihr mit Hilfe von zugelassenen Beweisregeln und Beweisschritten eine Menge von ausschließlich erfüllten Sequenzen entwickelt werden kann. Wir notieren dies als

Φ \overset{!}{⟹} ψ .

Wenn wir von der Interpretation bzw. Bewertung einer Sequenz abstrahieren wollen, lassen wir ${?, \sqrt,!}$ einfach weg.

Links