Kapitel 1

Aussagenlogik

1.1 ”Wahr“ und ”Falsch“

Wir werdenim FolgendenlogischeOperationenals VerknupfungenelementarerAussageneinfuhren.Hierzubenotigenwir zunachstzweiZeichen,diedieRolledesumgangssprachlichen

”Wahr“ und

”Falsch“

ubernehmen.Wir konnendieseeinfachWahr undFalschnennen,oderauch1 und0 oderauchA undBoderauchquimm undschnurz. Wichtig ist nur, dasswir zwei klar unterscheidbareSymboleeinfuhren.Der Einfachheithalberhaltenwir unsan die Konventionenund nennendieseZeichen1 und 0; wobeider1 dieRolledesumgangssprachlichen

”Wahr“ undder0 dieRolledesumgangssprachlichen

”Falsch“

zukommenwird.

Bei allen folgendenAusfuhrungensollte unsaberbewusstsein,dassdie Wahl der konkretenZeichenbeliebig ist, solangedie darausentstehendeSprachein sich konsistentund stimmig ist. In der Logikwerdenwir zunachstversuchen,durchrein formaleDefinitionenumgangssprachlicheBedeutungenzumodellieren.

Die Zeichen0 und1 bezeichnenwir auchalsWahrheitswerte.

1.2 LogischeOperatoren

Wir beginnenzunachstmit einerDefinition der logischenGrundoperationenund, oder und nicht. Wirwerdendiesezunachstalsein- bzw. zweistelligeOperatorendefinieren,welche(Paarevon) Wertenaus�0 � 1 � wiederauf

�0 � 1� abbilden.Wir vernachlassigendabeizunachstbewusstdie Unterschiedezwi-

schenSyntax(der formalenSchreibweise)undSemantik(derBedeutung).Fur jedendieserOperatorengebenwir dasFormelzeichenundeineAuswertungstablelle(Wahrheitstafel) an.Diesegibt an,wie wel-cherAusgangswertdenjeweiligenEingangskombinationenzugeordnetist.

1.2.1 Das”und“

Und: ZweistelligerOperator:” � “

A B A � B0 0 00 1 01 0 01 1 1

9

Daszweistellige� modellierthierbeidieumgangssprachlicheBedeutungdesWortes”und“ . DieAussage

A � B ist nurdannwahr, wennbeideTeilaussagenA undB wahrsind.

1.2.2 Das”oder“

Oder: ZweistelligerOperator:” � “

A B A � B0 0 00 1 11 0 11 1 1

Daszweistellige � modellierthierbeidie umgangssprachlicheBedeutungdesWortes”oder“ . Die Aus-

sageA � B ist dannwahr, wennmindestenseinederTeilaussagenA undB wahrist. Vorsicht: Man darfdas � nicht mit demumganssprachlichen

”entweder����� oder“ verwechseln,welchesnur wahr ist wenn

genaueinederTeilaussagenwahrist.

1.2.3 Das”nicht“

Nicht: EinstelligerOperator:” � “

A � A0 11 0

Daseinstellige� modellierthierbeidieUmgangssprachlicheBedeutungdesWortes”nicht“ . DieAussage� A nimmt immergenaudenentgegengesetztenZustandvon A ein.

1.3 Syntax

In derLogik ist (wiewir baldfeststellenwerden)dasstrengeAuseinanderhaltenvonSyntaxundSemantikeinerFormelvon entscheidenderBedeutung.

Die Syntaxbeschreibtlediglich, auswelcherZeichenfolgeeineFormelzusammengesetztist. Insbeson-deresprichtmanvon einersyntaktisch korrektenFormel, soferndie ZeichenfolgegewissenRegelnge-horcht.

Die SemantikeinerFormelspiegelt dagegenderen”Sinngehalt“ oder

”Bedeutung“ wider. In derAussa-

genlogikkannmansichdie Semantikalsdie zu einerFormelzugehorigeWahrheitstafelvorstellen.

Definition 1.3.1(Syntax der Aussagenlogik)Syntaktisch korrekteFormeln uber einer Menge � vonatomarenFormeln � : � A � B � C �������� A1 � A2 ��������� sinddurch folgendevier Regeln beschrieben:

(i) die atomarenFormelnaus � selbstsindsyntaktisch korrekt,

(ii) sind f undg syntaktisch korrekt,sosindauch � f � g und � f � g syntaktisch korrekt,

(iii) ist f syntaktisch korrekt,soist auch � � f syntaktisch korrekt,

10

(iv) ausschliesslich Formelndie nach einer der Regeln (i)–(iii) syntaktisch korrekt sind,sind syntak-tisch korrekt.

Auf denerstenBlick wirkt dieseDefinition von aussagelogischenFormelnetwasaufgesetztfur etwas,waseinemgut vertrautist. Warummussetwassokompliziert erklart werden,wennesdoch

”klar“ ist?

EinesolcheFormalisierunghatjedochmehrereVorteile:Zumeinenkonnenwir unsdadurcheinigen,wasdennnun

”genaugemeint“ ist. Zum anderenkonnenaufBasisdieserDefinitionAussagenuberFormeln

gemachtundbewiesenwerdenodergenauangegebenwerden,wie ihnenWertezugewiesenwerden(wiewir im Folgendensehenwerden).Im ubrigenentsprichtdie Definition auchdem,waswir intuitiv tun,wennwir eineFormelkorrektaufschreiben.

Beispiel1.3.2 ����� A � B � � � C � � � A � B � ist eineSyntaktisch korrekteFormel.Mankanndieswiefolgteinsehen:A, B undC sindnach Regel (i) syntaktisch korrekt,da sieatomare Formelnsind.Nach Regel(iii) ist � � C syntaktisch korrekt.Nach Regel � ii (unddersyntaktischenKorrektheitdervorherigenAus-drucke) sind � A � B und � A � B syntaktisch korrekt.Nach Regel � ii (unddersyntaktischenKorrektheitder vorherigenAusdrucke) ist auch ��� A � B � � � C � syntaktisch korrekt.Schliesslich ist nach Regel � ii (undallembisherGesagten) ����� A � B � � � C � � � A � B � einsyntaktisch korrekterAusdruck.

Nun ist es nicht die (einzige)Aufgabeder Logik, solchelangweiligenSchlussketten formal durch-zufuhren.Man solltesichaberdennochvergegenwartigen,dassgeradedurchdieseshochformelleVor-gehensicheinsolcher

”Syntaxcheck“ komplettautomatisierenlasstundvon einemComputerausfuhren

lasst.Vergleichbarespassiertz.B. in dererstenPhasebeimCompiliereneinesProgrammes,wenndieseszunachstauf syntaktischeKorrektheitgepruft wird.

AusderDefinitionderFormelsyntaxergibt sicheinenaturlicheArt, denAufbaueinerFormelalsbaumar-tigesDiagrammdarzustellen.Dafur schreibtmanunterdenverknupfendenOperatordieTeilformeln(unddiesewiederaufdie gleicheebenbeschriebeneArt undWeise).

Fur dasBeispielergibt sichdieDarstellungalssogenannterAbleitungsbaum:

PSfragreplacements

A

A

B

B C

���

�

�� � C ��

A�

B����

A�

B� � � � C ��� �A�

B�

Abbildung1.1:Ableitungsbaum

Zwei FormelnF und G nennenwir syntaktisch gleich, wennsie ausdenselbenZeichenin der selbenReihenfolgeaufgebautsind,wennsiealsowortwortlich gleichsind.Wir schreibendannF G.

Syntaxheisstalsokurz:Wasist eineFormel.

11

1.4 Semantik

Durchsukzessive Anwendungderin Abschnitt1.2angegebenenWahrheitstafelnkonnenwir dieFormelausdemletztenBeispielfur einebeliebigeBelegungderVariablen( atomarenTeilformeln)A, B undCauswerten.Wir konnenzurAuswertungauchdirektdenAbleitungsbaumzuHilfe nehmen.Nachdemwirdie Blattermit Wahrheitswertenbelegt haben,konnenwir nacheinanderdeneinzelnenKnotenebenfallsWahrheitswerte(gemassderWahrheitstafelnfur und, oder, nicht) zuordnen.Insbesondereergibt sichfurA 1, B 0 undC 0, dasssichdie FormelausunseremBeispielzu1 auswertet(SieheAbb. 1.2).

PSfragreplacements

1

1

0

0 0

���

�

� 10

1 1

1

Abbildung1.2:EineAuswertung

EineAuswertungderFormelfur alleachtverschiedenenEingangsbelegungenergibt die folgendeWahr-heitstabelle

A B C ����� A � B � � � C � � � A � B � 0 0 0 00 0 1 00 1 0 10 1 1 01 0 0 11 0 1 01 1 0 11 1 1 1

Die Wahrheitstabelledruckt den inhaltlichenGehalteinerFormel aus.Wir werdengleich denBegriffder Semantiknochscharfer fassen.Fur jetzt konnenwir ihn mit der Aufstellungder Wahrheitstabellegleichsetzen.DieSemantikeinerFormelist das,wasmanerhalt,wennmandieFormelfur allemoglichenEingangsbelegungenauswertet.

Semantikheisstalsokurz:WasbedeuteteineFormel.

12

1.5 SemantischeAquivalenz

ZweiFormelnkonnenunterschiedlichaussehenunddennochdiegleicheBedeutung( Semantik)haben.

Beispiel1.5.1 Fur die Formel � � A � � � B ergibt sich derenSemantikausfolgenderWahrheitstabelle.

A B � A � B � � A � � � B 0 0 1 1 10 1 1 0 11 0 0 1 11 1 0 0 0

Fur die Formel � � A � B ergibt sich derenSemantikausfolgenderWahrheitstabelle.

A B A � B � � A � B 0 0 0 10 1 0 11 0 0 11 1 1 0

Die Auswertungderbeiden(syntaktisch verschiedenen)Formelnfuhrt zumgleichenErgebnis.

BeideebengezeigtenBeispielehabendie gleicheWahrheitstabelle,obwohl sie eineunterschiedlicheSyntaxhaben.SolcheFormeln nenntman auchsemantisch aquivalent. Sind zwei Formeln F und Gsemantischaquivalent,soschreibenwir F � G.

1.6 ”Wenn ����� dann“

Wir wollen nun sehen,wie sich eine Aussageder Form”Wenn A dannB“ in unserbisherigesSy-

stemeinfugenlasst.Wir fuhrenhierfur die Schreibweise� A � B ein. Dies ist allerdingslediglich eineAbkurzungfur: � A � B : ��� � A � B DieseDefinition lasstsichsobegrunden:

WennA dannB� WennA eintritt, danntritt auchB ein� A tritt nichtein oder(A tritt ein undB tritt ein)� A tritt nichtein oderB tritt ein� (nichtA) oderB

Wir wollen unsdieseetwasunanschaulicheAquivalenzvon A � B und ��� � A � B nochmalsaneinemBeispiel vergegenwartigen.Betrachtenwir denSatz

”Wennes regnetwerdendie Strassennass“ . Wir

konnenihn in die zwei Teilaussagen

A: Esregnet.

B: Die Strassenwerdennass.

13

zerlegen.Was ist nun daslogischeGegenteil diesesSatzes?Die Folgerung”Wennes regnet,werden

die Strassennass“ kanndurchdie AngabeeinesGegenbeispielswiderlegt werden.Die ExistenzeinessolchenGegenbeispielsubernimmtsomitdie Rolle deslogischenGegenteils.Wie siehtnunein solchesGegenbeispielaus?

”Esmussregnen,unddieStrassensindnichtnass“ . Also in FormelnA � � � B . Somit

mussgelten: � A � B ���� � � A � � � B � � �Die letzenFormellasstsichaberwie folgt umrechnen:� � A � � � B � ���� � A � � � � � B � ���� � A � B �� A � B Dieswargenaudie AussageunsererDefinition.

1.7 Tautologien

Als Tautologien bezeichnetman Aussagen,die unabhangig von der Belegung der atomarenFormelnimmerwahrsind.EineeinfacheTautologieist z.B. � B � � B , wie mansichleicht mit Hilfe einerWahr-heitstabelleklar machenkann.

Beispiel1.7.1 Aussage:”Wennder Hahnkraht auf demMist, verandertsich dasWetter, oderesbleibt

wieesist.“ Zerlegenwir denSatzin atomare Aussagen,erhaltenwir

A : Hahnkraht aufdemMist

B : Wetterandertsich� � B : Wetterbleibt

Als Formelsiehtdie Aussage folgendermassenaus:

A ��� B � � � B � ��� � A � � B � � � B � � � ��� � A � 1 � 1

Der Satzist alsoeineTautologie.

14

1.8 UnterschiedzwischenSyntaxund Semantik

Die Symbole� � � und � habeneine”Doppelrolle“ , diesichausihrerBedeutungin SyntaxundSemantik

ergibt. Zur besserenUnterscheidungbenutzenwir temporarzweiverschiedeneZeichensatze � , � , � und� � �� , � � �� , � � � �� � � � fur die syntaktischebzw. fur die semantischeEbene.Die RollenderbeidenEbenenlassensichgrobfolgendermassenumreissen:

1. Syntax: Als”Zeichen“ in einemsyntaktischkorrektenAusdruck,z.B. in ����� � A � B � C .

Die syntaktischeKorrektheiteiner solchenFormel lasstsich allein durch das in Abschnitt 1.3angegebeneVerfahrentesten.Die konkreteBedeutungderZeichenist dabei(abgesehenvonderenStelligkeit) unerheblich.

2. Semantik: Als zweistelligeOperatoren� � � �� � � � �� bzw. einstelligeOperatoren� � � � �� � � � auf denWerten�0 � 1 � .

x y x � � � � y0 0 00 1 01 0 01 1 1

x y x � � � � y0 0 00 1 11 0 11 1 1

x � � � �� � � � x0 11 0

Die Wahrheitstafelngebenan,wie die ZeichenalsOperatorenausgewertetwerdensollen.

Durch eine Kette von Definitionenwollen wir nun eine formale Definition desBegriffes”Semantik“

erarbeiten.Wennwir in folgendenvon”Formel“ sprechen,setztenwir immer stillschweigendvoraus,

dassdie Formelsyntaktischkorrektist.

Definition 1.8.1(Mengevon atomaren Teilformeln passtzu Formel) Fur eineFormel F sei � F dieMenge aller atomaren TeilformelnvonF. EineMenge � vonatomaren Formelnpasstzu einerFormelF, wenn � F � � gilt.

Mit anderenWortenpasstdie Menge � zu F , wennsie mindestensalle atomarenTeilformeln von Fenthalt.

Definition 1.8.2(Semantik der Aussagenlogik)Sei � eineMenge vonatomarenFormelnund �! seidieMenge aller Formelnuber � .

Seinun " : �#� �0 � 1 � eineBelegungder atomarenTeilformelnmit Wahrheitswerten.(" ist alsoeine

Funktion,die jederatomarenFormelaus � denWert 0 oder1 zuweist.)

Wir betrachtennuneineFortsetzung$" : � D � �0 � 1 � von " , die jeder Formel uber � einenWert aus�

0 � 1 � zuordnet.Wir definieren $" wie folgt:

$"%� A : "&� A fur alle atomarenTeilformelnA '("$"&� F � G : )1 falls $"&� F � 1 und $"&� G � 10 sonst$"&� F � G : )1 falls $"&� F � 1 oder $"&� G � 10 sonst$"&� � F : )1 falls $"&� F � 00 sonst

15

Die zugegebenermassenaufdenerstenBlick etwasumstandlicherscheinendeDefinitionvon $" formali-siertdasAuswerteneinerFormelnachdemWahrheitswertefur derenatomareTeilformelngegebensind.JedeBelegung " : �#� �

0 � 1 � entsprichtdabeieinerkonkretenZuordungvon Wahrheitswerten.$"&� F ergibt danngenaudie Auswertungder Formel unter dieserBelegung.Man beachte,dasses zu einergegebenenMenge � von n atomarenTeilformeninsgesamt2n verschiedeneBelegungen" gibt. Dieseentsprechenim PrinzipdeneinzelnenZeilenderWahrheitstafeln.

Bemerkung1.8.3* Da essich perDefinitionbei $" umeineFortsetzungvon " handelt,schreibenwir derEinfachheithalberim folgendenstatt $" auch " .* Wir ubertragen den Begriff, dasseine eine Menge von atomaren Teilformenzu F

”passt“ auf

Belegungen.Wir sagen,dasseineBelegung " : ��� �0 � 1 � zueinerFormelF

”passt“ , falls � F �� .

Wir konnendie in 1.8.2 gegebenenAuswertungsregeln unter Verwendungder DoppelbedeutungderZeichen� � � und � auchfolgendermassenausdrucken:

Der Belegungsoperator" hat vier Eigenschaften:* EineBelegung " ordnetatomarenFormeln � A � B � C �������+ konkreteWahrheitswertezu,* "&� x � y ,-"&� x � � � � "&� y ,* "&� x � y ,-"&� x � � � � "&� y ,* "&� � x , � � � �� � � � "&� x .”Eselsbrucke“ : DerBelegungsoperator" stehteigentlichfur

”Auswertung“ .

Beispiel1.8.4 Der Belegungsoperator " kann mittelsden obengenanntenEigenschaftenin Formelnhereingezogen werden.Habenwir zumBeispiel "&� A . 0 ��"%� B / 1 ��"&� C / 1 undwollendie Formel��� � A � B � C auswerten,ergibt sich:"%����� � A � B � C � "&��� � A � B � � � � "&� C �0"&� � A � � � � "&� B � � � � � "&� C ��� � � � �� � � � "&� A � � � � � "&� B � � � � � "&� C ��� � � � �� � � � 0 � � � � 1 � � � � 1 � 1 � � � � 1 � � � � 1 1 � � � � 1 1

Die obigeDefinitioneinerkonkretenAuswertungermoglichtesunsnunzusagen,waswir unterseman-tischaquivalentenFormelnverstehenwollen.

Definition 1.8.5(Semantischaquivalent) ZweiFormelnF undG heissensemantischaquivalent, wennfur alle Belegungen " : �1� �

0 � 1 � (diezuF undG passen)gilt: "&� F ,2"%� G .Wir schreibendann:F � G.

16

Bemerkung1.8.6 Umgangssprachlich heisstF � G: BeimEinsetzenkommtimmerdasGleiche raus.Verknupft mandieseDefinition mit der Interpretationaus1.8.2,erklart sich jetzt auch: Zwei Formelnsindsemantisch aquivalent,wennsiedie gleichenWahrheitstafelnhaben.

Beispiel1.8.7 Die FormelnF #� � A � � � B und G � � A � B sind semantisch aquivalentwie manausderWahrheitstafelunschwerentnehmenkann.

A B F G0 0 1 10 1 0 01 0 0 01 1 0 0

Lagen die beidenFormel realisiert als (ideale) logische Schaltkreisevor, so gabeesvon aussenkeineMoglichkeit siezuunterscheiden.

PSfragreplacements

A AB B

F G

Abbildung1.3:F undG sindsemantischaquivalent

Beispiel1.8.8 Auch die beidenFormeln F A � � B � � � B � und G A sind semantisch aquivalent,obwohldie FromelG weniger atomare Teilformelnhat als F. Wir konnenunseinfach vorstellen,dassder

”Eingang“ B in G zwarexistentist, abervonG nicht weiterverwendetwird. Auch hier gilt wieder,

dasssich denFormelnentsprechendelogischeSchaltkreisevonaussennicht unterscheidenliessen.

PSfragreplacements

A AB B

F G

Abbildung1.4:F undG sindsemantischaquivalent

17

1.9 SemantischaquivalenteFormeln

Der Begriff dersemantischenAquivalenzermoglicht esnunmit Formelnzu”rechnen“ . Rechnenheisst

hier, dassbestimmteAusdrucke durchsemantischaquivalenteAusdrucke ersetztwerdendurfen. WirgebenzunachsteineListe von semantischaquivalentenFormeln,die letztlich die Rechenregenmit logi-schenOperationenwiderspiegeln:

Idempotenz: � F � F �� F � F � F �� FKommutativitat: � F � G ���� G � F � F � G 3��� G � F

Assoziativitat: ��� F � G � H 4��� F � � G � H � ��� F � G � H 4��� F � � G � H � Absorption: � F � � F � G � 3� F � F � � F � G � 3� F

Distributivitat: � F � � G � H � 5����� F � G � � F � H � � F � � G � H � 4����� F � G � � F � H � De MorganscheRegeln: � � � F � G � ������ � F � � � G � � � � F � G � ������ � F � � � G �

DoppelteNegation: � � � � F � ,� F

Manbeachte,dassesfur jedederRegeln(bisaufdie letzte)zweiVariantengibt, dievollkommensymm-terischin � und � sind.Man kannjedeeinzelneRegel leicht mit Hilfe einerWahrheitstafelnachprufen.Nun nocheineListe von Regelnwelchedirekt mit

”0“ und

”1“ in Verbindungstehen.Formalhabenwir

auf der syntaktischenEbenediesebeidenZeichenzunachst(noch)nicht eingefuhrt. Dies machtabernichts,dawir sieeinfachalsAbkurzungenfur folgendeFormeln

”definieren“ konnen:

1 �� A � � � A � 0 �� A � � � A � DerAusdruckin dererstenFormelist immerwahr( 1). DerAusdruckin derzweitenFormelist immerfalsch( 0). Wir erhaltensoz.B. nochweitereRegeln:� A � 1 3� 1 � A � 0 �� 0� A � 0 3� A � A � 1 �� A� A � 1 ,� 1 � 0 � A �� 1

Um mit formalerSicherheitauchtatsachlichErsetzungendurchfuhrenzu konnen,benotigenwir nochfolgendenSatz:

Satz1.9.1 (Schoning, S.24) SeiF � G, und F Teilformel von H. Dann gilt H � H 6 , wobeiH 6 ausHhervorgeht,wennirgendeinVorkommenvonF durch G ersetztwird.

Der Beweis diesesSatzeserfolgt letztlich durchInduktion uberdie Langeder Formeln.Man findet inz.B. im Schoning.

1.10 Weglassenvon Klammern

Bisherhabenwir versucht,gemassunsererRegelnfur syntaktischkorrekteFormelnmit Klammerungensehrstrengumzugehen.Leider beschehrtunsdiessehrviel unnotige Schreibarbeit.Wir wollen dieseumgehen,indemwir (ahnichwie beimRechnenmit Zahlen)ein paarvereinfachendeRegelneinfuhren.DiesewerdenzumTeil durchdie im letztenAbschnittangegebenenAquivalenzengerechtfertigt.

1.10.1 Weglassenausserer Klammern

Die auserstenKlammerneinerFormelkonnenohneMissverstandnisseweggelassenwerden.Wir schrei-benalsoz.B. � A � B � C statt ��� A � B � C .

18

1.10.2 Weglassenvon Klammern bei Folgenvon 7 oder 8BestehteineFormel auseinerHintereinanderausfuhrung vieler und-Operationen,so sagtunsdasAs-soziativgesetz,dassesfur semantischeAquivalenzauf die ReihenfolgederAuswertung(Klammerung)nichtankommt.Esgilt z.B.� A � B � � C � D ������ A � B � C � D ��� A � � B � � C � D � �Wir lassendannkurzerhandeinfachalle innerenKlammernbeieinemsolchenAusdruckweg undschrei-beneinfach

A � B � C � D �Dasselbemachenwir auch,wennin einerFormelausschliesslichoder-Operatorenvorkommen.

Vorsicht: Die Regel ist nicht anwendbar, wennin einerFormel � und � gemischtvorkommen.

1.10.3 Priorit atsregeln

Weiterhinfuhrenwir nochRegelnein,die AuswertungsprioritatenderOperatorenangeben.

’ � ’ bindetstarker als’ � ’ und’ � ’,’ � ’ und’ � ’ bindetstarker als’ � ’.

Somitkonnenwir anstatt’ ��� A � B � � � C � 5�9� A � B ’ einfach’ � A � B � � C � A � B’ schreiben.

1.11 Der Aquivalenzoperator

Wir fuhrennunnocheinenweiterenOperator’ : ’ ein.Die”Bedeutung“ desOperatorsist

”A ist aquiva-

lentzuB“ . Genausowie schonbeimOperator’ � ’ konnenwir denAquivalenzoperatorausdenelemen-tarenGrundoperationen� . � , � zusammensetzen.Wir definieren

A : B : � A � B � � � A � � B �Die WahrheitstafeldiesesOperatorsist:

A B A : B0 0 10 1 01 0 01 1 1

Der Operatorwertetalsoimmerdannzu 1 aus,wennbeideEingangeidentischsind.Der folgendeSatzverknupft denBegriff dersemantischenAquivalenzmit demAquivalenzoperator (Ein Beweisstehtz.B.im Schoning).

Satz1.11.1 F � G, genaudannwenn � F : G �� 1

Beispiel1.11.2 Wir wissenbereits,dassdieFormeln � � A � B und � A � � B semantisch aquivalentsind.UnterAnwendungdesobigenSatzeslasstsich diesauch ohneWahrheitstafel,reindurch Rechnen,uber-prufen.Wir mussennachweisen,dass ��� � � A � B � � � � A � � B � � ��� �;� � A � B � � � � � A � � B � eineTautologie ist.

19

Wir rechnen ��� � � A � B � � � � A � � B � � ��� �!� � A � B � � � � � A � � B � � ��� � A � � B � � � A � � B � � ��� A � B � � A � B � � � � A � � B � � A � B � � � A � B � � A � B � 1

(Zugegebenermassen,ist die Wahrheitstafelmethodeeinfacher, aberderSatzwird unsspaternochvonNutzensein.)

1.12 Normalformen

Zunachstfuhrenwir wiedereineabkurzendeSchreibweiseein. Vergleichbarmit demSummationsope-rator∑ in derArithmetik erlaubenwir es,mehrere� oder � Operatorenzusammenzufassen:

F1 � F2 � F3 � ����� � Fk k<i = 1

Fi

F1 � F2 � F3 � ����� � Fk k>i = 1

Fi

Definition 1.12.1(Literal) Ein Literal ist eineatomare Formelodereinenegierteatomare Formel.

Definition 1.12.2(Konjunkti veNormalform) Eine Formel F ist in Konjunktiver Normalform (kurzKNF), wennsiedieGestalt

F @? k<i = 1

? mi>j = 1

Li A j BCBmit LiteralenLi A j hat.

Definition 1.12.3(Disjunkti ve Normalform) EineFormelF ist in DisjunktiverNormalform(kurzDNF),wennsiedie Gestalt

F @? k>i = 1

? mi<j = 1

Li A j BCBmit LiteralenLi A j hat.

EineKNF entstehtalsoausderund-VerknupfungmehrererTerme,dienuroder-OperatorenundLiteraleenthalten.AnalogentstehteineDNF ausderoder-VerknupfungmehrererTerme,dienurund-OperatorenundLiteraleenthalten.Die einzelnenTermediehierbeiverknupft werdennenntmanauchKlauseln.

NebenihremstrukturellsehreinfachenAufbau,ist dasbemerkenswerteandiesenNormalformen,dasseszu jederFormeleinesemantischaquivalenteDarstellungalsDNF (bzw. KNF) gibt. Allerdingsist dieseDarstellungim Allgemeinennicht eindeutig.Durch sukzessivesAnwendender DistributivgesetzeundderDe Morgan’schenRegelnlasstsichjedeFormeldurchRechnenin eineDNF bzw. KNF umwandeln.Es gibt allerdingsaucheineeinfacheMethodewie maneineDNF quasidirekt ausder Wahrheitstafelablesenkann.Wir machenunsdasVerfahrenaneinemBeispielklar.

20

Beispiel1.12.4 Betrachenwir eineFormelF mit der folgendenWahrheitstafel:

A B C F0 0 0 00 0 1 00 1 0 10 1 1 11 0 0 11 0 1 11 1 0 01 1 1 1

Fur eineDNF betrachtenwir alle Zeilender Wahrheitstafel,in denenF denWert 1 hat undschreibendieseZeilenals

”und“ –Klausel.Hat dabeieineatomare Formel in der Zeile denWert 1, wird sie als

Literal Li A j A ubernommen,hatsiedenWert 0 wird siealsLiteral Li A j � A ubernommen.EinesolcheKlauselist eineFormel,die genaunur an der betrachtetenZeilezu ’1’ evaluiert undansonstenein ’0’ergibt. Alle soerhaltenenFormelnwerdenmit

”oder“ verknupft.

Fur dasBeispielergibt sich (ausder3., 4.,5., 6. und8. ZeilederTabelle):� � A � B � � C � � � A � B � C � � A � � B � � C � � A � � B � C � � A � B � C Wir konnenauch eineKNF direkt ausder Wahrheitstafelablesen,indemwir alle 0–Zeilenbetrachtenunddiesmaleineatomare FormelA mit demEintrag 1 als Literal Li A j � A undbei einemEintrag 0 alsLiteral Li A j A ubernehmen.DieseLiterale werdenmit

”oder“ verknupft unddie einzelnenZeilenmit

”und“ .

Fur dasBeispielergibt sich (ausder1., 2. und7. ZeilederTabelle):� A � B � C � � A � B � � C � � � A � � B � C Sowohldie DNF als auch die KNF sindsemantisch aquivalentzuF.

Ein wenigVorsichtist geboten.NachunsererDefinitionist dieDNF (bzw. KNF) einerFormelwie gesagtkeineswegs eindeutig.So hat z.B. die Formel F ausdemletztenBeispielauchnochfolgendekurzereDNF (wie manunschwernachpruft): � � A � B � � A � � B � � A � B � C Die erstenbeidenZeilendieserDNF fassenpraktischimmerzweiZeilenunserer

”Langfassung“ zusam-

men.

21

1.13 Modell, Erf ullbark eit, Tautologie

Nunmehrwerdenwir denBegriff desModellseinerFormel kennenlernen.Obwohl dieserBegriff (zu-mindestwasdie Aussagenlogikbetrifft) in seinerDefinitionsehreinfachist, spieltereinezentraleRollein derLogik. Zunachsterinnernwir uns,dasseszueinerFormelF mit n atomarenTeilformelninsgesamt2n verschiedenedazupassendeBelegungsoperatoren" gab— fur jedeZeile derWahrheitstabelleeine.WertetdieFormelF fur einebestimmtenBelegungsoperator" aus,soerhalt manentwedereine’1’ odereine’0’. Im Falleeiner "&� F , 1 nenntman " ein Modell von F. Ist " Modell von F, soschreibenwirauchabkurzend"ED F. Der Begriff desModellesgestattedunsnun einigenutzlicheweitereBegriffeeinzufuhren,die esunserleichternuberFormelnzu

”reden“ .

Definition 1.13.1(Erf ullbark eit, Tautologie)* F ist erfullbar , falls esein " gibt mit "FD F.* F ist”Tautologie“ , wennfur jedes" gilt: "GD F.

(Wir schreibendann D F.)* F ist unerfullbar , falls eskein " gibt mit "GD F.

Eine Formel ist also erfullbar, wenn ihre Wahrheitstabellein der letztenSpaltemindestenseine ’1’enthalt. Hat die letzte Spaltenur Einsen(d.h. die Formel ist unabhangig von der Belegung wahr) soist sieTautologie. Hat die letzteSpaltenur Nullen so ist sieunerfullbar. (Auf eineretwaswenigerfor-malenEbenehattenwir denBegriff derTautologiebereitseingefuhrt.) Auch derBegriff der logischenFolgerunglasstsichmit demModellbegriff elegantformulieren.

Definition 1.13.2(Folgerung) G ist FolgerungvonF1 � F2 ������� Fk wennfur alle " mit"FD F1 ��"FD F2 �������H��"GD Fk

auch "GD G gilt.

DieseDefinition desBegriffes Folgerung fasstgenauunsererumgangssprachlichesVerstandnisdiesesWortes.Nehmenwir anF1 � F2 ������� Fk seienirgendwelcheAussagenundG seieineFolgerungausihnen,dannbedeutetdas:

”wennimmer fur eineBelegung " alle Fi erfullt sind,dannist auchG erfullt“ . In

dieserDefinition desFolgerungsbegriffes liegt letztlich auchdie RechtfertigungderDefinition unseres’ � ’-Operators.Dieswird durchdenfolgendenSatzdeutlich.

Satz1.13.3 G ist FolgerungvonF1 ������� Fk g.d.w. die Formel � F1 � ����� � Fk ,� G eineTautologie ist.

Beweis: Wir habendie AquivalenzderfolgendenbeidenAussagenzu zeigen:

(1) Fur alle " mit "%� F1 �������I"&� Fk � 1 gilt "&� G , 1.

(2) Fur alle " gilt "%��� F1 � ����� � Fk �� G � 1

Wir benutzendenfolgendenZusammenhang:"&��� F1 � ����� � Fk �� G �����0"&� F1 � � � � ����� � � � � "&� Fk � J���� ���� "&� G � 22

Essindzwei Richtungenzu zeigen.(1) � (2): Sei " beliebig.Entwedergilt "&� F1 JK�����LM"&� Fk J 1undsomitnach(1) auch"&� G , 1. Dannist ���0"&� F1 � � � � ����� � � � � "&� Fk � ����� ���� "&� G � �K��� 1 � ����� � 1 J� 1 � 1.Andernfallsgibt eseinFi mit "%� Fi 3 0. Dannist ���0"&� F1 � � � � ����� � � � � "&� Fk � 3�E"&� G � 3N��� 0 ����� ���� "&� G � � 1.

(2) � (1): Sei " sodass"&� F1 5 1 �������O��"&� Fk 5 1. (2) impliziert ���0"&� F1 � � � � ����� � � � � "&� Fk � b �P"%� G � 5 1.Einsetzenergibt ��� 1 � � � � ����� � � � � 1 3���� ���� "&� G � , 1. Undsomit � 1 �Q"%� G � , 1. Also "&� G � 1.

1.14 DasErf ullbark eitsproblem

Wir wollennundieEntscheidung,obeinegegebeneFormelF erfullbar ist, alsalgorithmischesProblemauffassen.In der Tat handeltessich dabeium einesehrfundamentaleFragestellung,da sich,wie wirgleichsehenwerden,viele (auchpraxisrelavante)algorithmischeProblemedaraufzuruckfuhrenlassen.

Durch unserestrengeTrennungvon Syntaxund Semantikkonnenwir eine Formel als eine einfacheZeichenreiheauffassen.DieseZeichenreihelasstsich in einenComputereingeben.Man kannso nacheinemAlgorithmusfragen,der entscheidetob eineeingegebeneFormel erfullbar ist odernicht. Es istnicht allzuschwer, ein Computerprogrammzu schreiben,welchesdiesleistet.EineoffensichtlicheHer-angehensweisehierfur ist es,ein Programmzu schreiben,welchesalle moglichenBelegungenderFor-mel durchprobiertund feststellt,ob fur irgendeinedieserBelegungendie Formelzu ’1’ auswertet.HateineeingegebeneFormeln atomareTeilformeln,somussenmit diesernaivenMethodeschlimmstenfalls(wenndie Formelunerfullbar ist) 2n verschiedeneBelegungendurchgetestetwerden.Die

”worst-case“

LaufzeiteinessolchenAlgorithmuswaredannexponentiellin derAnzahlderatomarenFormeln.

Exkurs: Massefur die Geschwindigkeit (Komplexitat) einesAlgorithmuslassensichmit Mitteln derKomplexitatstheorie(sieheVorlesung

”TheoretischeInformatik“ ) formulieren.ExponentielleAlgorith-

mengehorendabeizu den”sehrlangsamen“ Algorithmen.Die Frageist berechtigt,ob esfur die Erfull-

barkeitsproblematiknichteinwesentlicheschnelleres(polynomiales)Verfahrengebenkonnte.In derTathandeltessichhierbeium die wohl grosstederzeitungelosteFrageder Informatik. Die BeantwortungdieserFragebeantwortetgenaudasberuhmte

”P NP?“ -ProblemdertheoretischenInformatik.

Wir wollen nun sehen,dasssich zunachstinnerhalbder Logik viele Problemeauf dasErfullbarkeits-problemzuruckfuhrenlassen.Hierzufuhrenwir die Abkurzung �R� F fur die Aussage

”F ist erfullbar“

ein. Der Ausdruck �R� F ist ‘1’ wennF erfullbar ist und ‘0’ andernfalls. Beispielsweisesind folgendeProblemeaufdasEntscheidbarkeitsproblem zuruckfuhrbar:* GegebenG, ist G unerfullbar?(Teste:

” � �R� G � 1“ )* GegebenF1 �������O� Fk, sindF1 �������O� Fk gleichzeitigerfullbar?(Teste:”�S� F1 � F2 � ����� Fk , 1“ )* GegebenG, ist G eineTautologie?(Teste:

” � �S� � G � � 1“ )* Folgt G ausF1 �������H� Fn? (Teste:” � �S� � ��� F1 � F2 � ����� � Fk ,� G � � 1“ )

Wir wollenunskurzzweimehrpraxisorientierteProblemebetrachten,dieaufdasErfullbarkeitsproblemzuruckgefuhrt werdenkonnen.

Beispiel1.14.1 Zunachst betrachtenwir dasProblemdasunter demNamenbipartite graph matchingbekanntist. Man kenntesauch unter demBegriff

”StabileHochzeiten“ . Betrachtenwir ein virtuelles

Heiratsvermittlungsinstitut, welchesin seinerKartei n Mannerund n Frauenhat. Aus den jeweiligen

23

angabender VorliebenkanndasHeiratsinstituterkennen,wer mit wemeinehinreichendharmonischeEheverbringenkann.Nunist dasHeiratsinstitutdaraninteressiert,moglichstalle MannerundFrauenindenstabilenHafenderEhezubringen(denndasbringt demInstitutammeistenGeld).Glucklicherweiseist amInstitutauch einLogiker angestellt,derdasProblemwie folgt modelliert:

Wir fassendie MannerundFrauenals Knotenin einemGraphenauf. Ein MannundeineFrau werdenmit einerKanteverbunde, sofernsiepotentielleEhepartnersind.Ziel ist esnuneineAuswahlvonKanten(Hochzeiten)zu treffen,sodassjederMannmit genaueinerFrau verbundenist. EineBeispielsituationist in Abb. 1.5.gegeben.

PSfragreplacements

A1

A2 A3A4

A5

A6 A7

M1 M2 M3 M4

F1 F2 F3 F4

Abbildung1.5:BeispieleinesErfullbarkeitsproblems

Wir ordnennun jeder der Kanteneine entsprechendeatomare Teilformel A1 �������H� A7 zu. Das Vorhan-denseinbzw. nicht-Vorhandenseineiner Kantecodieren wir in denentsprechendenWahrheitswertderatomaren Formel.Die Tatsache, dassbei M1 genaueineder KantenA1 bzw. A2 eingeht, lasstsich als� A1 � � A2 � � � A1 � A2 J 1. formulieren.Die Tatsache, dassA3 amKnotenM2 eingeht lasstsich ein-fach als A3 1 formulieren. Die Tatsache, dassvon A4, A5, A6 genaueineKantebei M3 eingeht ist� A4 � � A5 � � A6 � � � A4 � A5 � � A6 � � � A4 � � A5 � A6 . Und so weiter fur jedenKnoten.Alle dieseFormelnsollengleichzeitgerfullbar sein.Wir erhaltenalsodurch betrachtenaller Knoten��� A1 � � A2 � � � A1 � A2 � � � A3 � ��� A4 � � A5 � � A6 � � � A4 � A5 � � A6 � � � A4 � � A5 � A6 � � � A7 � � A1 � ��� A2 � � A3 � � A4 � � � A2 � A3 � � A4 � � � A2 � � A3 � A4 � � ��� A5 � � A7 � � � A5 � A7 � � � A6 DieseFormelist genaudannerfullbar, wenneseineMoglichkeit gibt alle Personenzuverheiraten.

Tatsachlichsinddie Formeln,die ausdemletztgenanntenBeispielentstehen,von sehrspeziellerNatur.Es existierenfur diesenSpezialfall desErfullbarkeitsproblemsogarpolynomiale(d.h. schnelle)Algo-rithmen.DasnachsteBeipiel verdeutlicht,dassschongeringfugigeVerallgemeinerungenzu wesentlichschwierigerenErfullbarkeitsproblemenfuhren.

Beispiel1.14.2 Stellenwir unseineFirma vor, in der 3n Personen1 � 2 �������� 3n arbeiten.Es ist bekannt,dassnur bestimmtePaare von Personen(z.B. � 1 � 2 �H� 1 � 7 �H� 2 � 9 T���H� ) gerne zusammenarbeiten.Ist esmoglich, n Dreierteamszubilden,sodassin jedemTeamjedergernemit jedemarbeitet?Wiederkonnenwir dasProblemals Graphmodellieren,bei demgewisseKantenausgewahlt werdenmussen.

24

DiesesProblemist formulierbaralsErfullbarkeitsproblem (selbstprobieren).Allerdingsist dasProblemnicht effizientlosbar:im wesentlichenist nur Durchprobierenmoglich.

1.15 Resolutionsalgorithmus

Wir habengesehen,dassmanzurNot durchProbierendasErfullbarkeitsproblem algorithmischentschei-denkann.Wir wollen nun einenAlgorithmusfur dasErfullbarkeitsproblemkennenlernen,der zumin-destfur einigewichtigeSpzialfalle ein wesentlichbesseresGeschwindigkeitsverhalten aufweist.DiesersogenannteResolutionsalgorithms ist auchdie Grundlagevieler Programmiersprachenin der Logik-Programmierungwie z.B. von PROLOG(sieheKapitel 4).

Um unsim Folgendenein wenigSchreibarbeitzu sparen,fuhreneineMengenschreibweisefur Formelnin konjunktiver Normalformein.EineFormelF in KNF bestehtauseiner‘ � ’-VerknupfungvielerKlau-selnK1 � K2 �������O� Kn. JedeKlauselselbstbestehtauseiner‘ � ’-Verknupfungvon Literalen.

Wir schreibennunjedeeinzelneKlauselalseineMenge,diealleLiteraleenthalt. Sowird z.B.A � � B � Czu�A � � B � C � . MehrfachauftretendeLiterale tretendabeiin der Mengenur einmalauf. Dies tragt der

TatsacheRechnung,dasseineWiederholungdesgleichenLiterals innerhalbeinerKlauselnichtsanderSemantikderFormelandert(dennA � A � A). Alle KlauselderFormelF fassenwir wiederumin einerMengezusammen.Auch hier unterstutzt die Mengenschreibweisedie Tatsache,dasMehrfachvorkom-menderselbenKlauselkeinenEinflussaufdie Semantikhat.

Beispiel1.15.1 Die Formel

F �� A � B � � C � � � A � � E � � � C � D � E � � C � � � D � � C entspricht in derneuenSchreibweisederMenge

F �L� A � B � � C ��� � � A � � E ��� � � C � D � E ��� � C ��� � � D � � C �L���Wichtig ist hierbei,dasses sich bei der Mengenschreibweisetatsachlich nur um eine andereArt derDarstellungdergleichenFormelhandelt.Da nachAbschnitt1.12jedeFormelF eineKNF besitzt,kannmanauchjedeFormelin Mengenschreibweisedarstellen.

Wir gebennuneineRegelan,wie manauszweiKlauselneineneuegewinnt: densogenanntenResolven-ten.

Definition 1.15.2(Resolvent) SeienK1 � K2 undR Klauseln.R ist ResolventvonK1 undK2, falls eseinLiteral L gibt, sodassL ' K1und� L ' K2 und

R �� K1 U � L �V XWY� K2 U � � L �V �25

Zwei KlauselnK1 undK2 sindalsomiteinanderresolvierbar, wennesein Literal L gibt, welchesin K1

vorkommt und welchesnegiert in K2 vorkommt. Der Resolvent entstehtdann,indemmanausK1 dasLiteral L entfernt,ausK2 dasLiteral � L entfernt,unddie beidensoentstandenenMengenvereinigt.Sohabenz.B. die beidenKlauseln

�A � B � � C � und

� � A � � E � denResolventen�B � � C � � E � . Man notiert

einensolchenResolutionsschritt auchoft in FormeinesResolutions-Diagramms:PSfragreplacements�

A � B � � C � � � A � � E ��B � � C � � E �

� A � B � � C �H� � A � � E darausfolgt � B � � C � � E

Abbildung1.6:Resolutionsschritte

Warum ist man nun an Resolventeninteressiert?Ein Resolvent ist eine logischeKonsequenzseinerbeidenKlauseln.Hat manalsoeineBelegung,die BeideKlauselnwahrmacht,so ist auchautomatischderResolventwahr(Vorsicht,dasUmgekehrteist nichtderFall).

Satz1.15.3(Resolvent ist FolgerungseinerKlauseln) Sei K1 und K2 Klauselnund R ein ResolventdieserKlauseln.Hat maneineBelegung " mit "&� K1 J 1 und "&� K2 � 1, soist auch "&� R J 1.

Beweis: SeiL ' K1 dasLiteral, welcheszurResolutionfuhrt.Nehmenwir an,wir habeneineBelegung" , die K1 undK2 wahrmacht.Wir unterscheidenzwei Falle.

Fall 1 "&� L Z 0: da "&� K1 Z 1 ist, musses in K1 ein weiteresLiteral L 6 mit "&� L 60 / 1 geben.NachDefinition desResolventenkommt diesesLiteral L 6 auchin R vor. Da R nur ausmit oder verknupftenLiteralenbesteht,gilt somit "&� R , 1.

Fall 2 "&� L 4 1: GehtanalogzuFall 1.NurmussendieRollenvonL, � L undK1, K2 vertauschtwerden.

Der o.g. Satzhangtauchdamit zusammen,dassessich bei der folgendenFormel um eineTautologiehandelt(wie manz.B.durchWahrheitstafelnachprufenkann):� L � F � � � L � G ��[� F � G �Wir kommenaufdiesenSachverhaltspaternochmalszuruck.

Analogie: Beim HerleitendesResolventenauseinerKlauselhandeltessichum einenganzanalogenVorgangzumHerauslosenvonVariablenauseinemGleichungssystem.Habenwir z.B.zweiGleichungen13x U y \ 2w 0 undy \ 5t U 2q 0 sokonnenwir dieseaddierenunderhalten13x \ 2w \ 5t U 2q 0.Die letzteGleichungist einelogischeKonsequenzdererstenbeiden,dieVariabley wurdeherausgelost.

Ist R Resolvent zweierKlauselnin F , so konnenwir R zu denKlauselnvon F dazunehmen,ohnedieSemantikvon F zu verandern.Nehmenwir alle moglichenResolventenhinzu,so sprichtmanvon derResolventenmenge von F.

Definition 1.15.4(Resolventenmenge)SeiF eineFormelin KNF.

Res� F � � R D Rist ResolventzweierKlauselnin F �JW F

26

Die MengeRes� F bestehtalso ausallen Klauselnvon F und allen moglichenResolventenvon F.Insbesondereist Res� F wiedereineFormelin konjunktiver Normalform.Esgilt

Satz1.15.5 F ist semantisch aquivalentzuRes� F .Beweis: Sei " einezu F passendeBelegungund seienK1 �������H� Kn die Klauselnvon F. Angenommen"&� F Z 1. In diesemFall gilt fur alle Klauseln "%� Ki Z 1. Sei nun R Resolvent zweierKlauselnvonF. Nach Satz 1.15.3 gilt "&� R ] 1 Somit werten alle Resolventenunter " zu ’1’ aus.und es gilt"&� Res� F � , 1.

Seiumgekehrt "&� F � 0, danngilt sicher"&� Res� F � , 0, daja F � Res� F .Wir konnennundenProzessdesHinzunehmensvon Resolventenwiederholtanwenden.Wir setzen:

Res0 � F � FRes1 � F � Res� Res0 � F � , Res� F Res2 � F � Res� Res1 � F � , Res� Res� F � ...Resi � F , Res� Resi ^ 1 � F � ...

Die FormelResi � F entstehtalsodurch i-mal wiederholtesAnwendendesRes�_�����+ Operators.Bemer-kenswerterweisegibtesdabeieinenPunkt,wobeidieserwiederholtenAnwendungkeineneuenKlauselnmehrhinzukommen.

Satz1.15.6(Sattigung der iterierten Resolution) SeiF eineFormelin KNF. Esgibt ein i mit

Resi � F � Resi ` 1 � F �Beweis: DerBeweiswird in denUbungendurchgefuhrt. Er ist eineeinfacheKonsequenzausderTatsa-che,dassesuberendlichvielenatomarenTeilformelnnur endlichviele semantischverschiedeneKlau-selngebenkann.

Die gesattigte Resolventenmengewird von uns bald von grosserBedeutungsein.Fur das i ausdemobigenSatzsetzenwir dafur

Resab� F J Resi � F �Insbesonderegilt:

Satz1.15.7 F ist semantisch aquivalentzuResa � F .Beweis: Der Satzfolg durchwiederholteAnwendungvon Satz1.15.5.undderSattigungsaussagevonSatz1.15.6.Wir habenF Res0 � F J� Res1 � F ��N�����c� Resi � F ,�K�����V� Resa � F �

27

Wollenwir eineAussageuberdieErfullbarkeit einerFormelF machen,soliefert Resa � F sehrnutzlicheInformation.Fur jedesModell " von F mussenalle (!) Klauselnin Resa � F erfullt sein.Insbesondere,wennResa � F einelementigeKlauselnenthalt, konnenwir darausdirekt notwendigeVariablenbelegun-genvon deratomarenTeilformelnvon F ablesen.

Beispiel1.15.8 Betrachtenwir wiederdie Formel

F �� A � B � � C � � � A � � E � � � C � D � E � � C � � � D � � C �DasfolgendeDiagrammzeigteinige Resolutionsschritte.

PSfragreplacements

dC e dVf

D g f C edVf

D e dVfC g D g E e

dVfC g E e d

C edE e dVf

A g f E edVf

A e dA g B g f C e

dB g f C e d

C edB e

Abbildung1.7:Resolutionsschritte

Insbesondere stellenwir fest,dassin Resa � F die Literale � A, B, C, � D und E auftreten.Fur jedesModell vonF mussendieseLiterale zu‘1’ auswerten.Die BelegungA 0, B 1, C 1, D 0, E 1ist somitdaseinzigmoglicheModell vonF.

28

1.16 Die leereKlausel

In unsererBetrachtungvon Resolutionund Resolutionsschrittenmussenwir der Klausel,welcheauseinerleerenMengevon Literalenbesteht,besondereBeachtungschenken.Erinnernwir uns,dasseineKlausel

�L1 � L2 �������H� Lk � einer oder-Verknupfung L1 � L2 � ����� � Lk der Literale entspricht.Habenwir

eineKlausel�L � mit nur einemLiteral, entsprichtdieseder Formel L, die nur ausdemLiteral selbst

besteht.Tritt die leereMengealsKlauselauf,mussenwir unsGedankenmachen,wasesbedeutet,wennmaneineoder-VerknupfungubereineleereMengevonLiteralendurchfuhrt. Letztlichbleibtunshierfurnichtsanderesubrig, alsdies“willk urlich” zu definieren.Dennochsollte (um insgesamtein stimmigesSystemzu erhalten)dieseDefinition sogetroffen werden,dasssiemit Eigenschaftenin Einklangsteht,die manvon verknupftenLiteralenerwartet;und die wir spaternochausnutzenwerden.Dies schranktuns,wie die folgendenUberlegungenzeigen,in der Wahl der Moglichkeiten fur die Definition kraftigein.

Betrachtenwir hierzunochmalsdie Klausel�L1 � L2 �������H� Lk � . Fur einebestimmteBelegung " evaluiert

diesezu ’1’ genaudann,wenneswenigstensein Li in der Klauselgibt mit "%� Li . 1. UbertragenwirdieseEigenschaftauf die Menge

� � , welchekein Literal enthalt, somussenwir diesesingemassimmerzu ’0’ auswerten(in

� � gibt eskein Literal, daszu ’1’ auswertet).Wir definierensomit "&� � �V / 0 furbeliebigeBelegungen" .

Bemerkung: Analogkannmanargumentieren,dasseineund-VerknupfungubereineleereMengeim-merzu ’1’ evaluiert.

In Ubereinstimmungmit derrestlichenLogikliteraturfuhrenwir fur die ausderleerenMenge� � beste-

hendeKlauselnochdasZeichen’ h ’ ein.

UnsereDefinition "&�ihC J 0 stehtin schonemEinklangmit derfolgendenBeobachtung:

Satz1.16.1 Ist hK' Resa � F , soist F unerfullbar.

Beweis: Sei F eine Formel und hP' Resa � F . Die leereKlausel h kann nur durch einenResolu-tionsschrittzweier Klauselnder Form

�L � und

� � L � entstandensein.Also gibt es ein Literal L mit�L �j' Resa � F und

� � L �k' Resa � F . In jederBelegung " mit "&� F � 1 musswegenSatz1.15.7gelten"&� L � 1 und "&� � L J 1. Diesist aberunmoglich,alsoist F unerfullbar.

Beispiel1.16.2 Wir zeigenmit Resolutiondie Unerfullbarkeit der folgendenKlauselmenge:

F �L� A � � B ��� � � A ��� � B �L�Wir konnendie folgendenResolutionsschritte durchfuhren:

PSfrag replacements

�A � � B � � � A �

� � B � �B �

hAlso hK' Resa � F , undnach Satz1.16.1folgt die Unerfullbarkeit vonF.

29

1.17 Exkurs: Beweismethoden

Im nachstenKapitel werdenwir unsdamitbeschaftigen,die Umkehrungvon Satz1.16.1zu zeigen:“ IstF unerfullbar, so liegt h in Resa � F .“ Bevor wir unsjedochan diesesnicht ganzleichteUnterfangenwagen,mochteich andieserStellenochein paarprinzipielleWortezuBeweisverfahrensagen.

DemaufmerksamenLeserwird aufgefallen sein,dasswir unsbeimDurchfuhrenvon formalenBewei-senauf dieserelementarenStufeder Logik immer ein wenig aufsGlatteisbegeben.Wie eingangsdesSkripteserwahnt,soll ja Logik gerade(unteranderem)dazudasein,die formalenGrundlagen desma-thematischenBeweisenszuschaffen. Fangtmannunaberan, formaleBeweisezu verwenden,um damitdieGrundlagendesformaleBeweisenszuschaffen, lauftmanstandigGefahr, sichin einenZirkelschlusszu verfangen,derdasganzeGedankengebaudezumEinsturzenbringenkann.Wir werdenspatersehen,daseshierfur Moglichkeitengibt, sichquasi

”andeneigenenHaarenausdemSumpfzu ziehen“ . Man

formuliert dasBeweisenals einenrein syntaktischenProzessderFormelmanipulationund stellt spaterfest,dassdieserBeweisbegriff mit demmehroderwenigerintuitivenBeweisbegriff ubereinstimmt.DerRahmenunsererVorlesunggestattetesjedochim Momentnicht, auf dieseSubtilitateneinzugehen,dadieseinsbesondereeinenerheblichgrosserentechnischenAufwandbenotigen.Wir gehenmehroderwe-nigerdavonaus,dassirgendeinLogikerdieseArbeit bereitsfur unsgemachthatundwir unsmit unserenBeweisen,sofernwir unsnuranbestimmteRegelnhalten,aufsicheremBodenbefinden.

Dennochmochteich an dieserStelleeinmalexplizit aufzahlen,welchedieserRegeln bei unserenBe-weisenstandig wiederverwendetwerden.Viele dieserRegeln erscheinennahezubanalund bedurfenanscheinendkeinerweiterenBegrundung.Dennochsolltemansichdaruberim Klarensein,dassessichbeimAnerkennendieserRegelnletztlich um eineArt gesellschaftlicheKonventionhandelt.

1.17.1 Schlussregel

Habenwir die Aussage”Aus A folgt B“ bereitsbewiesen,und wissenwir ferner, dasdie Aussage

”A“

wahrist, sodurfenwir ausbeidenAussagenzusammen”B“ folgern.

Wir habenhiervonz.B.beimBeweisvonSatz1.16.1gebrauchgemacht.EinerderBeweisschrittebestand(beinahererBetrachtung)ausderfolgendenArgumentation:

Wir wissen”Aus "%� F � 1 folgt "&� Resa � F � , 1“

undwissen”"%� F , 1“

alsogilt”"&� Resa � F � , 1“ .

1.17.2 Widerspruchsbeweis

Ein haufigesMuster zum BeweiseneinesSachverhaltes”A“ ist der sogenannteWiderspruchsbeweis.

Man nimmt dazutemporar die Wahrheitder negiertenAussage” � A“ an und fuhrt dieseAussagezu

einemWiderspruch.Widerspruch heissthierbei,dasman sowohl eine weitereAussage”B“ als auch

derenNegation” � B“ folgernkann.Diesekonnennicht gleichzeitigwahrsein,alsomussdie Annahme

” � A“ falschgewesenseinundsomitdie eigentlichzu beweisendeAussage”A“ stimmen.

Auch hiervon wurdeim Beweisvon Satz1.16.1Gebrauchgemacht.Um zu zeigen,dassF unerfullbarist, nahmenwir vorubergehendan,esgabeein " mit "&� F , 1. Darauskonntenwir wiederumfolgern,dasssowohl "&� L J 1 alsauch"&� L kl 1 geltenmuss:ein Widerspruch.

30

1.17.3 VollstandigeInduktion

Eine weitereBeweistechnikist die sogenanntevollstandige Induktion. VollstandigeInduktion wird oftangewandt,wennmannichtnureineAussage,sonderneine(abzahlbar)unendlicheKlassevonAussagenbeweisenwill. Abzahlbarheissthierbei,dassmandie Aussagendurchnumerierenkann.Also angenom-menwir habeneineunendlicheSequenzvon AussagenA0 � A1 � A2 ������� undwollendieAussage

”Fur alle i

gilt Ai“ beweisen.Wir stehenhierbeivor demProblem,dasswir womoglichnichtunendlichvieledirekteBeweiseangebenkonnen(undwollen).EinenAusweg schafft dieMethodedervollstandigenInduktion.HierzumussmanzweiAussagenbeweisen:

1.”A0 ist wahr“ (Induktionsanfang).

2.”AusAi folgt Ai ` 1“ (Induktionsschluss).

Hiermit hatmanzwarnichtunendlichvieleBeweiseaufgeschrieben,abereineMethodeangegeben,wiemanim Bedarfsfall jedeeinzelnedieserAussagen(unterVerwendungderSchlussregel) herleitenkann.Verlangtjemandz.B.einenexplizitenBeweisderAussageA3 sokannmanargumentieren

”A0 ist wahrundausA0 folgt A1. Also ist auchA1 wahr.“

”A1 ist wahrundausA1 folgt A2. Also ist auchA2 wahr.“

”A2 ist wahrundausA2 folgt A3. Also ist auchA3 wahr.“

DieseArgumentationgehtnaturlich fur jedebeliebigeAussageAi, die Schlusskettewird blosslanger.

Beispiel1.17.1 Wir wollenzeigen,dass

n

∑j = 1

j n2 \ n2

�Wir zeigenzunachst,dassdie Aussage fur n=1 gilt: ∑1

j = 1 j 1 12 ` 12 �

Nunzeigenwir, dassausderAussage ∑ij = 1 j i2 ` i

2 die Aussage ∑i ` 1j = 1 j Gm i ` 1n 2 ` m i ` 1n

2 folgt.

i ` 1

∑j = 1

j i

∑j = 1

j \ i \ 1 i2 \ i2

\ i \ 1 i2 \ i2

\ 2i \ 22

i2 \ 2i \ 1 \ i \ 12

� i \ 1 2 \o� i \ 1 2

1.18 Hauptsatz der Resolution

Wir zeigennun,dassauchdieUmkehrungvon Satz1.16.1gilt.

Satz1.18.1(Hauptsatzder Resolution) F ist genaudannerfullbar, wenn h#l' Resa � F .

31

Beweis: Nachdemwir die eineRichtungdesBeweisesbereitsdurchSatz1.16.1abgedeckthaben,ver-bleibtzuzeigen,dassausderUnerfullbarkeit vonF dieAussagehp' Resa � F folgt. OhneBeschrangungderAllgemeinheit,konnenwir annehmen,dassF keineKlauselK enthalt, die gleichzeitigein Literal LunddessenNegation � L enthalt. EinesolcheKlauselwarenamlicheineTautologieundwurdekeinerleiBeitragzur gesamtenFormelleisten.

Wir fuhrendenBeweisdurchvollstandigeInduktionuberdieAnzahlderatomarenTeilformeln,die in Fauftreten.

Induktionsanfang: Wir zeigenzunachst,dassdie Aussagefur alle Formelnmit lediglich einemAtomA gilt. EinesolcheFormelkann(unterunsererobigenAnnahme)nur die Klauseln

�A � und

� � A � ent-halten.Enthalt sie nur eine dieserKlauseln,so ist sie erfullbar. Unerfullbar ist also nur die FormelF �L� A ��� � � A �L� . Ein Resolutionsschrittzeigt hK' Res� F .Induktionsschluss: Nunmehrwollen wir ausderTatsache,dassdie Behauptungfur alle Formelnmithochstensi Atomengilt, zeigen,dasssie auchfor alle Formelnmit hochstensi \ 1 Atomengilt. Wirkonnenalsoals Induktionsannahmevoraussetzen,dassfur alle FormelnF mit i AtomenA1 �������� Ai gilt:“AusF unerfullbar folgt hK' Resa � F ”.SeinunF unerfullbar mit AtomenA1 �������O� Ai � Ai ` 1. Wir betrachtenfunf verschiedeneMegenvon Klau-seln.

F0 � K DK ' F � Ai ` 1 ' K � (Alle Klauseln,die Ai ` 1 enthalten.)F1 � K DK ' F � � Ai ` 1 ' K � (Alle Klauseln,die � Ai ` 1 enthalten.)G F U � F0 W F1 (Alle Klauseln,die wederAi noch � Ai ` 1 enthalten.)F 60 � K U � Ai ` 1 �XDK ' F0 �F 61 � K U � � Ai ` 1 �XDK ' F1 �

UnsereallgemeineAnnahme,dassF keineKlauselnenthalt, die gleichzeitigein Literal undseineNe-gationenthalten,zeigt,dassF die disjunkteVereinigungder MengenF0, F1 und G ist. DasheisstjedeKlauselvon F kommtin genaueinerdieserdreiMengenvor.

Wir machennuneineFolgeeinfacherBeobachtungen:

(1) FallsGunerfullbar, danngilt (nachInduktionsvoraussetzung) hq' Resa � G unddamit hq' Resa � F .Wir konnenbisaufweiteresalsodieAnnahmemachen,dassG erfullbar ist. Zur spaterenReferenzbezeichnenwir dieseAussagemit �srV .

(2) G W F 60 ist unerfullbar.Beweis: WareG W F 60 erfullbar mit Belegung " :

�A0 �������O� Ai �t� �

1 � 0 � , so wahlt maneinfach" i ` 1 0. DieseBelegungerfullt G � F0 undF1. Dies ist ein Widerspruchzur Unerfullbarkeit vonF.

(3) G W F 61 ist unerfullbar.Beweis: analogzu (2).

(4) hK' Resa � G W F 60 Beweis: G W F 60 hatnur i Atomeundist nach(2) unerfullbar. Die Induktionsvoraussetzung impli-ziert, dassh�' Resa � G W F 60 . Zur weiternReferenzbezeichnenwir die hier zumHerleitenvon hverwendeterResolutionsfolgemit u 0.

(5) hK' Resa � G W F 61 Beweis: wie bei (4). Zur weiternReferenzbezeichnenwir diehier zumHerleitenvon h verwen-deterResolutionsfolgemit u 1.

32

(6) Ai ` 1 ' Resa � G W F0 Beweis: Wir betrachtendie Resolutionsfolgeu 0. Wir stellenzunachstfest,dass,weil G wegen(*) erfullbar ist, an u 0 mindestenseineKlauselausF 60 beteiligt ist. Nun ersetzenwir in u 0 jedesVorkommeneinerKlauselK ausF 60 durchdie entsprechendeKlauselK W � Ai ` 1 � ausF0. Fuhrenwir die soveranderteResolutionsfolgeaus,soerzeugtdiesedasLiteral Ai ` 1.

(7) � Ai ` 1 ' Resa � G W F1 Beweis: analogbei (6) nurmit u 1 alsResolutionsfolge.

(8) hK' Resa � F Beweis: DieseAussagefolgt direkt ausaus(6) und(7) undeinemResolutionsschritt.

Aussage(8) ist genauunsereherzuleitendeTatsache.

1.19 Resolutionsalgorithmus

Die ErkenntnissederletztenAbschnittekonnenwir direkt in einenAlgorithmusumformen,derentschei-det,obeineFormelerfullbar ist odernicht.Wir musseneinfachderReihenachimmerneueResolventenherleitenund feststellen,ob irgendwanndabei h in derResolventenmengeauftaucht.In etwas

”salop-

per“ Schreibweiselasstsich der Algorithmus wie folgt formulieren(hierbei sind F und G geeigneteDatenstrukturenfur Klauselmengen):

Algorithmus 1.19.1Eingabe:EineFormelF in KNF.

Ausgabe:”Ja“ wennF erfullbar ist.

”Nein“ sonst.

repeat�

G : F;

F : Res� F ;� until �ihK' F or � F G if hK' F write(“No”);

elsewrite(“Yes”);

NachallembisherGesagtenist esklar, wie derAlgorithmusarbeitet.Bei dersukzessiven Hinzunahmevon Resolventen,wird entwederirgendwanndie leereKlausel h erzeugt.Dannsindwir fertig undwis-sen,dassF unerfullbar ist. Odereswird auf GrundderSattigungseigenschaft der iteriertenResolutionder Punkterreicht,an dem keine neuenResolventenmehr erzeugtwerdenkonnenund h nochnichtabgeleitetwurde.Dannsindwir fertig undwissennachSatz1.18.1,dassF erfullbar ist.

1.20 Folgerung von Literalen

Wir werdenspater, wennwir dieLogikprogrammiersprachePROLOGbehandeln,sehen,dassmanhaufigdasZiel hat,fur einegegebenenFormelF zu entscheiden,ob ausihr ein bestimtesLiteral L folgt. (MitanderenWorten:zu entscheidenob fur jedeBelegung,mit "&� F � 1 automatisch"%� L , 1 gilt).

33

Dar HauptsatzderResolutiongestattetunsnun,in einemsolchenFall mit demResolutionsalgorithmuszu uberprufen.

Satz1.20.1 Sei F eine Formel in KNF und L ein Literal. L ist Folgerung von F genaudann,wennhK' Resa � F W � � L �V .Beweis: NachSatz1.18.1genugt eszu zeigen,dassdie Aussage

”L ist Folgerungvon F“ gleichwertig

mit der Unerfullbarkeit von F W � � L � ist. SeialsoL Folgerungvon F . Entwederist F selbstunerfull-bar, oderesgibt eineBelegung " mit "&� F Z 1. Danngilt aberauch "&� L ! 1. Somit ist F W � � L �unerfullbar. SeiumgekehrtF W � � L � unerfullbar. Entwederist bereitsF unerfullbar, womit L trivialer-weiseFolgerungvon F ist. Andernfalls gibt e eineBelegungmit "%� F J 1. Fur diesemussaber, wegenderUnerfullbarkeit von F W � � L � gelten:"&� L , 1. Somitist L Folgerungvon F.

Man konntezunachstmeinen,dasZeigenderUnerfullbarkeit von F W � � L � seiein umstandlicherWeg,um zu beweisendassL Folgerungvon F ist. In der Tat wird in vielen Fallen L einfach selbstin deriteriertenResolventenmengevonF auftauchen.DiesmussjedochnichtderFall sein,wennF unerfullbarist.DasdurchSatz1.20.1nahegelegteVerfahrenfasstaufeinfachsteWeisediesebeidenFallezusammen.

1.21 Hornklauseln

Abschliessendwollen wir unserAugenmerknochauf einespezielleForm von Klausenrichten,die so-genanntenHornklauseln.

Definition 1.21.1 EineKlausel,diehochstensein positivesLiteral enthalt heisstHornklausel.

Hornklauselnsindauszwei Grundensehrwichtig. Erstenskannfur eineFormelF, die nur ausmehre-renHornklauselnbestehtrelativ

”schnell“ entschiedenwerden,ob h1' Resa � F . Zweitensmodellieren

HornklauselngenaudasAuftretenvon”Fakten“ ,

”Regeln“ und

”Anfragen“ in einerDatenbank.

Um dieseinzusehen,machenwir unszunachstklar, welcheFormeneineHornklauselannehmenkann.Betrachtenwir eineFormelF welcheeineHornklauselK enthalt.

Fall 1: Die HornklauselK bestehtnurauseinemeinzigenpositivenLiteral L. EineBelegung " , die Fwahrmacht,mussdannnotwendig"&� L J 1 haben.DasLiteral L ist ein Faktum.

Fall 2: Die HornklauselK habedie Form� � H1 ������� � Hk � C � fur atomareFormelnH1 �������O� Hk � C. Wir

haben

K � H1 � ����� � � Hk � C � � � H1 � ����� � Hk � C � � H1 � ����� � Hk �� C �Sindin einerBelegungmit "&� F 5 1 dieAtomeH1 ������� Hk mit ’1’ belegt, somussauch"&� C � 1 gelten.EinesolcheHornklauselkannauchalsRegel aufgefasstwerden.Die HypothesenH1 ������� Hk implizierendieKonklusionC.

Fall 3: EtwassubtileristderFall wennK lediglichausnegiertenLiteralenbesteht.SeiK � � Q1 ������� � Qk �mit AtomenQ1 �������O� Qk. Wir habendann

K � Q1 � ����� � � Qk � � � Q1 � ����� � Qk �Nehmenwir weiteran,dassF ansonstennurausHornklauselnderFormenausFall 1 undFall 2 besteht,so konnenwir die KlauselK als die folgendeAnfrage (Query)auffassen:

”Folgt ausallen Faktenund

Regelnin F die AussageQ1 � ����� � Qk?“ Diesist genaudannderFall, wennF W � K � unerfullbar ist.

34

Beispiel1.21.2 Betrachtenwir die folgendeAnsamlungvoneinemFaktumundvier Regeln:

1 : A2 : A � B3 : A � C � D4 : A � B � C5 : B � D � E

Wir konnenall dieseKlauselnin einerKNF, welchenur ausHornklauselnbesteht,zusammenfassen.

F �L� A ��� � � A � B ��� � � A � � C � D ��� � � A � � B � C ��� � � B � � D � E �L�Wir konnenF als

”Datenbank“ vonRegeln undFaktenauffassen.An diesekannmanjetztzumBeispiel

die Anfrage”gilt ’E’?“ stellen.Hierzumuss(nach Abschnitt 1.20)lediglich die Nicht-Erfullbarkeit von

F W � � E � nachgewiesenwerden.(Manbeachtedas � E eineweitereHornklauselist.) Dieskannz.B.mitdemResolutionsalgorithmusgeschehen.Aber auch ohneResolutionsalgorithmuskannmansich leichtklarmachen,dassE ausdenRegeln und Faktender Datenbankfolgt. Faktum’1’ in unserer Liste er-zwingt,dassin jeder Belegung " die F wahrmacht "&� A Z 1 geltenmuss.Aus Regel ’2’ erhalt mandann"&� B 5 1. Regel ’4’ liefert dannmit (zusammenmit "%� A 5v"&� B 5 1), dassauch "&� C 3 1 geltenmuss.Regel ’3’ liefert nun "&� D J 1. Schliesslich liefert Regel ’5’ gerade "&� E � 1. DieseAbleitungs-folge lasstsich naturlich einszueinsin eineResolutionsfolge ubersetzen.

FurdasBearbeitenvonAnfragenaufdurchHornklauselngegebenenDatenbankenausRegelnundFaktengibt eswesentlicheeffektivereVerfahrenalsdasstureAbleitenaller moglichenResolventen.Man kannversuchendieRegelstrukturdirektauszunutzen.Hierbeigibt eszwei prinzipielleVorgehensweisen:

bottom-up: ManmarkiertzunachstalleFaktenals”bewieseneAussagen“ . Ausgehendhiervonmarkiert

manalle Literale als”bewiesen“ , die sich durchRegeln ausdenschonbewiesenenAussagenableiten

lassen.DiesmachtmansolangebisentwederdieAnfrageals”bewieseneAussage“ erreichtwird, oderbis

keineweiterenAussagenbewiesenwerdenkonnen.DiesesMarkierungsalgorithmusgenannteVerfahrenhat denNachteil,dasseventuell viele Aussagenabgeleitetwerden,die zur Anfrage uberhauptkeinenBeitragleisten.Die in unseremBeispielverfolgteStrategie entsprachgenaudiesemVorgehen.

top-down: Man gehtvon der Anfrageausund suchtnachRegeln, ausdenendie Anfrageabgeleitetwerdenkann.Die in diesenRegelnaufretendenHypothesenliteralefasstmanalsneueAnfragenauf,die

”rekursiv“ bearbeitetwerden.Entwederkannmanletztlich jedeAnfrageauf Faktenzuruckfuhren,oder

mannbleibt irgendwannstecken.DiesesVorgehenentsprichtdemin derProgrammiersprachePROLOGzumeistimplementiertenAlgorithmus.

Beispiel1.21.3 In userem obigem Beispielwurde eine top-downStrategie ungefahr so aussehen.Wirwollen E beweisen.Regel ’5’ sagt, dasswir dasnur erreichenwennwir zunachst B und D beweisen.Regel ’2’ sagt, dassB ausA bewiesenwerdenkann.Fakt ’1’ sagt, dassA aber Faktumist. Somitist Bbewiesen.Esbleibtalsonoch D zubeweisen.Undsoweiter �����1.22 Ein Ausblick auf PROLOG

Die SprachePROLOG machtexplizit Gebrauchdavon, Fakten,RegelnundAnfragenalsHornklauselnzu formulieren.Es wird allerdingseine zusatzlicheFreiheit geschaffen: die Regeln durfen Variablenbeinhalten,die durchbeliebige

”Namen“ ersetztwerdendurfen.Eine PROLOG-Regel kannsomit fur

35

eineunendlicheMengevon Regelnstehen,die entstehen,wennmanfur einesolcheVariablebeliebigeWerteeinsetzt.

Zum besserenVerstandnisbetrachtenwir ein kleineskonkretesPROLOG Programmzu Thema”Fami-

lenbeziehungen“ :

1 : vater(adam,bertold).2 : vater(bertold,claus).3 : vater(adam,dieter).4 : bruder(X,Y):-vater(Z,X),vater(Z,Y).5 : opa(X,Y):-vater(X,Z),vater(Z,Y).6 : onkel(X,Y):-vater(Z,Y),bruder(Z,X).

Aussagenderwie vater(adam,claus) oderopa(dieter,adam) werdengelesenals”Adam ist Vater

von Claus“ bzw.”Dieter ist Opa von Adam“ und ubernehmendie Rolle der atomarenFormeln.Sie

konnenentwederwahr oderfalsch sein.

Bei denerstendrei Zeilen desProgrammshandeltessich um Fakten. Die letztendrei Zeilen desPro-grammsstellenRegelndar. JedeRegel reprasentierthierbeigleichzeitigalleRegeln,dieentstehenwennmanX, Y undZ durchbeliebigeNamenersetzt.HierbeimussderselbeBuchstabeinnerhalbeinerRegelimmer durchdenselbenNamenersetztweden.Die Regel opa(X,Y):-vater(X,Z),vater(Z,Y) be-sagtalso,dasswennz.B.vater(adam,bertold) undvater(bertold,claus) bereitsbewiesenwurde,auchdie Aussageopa(adam,claus) gefolgertwerdenkann.

Typischerweisefasstman nun ein solchesPROLOG-Programmals eine Datenbankauf, an die be-stimmt Anfragengestelltwerdenkonnen,welchedie Datenbankversuchtmit JA oderNEIN zu beant-worten.Die SuchederAntwort wird hierbeiuberResolutiondurchgefuhrt. Wir wollen z.B. wissenobonkel(dieter,claus) gilt. In PROLOGSyntaxstellenwir die Anfrage:

?-onkel(dieter,claus).

Prolog geht zum Beantworten dieserFrageungefahr wie folgt vor: Aus Zeile ’6’ erkennt man dassonkel(dieter,claus) nur gefolgertwerdenkann,wennmanein Z findet mit vater(Z,claus) undbruder(Z,dieter). Nunwird festgestellt,dasnur in Zeile ’2’ die Moglichkeit bestehtein geeignetesZzu findenum vater(Z,claus) zu erfullen. EsmussalsogeltenZ=bertold. Nunmehrbleibt zu zeigendassbruder(bertold,claus) ableitbarist. Zeile ’4’ besagt,dassdiesmoglich ist, sofernein (neues)Zgefundenwird, welchesvater(Z,dieter) undauchvater(Z,bertold) erfullt. Die einzigeMoglich-keit hierfur ist (Zeile ’1’ und’3’) durchZ=adam gegeben,welchesdieseForderungauchwirklich erfullt.Die Anfragekannsomitmit JA beantwortetwerden.

Wir werdenunsim viertenTeil derVorlesungnochsehrausfuhrlich mit PROLOG beschaftigen.AlleindasebendiskutierteBeispiel zeigt, dasses dazunotig sein wird, in vernunftiger formalerWeisemitVariablenumzugehen,Aussagenuber Existenzbestimmter

”Namen“ machenzu konnen,unendliche

Mengenvon Regeln zu verwaltenusw. Hiermit beschaftigt sich der zweiteTeil unsererVorlesungdie

”Pradikatenlogik“ , denwir nunmehrbetreten.

36