Klausul (logik)
I logik är en sats en propositionsformel som bildas från en finit samling av bokstavliga (atomer eller deras negationer) och logiska bindemedel . En sats är sann antingen när minst en av bokstavssatserna som bildar den är sann (en disjunktiv sats, den vanligaste användningen av termen), eller när alla bokstavssatser som bildar den är sanna (en konjunktivsats, en mindre vanlig sats användning av termen). Det vill säga, det är en finit disjunktion eller konjunktion av bokstaver, beroende på sammanhanget. Klausuler skrivs vanligtvis enligt följande, där symbolerna är bokstavliga:
Tomma klausuler
En sats kan vara tom (definierad från en tom uppsättning bokstaver). Den tomma satsen betecknas med olika symboler som , eller . Sanningsutvärderingen av en tom disjunktiv sats är alltid . Detta motiveras genom att beakta att är det neutrala elementet i monoiden .
Sanningsutvärderingen av en tom konjunktivsats är alltid . Detta är relaterat till begreppet en tom sanning .
Implikativ form
Varje icke-tom (disjunktiv) sats är logiskt likvärdig med en implikation av ett huvud från en kropp, där huvudet är en godtycklig bokstav av satsen och kroppen är konjunktionen av negationerna av de andra bokstavliga. Det vill säga, om en sanningstilldelning gör att en sats är sann, och ingen av kroppens bokstavliga ord uppfyller satsen, måste huvudet också vara sant.
Denna ekvivalens används ofta i logisk programmering , där satser vanligtvis skrivs som en implikation i denna form. Mer allmänt kan huvudet vara en disjunktion av bokstavliga ord. Om är bokstavstexterna i en sats och är huvudet, satsen skrivs vanligtvis så här:
- Om n = 1 och m = 0, kallas satsen ett ( Prolog ) faktum.
- Om n = 1 och m > 0 kallas satsen en (Prolog)-regel.
- Om n = 0 och m > 0, kallas satsen en (Prolog) fråga.
- Om n > 1 är satsen inte längre Horn .