Propositionele logica

Introductie

Logica heeft in de IT altijd al een grote rol gespeeld, maar in AI staat het logisch redeneren nog centraler. Kenmerkend voor AI-toepassingen ten opzichte van traditionele programma's is dat ze beter kunnen omgaan met onzekerheid. Waar in de traditionele automatisering onzekerheid zo veel mogelijk werd geëlimineerd, draait het er bij AI om dat, gegeven onzekerheid toch optimale beslissingen kunnen worden genomen.

Een van de bronnen van onzekerheid is dat het niet mogelijk is om een volledig beeld van de werkelijkheid te krijgen. We hebben een beperkt beeld van de werkelijkheid en die beschrijven we vaak met taal of met formules. (The language of logic) 

Het is wel mogelijk om iets nieuws van de werkelijk te ontdekken door al die zinnen slim te combineren. Met andere woorden door te redeneren.(logical reasoning). Redeneren is op basis van bepaalde uitspraken tot nieuwe inzichten komen via een aantal denkstappen.

De kunst is natuurlijk om de juiste denkstappen te nemen, anders maak je een beschrijving van de wereld die niet overeenkomt met de werkelijkheid. De propositielogica en relationele logica gaan hier over.

Een andere vraag is in hoeverre  je computers deze denkstappen kunt laten maken. Dit lijtk steeds beter te lukken. In veel AI-applicaties zie je rules-engines of theorem-provers terug. M.a.w. mechanismen die redeneren om op basis van bestaande dat iets nieuws te concluderen.

1. Syntax

Een atomaire propositie is een bewering die waar of niet waar is. Bijvoorbeeld: "2 is deelbaar", "Gerda is geweldig".

Een propositionele formule (of zin)  wordt samengesteld door het combineren van atomaire proposities en logische operatoren.

Er zijn verschillende logische operatoren:

\begin{align} \lnot&\; negatie (niet)\\ \land&\; conjunctie(en)\\ \lor&\; disjunctie(of)\\ \rightarrow&\; implicatie(als..dan)\\ \leftrightarrow&\; equivalentie (dan en slechts dan)\\ \end{align} Een voorbeeld van een propositione formule is: \begin{align} ((p \leftrightarrow r)\land (r \leftrightarrow q))\rightarrow& (p \leftrightarrow q) \end{align}
De syntax van propositielogica wordt in Backus Nauer Form als volgt gedefinieerd:

zin ::= <atomaire_propositie> | <formule>
<atomaire_propositie> := True | False | p | q | q | ... 
<formule> := $\lnot$ <formule>
| <formule> $\land$ <formule>
| <formule> $\lor$ <formule>
| <formule> $\rightarrow$ <formule>
| <formule> $\leftrightarrow$ <formule>
 
 De operatorvolgorde is haakjes, negatie, conjunctie, disjunctie, implicatie en equivalentie. Bij gelijke orde wordt er van links naar rechts gewerkt.

2. Semantiek

Een interpretatie houdt in dat aan een propositie een waarde wordt toegekend (Bijvoorbeeld: waar of niet waar, 0 of 1). Hieronder volgen twee voorbeelden van interpretaties  met drie proposities p, q, r.



Voorbeeld 1: 
\begin{align}
p^i = 1\\
q^i = 0 \\
r^i = 1\\
\end{align}
voorbeeld 2: 
\begin{align}
p^i = 0\\
q^i = 1 \\
r^i = 0\\
\end{align}

Uit de de interpretatie van de operators wordt met behulp van de interpretatie van de proposities vastgesteld. Aldus onstaat een waarheidstabel.

Het waarheidsgehalte van een formule kan worden afgeleid van de waarheidsgehaltes van de afzonderlijke atomaire proposities.

3. werken met één zin

Evaluatie is het vaststellen van het waarheidsgehalte van een samengestelde zin, gegeven een interpretatie (oftewel een truth assignment) van de propositionele constanten. Neem bijvoobeeld de zin  (p ∨ q) ∧ (¬q ∨ r) en interpretatie j:

pj = 0 qj = 1 rj = 0 (p ∨ q) ∧ (¬q ∨ r) (0 ∨ 1) ∧ (¬1 ∨ 0) 1 ∧ (¬1 ∨ 0) 1 ∧ (0 ∨ 0) 1 ∧ 0 0 Met andere woorden deze zin is niet waar gegeven de interpretatie j.

Satisfactie is het tegenovergestelde van evaluatie. We starten met een samengestelde zin en we zoeken uit of er een bepaalde of er een interpretatie is waarvoor de zin waar is. Bekijk bijvoorbeeld de zin p ∨ q ⇒ q ∧ r. We kunnen een truth table van deze zin maken voor alle combinaties van p,q,r (alle interpretaties)

De rijen met de specifieke combinatie van p,q,r in regels 2,3,4,6 leveren een onware zin op. De overige interpretaties leveren wel een ware zin op. 

Eigenschappen van zinnen
Een zin is valid (geldig) wanneer deze waar geeft bij iedere interpretatie (combinaties van toewijzingen aan de proposities). (p ∨ ¬p) is valid omdat ogeacht de waarde van p altijd 1 (waar) terug geeft.

Een zin is unsatisfiable wanneer er geen interpretatie bestaat waarvoor de zin een waar oplevert. De zin (p ∧ ¬p) is unsatisfiable.

Een zin is contingent if wanneer er interepaties bestaan die 1 terug geven (satisfied) en er zijn interpretaties die 0 teruggeven (falsifies). (p ∧ q) is contingent.

 4. Werken met twee zinnen (relaties tussen zinnen)

Zoals gezegd gaat er bij logica erom dat we verbanden leggen tussen zinnen en als we dat goed doen kunne we iets nieuws leren over de wereld. Er zijn drie type verbanden tussen logische zinnen te leggen. Om die verbanden formeel te kunnen bespreken voegen we aan de proposilogica metavariabelen toe.

Een meta-variabele (bijv: is een symbool warmee je aangeeft dat daar alle mogelijke zinnen in de propositelogica kunne worden ingevuld, mits ze maar aan de syntax voldoen.  Een zin met meta-variabelen wordt ook wel schema genoemd


entailment-relatie
Een zin φ logically entails een zin ψ (φ ⊨ ψ) dan en slechts dan iedere interpretatie waarbij φ waar is ook waar bij ψ geeft.


the sentence p logically entails the sentence (p ∨ q). Since a disjunction is true whenever one of its disjuncts is true, then (p ∨ q) must be true whenever p is true.


Deduction Theorem: A sentence φ logically entails a sentence ψ if and only if (φ ⇒ ψ) is valid. -> dus bij ieder interpretatie van beide zinnen waar geeft. (is dit zo?)





equivalentie-relatie 
Een zin φ is logically equivalent taan zin ψ dan en slechts dan iedere interpretatie waarbij  φ waar is ook  ψ waar geeft en andersom.

The sentence ¬(p ∨ q) is logically equivalent to the sentence (¬p ∧ ¬q).

Equivalence Theorem: A sentence φ and a sentence ψ are logically equivalent if and only if the sentence (φ ⇔ ψ) is valid.

De equivalentie relatie leert ons op zich niet zoveel nieuws over de wereld, maar kan worden gebruikt om moeilijk geformuleerde zinnen te vervangen door eenvoudiger zinnen. Ze geven immers dezelfde uitkomsten van waar en niet waar bij iedere mogelijk interpretatie.

consitentie-relatie

Consistency Theorem: A sentence φ is logically consistent with a sentence ψ if and only if the sentence (φ ∧ ψ) is satisfiable.

5. Bewijsvoering (Waarheidstabel, Mendelson, Fitch en regressie)

Er zijn diverse manieren om entailment en equivalentie vast te stellen. Via het gebruik van waarheidstabellen en via bewijsvoering. Bij waarheidstabellen vullen we voor beide zinnen de waarheidstabellen is en kijken of die voldoen aan de eigenschappen zoals gedefinieerd bij entailment-relatie, equivalentie relatie en of de consitence relatie.
De tabelmethode werkt maar wordt snel omslachtig omdat je om de relatie tussen twee zinnen vast te stellen alle interpretaties van deze twee zinnen moet moet uitwerken. Een alternatief is door goed te kijken naar de vorm (structuur)  van de zin (zoals zit er een implicatie in een zin, komt dezelfde propositieconstente of delen van een zin bij verschillende zinnen terug. Het interessante is dat allen op basis van deze gegevens je ook nieuwe dingen kunt afleiden over de wereld. Overigens geen nieuw idee. Aristoteles heeft al het een en ander uitgewerkt op dit gebied.

5.1 Vaststellen entailment tussen zinnen mbv waarheidstabellen

Nu een voorbeeld van een entalment-relatie tussen drie zinnen
 

5.2 Vaststellen entailment op basis van de structuur van de zinnen
Een andere manier om iets nieuws te leren over de wereld (conclusies te trekken) is door uit bestaande zinnen via bepaalde omzettingsregels te komen tot nieuwe zinnen. We werken dus niet met waarheidstabellen, maar door het toepassen van de juiste omzettingsregels kunnen we wel de juiste conclusies trekken.
   
A rule of inference (omzettingsregel) bestaat uit verschillende schema's (premisen), en ééń of meerdere aanvullende schema's (conclusies).

 Een axioma-schema is een schema zonder premisen.



5.2.1 Het Mendelsonsysteem
Het Mendelsonsysteem is een bewijssysteem dat bestaat uit één Rule of inference en drie axioma's.

5.2.2 Het Fitch systeem
Het Fitch systeem is net als het Mendelsonsysteem een bewijssysteem. Het is uitgebreid met het gebruik van aannames en subbewijzen en maakt gebruik van de volgende schema's.

5.3.3 Regressie
Een derde manier om vast te stellen of de geldigheid nieuwe zinnen kunnen worden afgeleid uit een verzameling  bestaande zinnen betreft de regressie-methode.

Om deze methode toe te kunnen passen, zijn eerst twee extra begrippen nodig. Dit betreffen:

1. Clausale vorm. Logische zinnen kunnen herschreven worden in een grammatica die clausale vorm wordt genoemd. De regessie methode werkt alleen met zinnen die volgens deze grammatica zijn opgesteld. Er is een procedure om zinnen in standaard propositiegrammatica om te zetten in clausale grammatica.
2. Er is een verschil tussen aan afleiding en een bewijs  volgens de regressie methode. Met een afleding bedoelen we hetzelfde als wat we een bewijs noemen bij bijv.. Lineaire bewijsvoering. Een regressie-bewijs betreft een afleding met een extra bewerking. Daar komen we later op terug.

Omzetten naar Clausal Form (CNF)
De grammatica van de clausale vorm wordt als volgt gedefinieerd:

 
Een atom is een uitspraak weergegeven met een symbool. (p)
Een literal is een atom of de ontkenning ervan  p of -p

Een clausal sentence is een literal of een disjunctie (of-relatie) van literalen.

If p and q are logical constants, then the following are clausal sentences.
p
¬p
¬p ∨ q
Een clause is de verzameling literals in een clausal sentence.
{p}
{q}
{p,q}

Let op. De lege clause is ook een clause. {}. Die gaan we later wanneer we het verschil tussen tussen regressie-afleiding en regressie bewijs  bespreken weer tegenkomen.

Elke formule van de klassieke propositielogica kan omgezet worden naar CNF door herhaling van de volgende stappen.

1. Elimineer ${\displaystyle \leftrightarrow }$ (bi-implicatie) met behulp van:

   ${\displaystyle P\leftrightarrow Q\equiv (P\rightarrow Q)\wedge (Q\rightarrow P)}$

2. Elimineer ${\displaystyle \rightarrow }$ (implicatie) met behulp van:

   ${\displaystyle P\rightarrow Q\equiv \neg P\vee Q}$

3. Verplaats ${\displaystyle \neg }$ (negatie) naar binnen met behulp van:

   ${\displaystyle \neg (\neg P)\equiv P}$ (elimineren van dubbele negatie)

   ${\displaystyle \neg (P\wedge Q)\equiv \neg P\vee \neg Q}$ (wetten van De Morgan)

   ${\displaystyle \neg (P\vee Q)\equiv \neg P\wedge \neg Q}$ (wetten van De Morgan)

4. Distribueer ${\displaystyle \vee }$ over ${\displaystyle \wedge }$:

   ${\displaystyle (P\wedge Q)\vee R\equiv (P\vee R)\wedge (Q\vee R)}$

voorbeeld:

	g ∧ (r ⇒ f)
I	g ∧ (¬r ∨ f)
N	g ∧ (¬r ∨ f)
D	g ∧ (¬r ∨ f)
O	{g}
	{¬r, f}

Afleiden en bewijzen volgens de regressie-methode


Resolution Principle.

{φ1, ... , χ, ... , φm}
{ψ1, ... , ¬χ, ... , ψn}
{φ1, ... , φm, ψ1, ..., ψn}

Hierboven zie je dat de toepassing van het resolutie- principe twee stappen inhoudt:

1. Samenvoegen van twee clauses
2. Het verwijderen van de clausal sentence die in de eerste clause voorkoemt en de ontkenning er van in de tweede (of andersom)

 voorbeeld:

{p, q}

{¬q, r}

{p, r}

Vaak zie je dat de samengestelde zin minder elementen bevat dan de twee originele:

{¬p, q}

{p, q}

{q}

{p, q, r}

{¬p}

{q, r}

Dit kan zelfs leiden tot een lege clausule:

{p}

{¬p}

{}

Dit betekent dat de verzameling zinnen / clauses een contradictie bevatten. Een speciaal geval betreft het volgende:

{p, q}

{¬p, ¬q}

{p, ¬p}

{q, ¬q}

We zien hier dat we op twee manieren het resoltie principe kunnen toepassen.


Afleidbaarheid (blijft er een zin over)
 Then we can derive the conclusion {r} as shown below.

1.	{¬p, r}	Premise
2.	{¬q, r}	Premise
3.	{p, q}	Premise
4.	{q, r}	1, 3
5.	{r}	2, 4

As an example, consider the clauses {p, q}, {p, ¬q}, {¬p, q}, and {¬p, ¬q}. There is no truth assignment that satisfies all four of these clauses

On the other hand, we can be sure of one thing. If a set Δ of clauses is unsatisfiable, then there is guaranteed to be a resolution derivation of the empty clause from Δ. More generally, if a set Δ of Propositional Logic sentences is unsatisfiable, then there is guaranteed to be a resolution derivation of the empty clause from the clausal form of Δ.

As an example, consider the clauses {p, q}, {p, ¬q}, {¬p, q}, and {¬p, ¬q}. There is no truth assignment that satisfies all four of these clauses.

1.	{p, q}	Premise
2.	{p, ¬q}	Premise
3.	{¬p, q}	Premise
4.	{¬p, ¬q}	Premise
5.	{p}	1, 2
6.	{¬p}	3, 4
7.	{}	5, 6

A resolution proof of a sentence φ from a set Δ of sentences is a resolution derivation of the empty clause from the clausal form of Δ ∪ {¬φ}

We have three premises - p, (p ⇒ q), and (p ⇒ q) ⇒ (q ⇒ r). Our job is to prove r.

1.	{p}	Premise
2.	{¬p, q}	Premise
3.	{p, ¬q, r}	Premise
4.	{¬q, r}	Premise
5.	{¬r}	Premise
6.	{q}	1, 2
7.	{r}	4, 6
8.	{}	5, 7