Term (logic)

Termy jsou:

• Konstanty (0, 1, π, …)
• Proměnné (x, y, z, …)
• Funkční symboly (+, /, f, …)

Well-formed formula

Formule jsou termy a:

• Predikétové symboly (<, >, =, …) (pokud tam není nic víc, jsou to atomické formule)
• Logické spojky a pomocné symboly (∧, ∨, (), …)
• Kvantifikátory (∃, ∀)

Interpretation (logic)

Realizace definuje konstanty, funkční symboly, predikátové symboly. Ne proměnné! Dostáváme tedy něco jako „předpis“ který čeklá na dosazení za proměnné.

Když už dosadíme za proměnné, provádíme ohodnocení proměnných.

Satisfiability, Validity

Tautologie je formule platná v každé realizaci, kontradikce obdobně.

Formule je splnitelná, pokud existuje nějaká realizace a ohodnocení proměnných ve kterém je platná.

Formule je logicky platná v nějaké realizaci pokud je úplně jedno jak ohodnotím proměnné a vždy to bude pravdivé.

Formule jsou ekvivalentní pokud pro libovolné realizace (ale pro obě formule stejné) a pro libovolné ohodnocení (opět stejné pro obě formule) dávají vždy stejné výsledky.