Devcon Web Studio Blog: propositielogica-formele-grondslagen-en-toepassingen-in-de-informatica-1

# Inleiding

Predicaatlogica, ook bekend als eerste-orde logica, is een krachtige uitbreiding van propositielogica die de mogelijkheid biedt om de interne structuur van uitspraken te modelleren en te redeneren over objecten en hun relaties. Terwijl propositielogica beperkt is tot het analyseren van gehele uitspraken met waarheidswaarden (waar of onwaar), laat predicaatlogica toe om te kwantificeren over individuen in een domein en relaties tussen deze individuen te beschrijven. Dit maakt predicaatlogica bijzonder geschikt voor complexe redeneerproblemen in disciplines zoals wiskunde, filosofie en informatica.

In de informatica vormt predicaatlogica de basis voor veel fundamentele concepten en technologieën. Het vermogen om universele en existentiële uitspraken te maken ("voor alle" en "er bestaat") maakt het mogelijk om algemene regels en uitzonderingen te formaliseren, wat essentieel is in domeinen zoals kunstmatige intelligentie, databases, formele verificatie en programmeertalen. Predicaatlogica biedt een formele taal om specificaties van systemen te beschrijven, eigenschappen van algoritmen te bewijzen, en kennis in computersystemen te representeren.

De relevantie van predicaatlogica in de informatica omvat onder meer:

Kunstmatige Intelligentie: Predicaatlogica wordt gebruikt voor kennisrepresentatie en automatisch redeneren in expertsystemen, ontologieën en semantische webtechnologieën.
Databases: Relationele databases vertrouwen op predicaatlogica voor het formuleren en optimaliseren van query's in talen zoals SQL.
Formele Verificatie: Het specificeren en verifiëren van correctheidseigenschappen van software en hardware maakt gebruik van predicaatlogische formules.
Programmeertalen: Geavanceerde typesystemen en contractgebaseerd programmeren gebruiken predicaatlogica om eigenschappen van programma's te formaliseren.
Automatisch Theorembewijs: Systemen zoals Coq en Isabelle bouwen voort op predicaatlogica om wiskundige stellingen en software-eigenschappen te bewijzen.

Dit artikel biedt een grondige behandeling van predicaatlogica, beginnend bij de formele grondslagen en voortbouwend naar praktische toepassingen. We definiëren de syntaxis en semantiek, onderzoeken kwantoren en hun eigenschappen, bespreken bewijstechnieken, en illustreren hoe predicaatlogica wordt toegepast in computationele contexten. Het artikel combineert formele definities met verhelderende voorbeelden en sluit af met oefeningen om het begrip te versterken.

# Formele Grondslagen

# Termen, Predicaten en Kwalificatoren

Predicaatlogica breidt propositielogica uit door uitspraken op te splitsen in objecten (termen) en eigenschappen of relaties (predicaten), en door kwantoren te introduceren om over deze objecten te redeneren.

Definitie 1.1: Een term is een uitdrukking die verwijst naar een object in een domein. Termen kunnen zijn:

Constanten: Symbolen die een specifiek object aanduiden, zoals jan of 5.
Variabelen: Symbolen die een willekeurig object in het domein vertegenwoordigen, zoals x of y.
Functie-uitdrukkingen: Toepassingen van functies op termen, zoals vader(jan) of plus(x, 1).

Definitie 1.2: Een predicaat is een symbool dat een eigenschap of relatie beschrijft over een of meer termen. Een predicaat met n argumenten wordt een n-ary predicaat genoemd. Voorbeelden:

Liefde(x, y): Een binaire predicaat dat uitdrukt dat x van y houdt.
Groter(x, y): Een binaire predicaat voor "x is groter dan y".
Student(x): Een unair predicaat dat aangeeft dat x een student is.

Definitie 1.3: Een kwantor is een operator die een uitspraak maakt over de reikwijdte van variabelen:

Universele kwantor (∀): "Voor alle".
Existentiële kwantor (∃): "Er bestaat".

Voorbeeld: De uitspraak "Alle studenten studeren" kan worden geformaliseerd als ∀x(Student(x) → Studeert(x)), terwijl "Er bestaat een student die gitaar speelt" wordt ∃x(Student(x) ∧ Speelt(x, gitaar)).

# Syntax van Predicaatlogica

De syntax van predicaatlogica definieert hoe welgevormde formules (WFFs) worden geconstrueerd.

Definitie 1.4: De taal van predicaatlogica L wordt inductief gedefinieerd als volgt:

Termen:
- Een constante c ∈ C (verzameling van constanten) is een term.
- Een variabele x ∈ V (verzameling van variabelen) is een term.
- Als f een n-ary functiesymbool is en t₁, ..., tₙ termen zijn, dan is f(t₁, ..., tₙ) een term.
Formules:
- Als P een n-ary predicaat is en t₁, ..., tₙ termen zijn, dan is P(t₁, ..., tₙ) een atomaire formule.
- Als φ en ψ formules zijn, dan zijn ¬φ, (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), en (φ ↔ ψ) formules.
- Als φ een formule is en x een variabele, dan zijn ∀xφ en ∃xφ formules.
- Alleen uitdrukkingen die volgens bovenstaande regels worden gevormd, zijn formules.

Conventie: Haakjes worden vaak weggelaten volgens dezelfde precedentieregels als in propositielogica, met kwantoren die de hoogste prioriteit hebben.

Voorbeelden van welgevormde formules:

Student(jan)
∀x(Student(x) → Studeert(x))
∃y(Liefde(jan, y) ∧ ¬Liefde(y, jan))
∀x∃y(Groter(y, x))

Voorbeeld van een ongeldige formule:

∀xStudent → Studeert(x) (ontbrekende argumenten voor predicaat Student).

# Semantiek van Predicaatlogica

De semantiek van predicaatlogica definieert hoe formules worden geïnterpreteerd en geëvalueerd.

Definitie 1.5: Een interpretatie I bestaat uit:

Een niet-lege verzameling D, het domein van de interpretatie.
Een toewijzing van elke constante c aan een element I(c) ∈ D.
Een toewijzing van elk n-ary functiesymbool f aan een functie I(f): Dⁿ → D.
Een toewijzing van elk n-ary predicaat P aan een relatie I(P) ⊆ Dⁿ.

Definitie 1.6: Een waardetoekenning v is een functie die variabelen toewijst aan elementen in D, v: V → D. Voor een interpretatie I en waardetoekenning v wordt de waarde van een term t, genoteerd als I,v(t), inductief gedefinieerd:

Voor een constante c: I,v(c) = I(c).
Voor een variabele x: I,v(x) = v(x).
Voor een functie-uitdrukking f(t₁, ..., tₙ): I,v(f(t₁, ..., tₙ)) = I(f)(I,v(t₁), ..., I,v(tₙ)).

Definitie 1.7: De waarheidswaarde van een formule φ onder interpretatie I en waardetoekenning v, genoteerd als I,v ⊨ φ, wordt inductief gedefinieerd:

Voor een atomaire formule P(t₁, ..., tₙ): I,v ⊨ P(t₁, ..., tₙ) als (I,v(t₁), ..., I,v(tₙ)) ∈ I(P).
Voor ¬φ: I,v ⊨ ¬φ als I,v ⊭ φ.
Voor φ ∧ ψ: I,v ⊨ φ ∧ ψ als I,v ⊨ φ en I,v ⊨ ψ.
Voor φ ∨ ψ: I,v ⊨ φ ∨ ψ als I,v ⊨ φ of I,v ⊨ ψ.
Voor φ → ψ: I,v ⊨ φ → ψ als I,v ⊭ φ of I,v ⊨ ψ.
Voor φ ↔ ψ: I,v ⊨ φ ↔ ψ als I,v ⊨ φ precies wanneer I,v ⊨ ψ.
Voor ∀xφ: I,v ⊨ ∀xφ als voor elke d ∈ D, I,v[x→d] ⊨ φ, waarbij v[x→d] de waardetoekenning is die x toewijst aan d en andere variabelen ongewijzigd laat.
Voor ∃xφ: I,v ⊨ ∃xφ als er een d ∈ D bestaat zodat I,v[x→d] ⊨ φ.

Definitie 1.8: Een formule φ is waar onder interpretatie I, genoteerd als I ⊨ φ, als I,v ⊨ φ voor alle waardetoekenningen v. Een formule φ is satisfiable als er een interpretatie I en waardetoekenning v bestaat zodat I,v ⊨ φ. Een formule φ is een tautologie als I ⊨ φ voor alle interpretaties I.

Voorbeeld: Beschouw de formule ∀x(Student(x) → Studeert(x)) met:

Domein D = {jan, marie}.
I(Student) = {jan}, I(Studeert) = {jan}. Voor elke v, als I,v(x) = jan, dan I,v ⊨ Student(x) → Studeert(x) (want beide waar); als I,v(x) = marie, dan I,v ⊨ Student(x) → Studeert(x) (want Student(marie) is onwaar). Dus I ⊨ ∀x(Student(x) → Studeert(x)).

# Kwantoren en hun Eigenschappen

# Universele en Existentiële Kwantoren

De universele kwantor (∀) en existentiële kwantor (∃) zijn de kern van predicaatlogica’s expressieve kracht.

Universele kwantor: ∀xφ stelt dat φ waar is voor alle mogelijke waarden van x in het domein. Bijvoorbeeld:

∀x(Groter(x, x) → x = x): Voor elk object x, als x groter is dan zichzelf, dan is x gelijk aan zichzelf.

Existentiële kwantor: ∃xφ stelt dat er minstens één waarde van x in het domein bestaat waarvoor φ waar is. Bijvoorbeeld:

∃x(Student(x) ∧ Speelt(x, gitaar)): Er is een student die gitaar speelt.

# Geneste Kwantoren

Kwantoren kunnen worden genest, wat leidt tot complexere uitspraken. De volgorde van kwantoren is cruciaal.

Voorbeeld:

∀x∃y(Liefde(x, y)): Voor iedereen x bestaat er een y waar x van houdt.
∃y∀x(Liefde(x, y)): Er is een y waar iedereen van houdt.

De eerste formule stelt dat iedereen van iemand houdt, terwijl de tweede stelt dat er een universeel geliefd persoon is. Deze formules zijn niet equivalent.

Definitie 2.1: Een variabele x in een formule φ is vrij als deze niet gebonden is door een kwantor ∀x of ∃x. Een formule zonder vrije variabelen heet een zin.

Voorbeeld:

In Student(x) ∧ ∃y(Liefde(x, y)) is x vrij en y gebonden.
In ∀x(Student(x) → Studeert(x)) zijn geen variabelen vrij (het is een zin).

# De Morgan's Wetten voor Kwantoren

Net als in propositielogica bestaan er equivalenties die negaties over kwantoren verplaatsen.

Stelling 2.2 (De Morgan's Wetten voor Kwantoren):

¬∀xφ ≡ ∃x¬φ
¬∃xφ ≡ ∀x¬φ

Intuïtieve uitleg:

"Niet iedereen studeert" (¬∀x(Studeert(x))) is equivalent aan "Er is iemand die niet studeert" (∃x(¬Studeert(x))).
"Er is niemand die gitaar speelt" (¬∃x(Speelt(x, gitaar))) is equivalent aan "Iedereen speelt geen gitaar" (∀x(¬Speelt(x, gitaar))).

Bewijs (schets): Voor ¬∀xφ: I ⊨ ¬∀xφ als er een d ∈ D bestaat zodat I,v[x→d] ⊭ φ, wat equivalent is aan I ⊨ ∃x¬φ. Het bewijs voor de tweede wet is analoog.

# Logische Equivalentie en Normaalvormen

# Logische Equivalentie in Predicaatlogica

Definitie 3.1: Twee formules φ en ψ zijn logisch equivalent, genoteerd φ ≡ ψ, als voor elke interpretatie I en waardetoekenning v, I,v ⊨ φ precies wanneer I,v ⊨ ψ.

Voorbeelden van equivalenties:

∀x(φ ∧ ψ) ≡ ∀xφ ∧ ∀xψ
∃x(φ ∨ ψ) ≡ ∃xφ ∨ ∃xψ
∀xφ ≡ ∀yφ[x/y] (hernoemen van gebonden variabelen, mits y niet voorkomt in φ).

# Prenex Normaalvorm

Definitie 3.2: Een formule is in prenex normaalvorm als deze de vorm heeft Q₁x₁Q₂x₂...Qₙxₙψ, waarbij elke Qᵢ een kwantor is (∀ of ∃) en ψ geen kwantoren bevat.

Procedure voor conversie naar prenex normaalvorm:

Elimineer implicaties en equivalenties (zoals in propositielogica).
Verplaats negaties naar binnen met De Morgan's wetten voor kwantoren.
Trek kwantoren naar buiten door equivalenties zoals:
- (∀xφ ∧ ψ) ≡ ∀x(φ ∧ ψ) (als x niet vrij is in ψ)
- (∃xφ ∨ ψ) ≡ ∃x(φ ∨ ψ) (als x niet vrij is in ψ)
Hernoem variabelen indien nodig om botsingen te vermijden.

Voorbeeld: Converteer ∀x(Student(x) → ∃y(Liefde(x, y))) naar prenex normaalvorm.

∀x(Student(x) → ∃y(Liefde(x, y)))
≡ ∀x(¬Student(x) ∨ ∃y(Liefde(x, y))) [Implicatie-eliminatie]
≡ ∀x∃y(¬Student(x) ∨ Liefde(x, y)) [Kwantor naar buiten]

De formule is nu in prenex normaalvorm.

# Skolem-vorm

Definitie 3.3: Een formule in prenex normaalvorm is in Skolem-vorm als alle existentiële kwantoren zijn geëlimineerd door Skolem-functies.

Procedure voor Skolemisatie:

Breng de formule in prenex normaalvorm.
Voor elke existentiële kwantor ∃x die volgt op universele kwantoren ∀y₁, ..., ∀yₙ, vervang x door een nieuwe functie f(y₁, ..., yₙ) en verwijder ∃x.

Voorbeeld: Skolemizeer ∀x∃y(Liefde(x, y)).

Stap 1: De formule is al in prenex normaalvorm.
Stap 2: Vervang ∃y door een functie f(x), wat geeft: ∀x(Liefde(x, f(x))).

De Skolem-vorm stelt dat voor elk x, x houdt van f(x), waarbij f een functie is die de "geliefde" van x kiest.

# Bewijstechnieken

# Natuurlijke Deductie voor Predicaatlogica

Natuurlijke deductie voor predicaatlogica breidt het systeem van propositielogica uit met regels voor kwantoren.

Belangrijke regels:

∀-introductie (∀I):

[x willekeurig] ... φ ∀xφ

Voorwaarde: x mag geen aannames hebben die x specifiek maken.

∀-eliminatie (∀E):

∀xφ φ[t/x]

Waarbij t een term is die x vervangt.

∃-introductie (∃I):

φ[t/x] ∃xφ
∃-eliminatie (∃E):

∃xφ [φ[c/x]] ... ψ ψ

Voorwaarde: c is een nieuwe constante die alleen in de subafleiding wordt gebruikt.

Voorbeeld: Bewijs ∀x(P(x) → Q(x)), ∃xP(x) ⊢ ∃xQ(x):

∀x(P(x) → Q(x)) [Premisse]

∃xP(x) [Premisse]

P(c) [∃E, 2, aanname voor c]

P(c) → Q(c) [∀E, 1]

Q(c) [MP, 4, 3]

∃xQ(x) [∃I, 5]

∃xQ(x) [∃E, 2, 3-6]

# Resolutie

Resolutie is een krachtige bewijstechniek voor predicaatlogica, vooral in geautomatiseerde systemen.

Procedure:

Converteer formules naar clausulevorm (conjunctie van disjuncties van literalen) via Skolemisatie en prenex normaalvorm.
Pas resolutie toe: Voor clausules C₁ = {L, ...} en C₂ = {¬L, ...}, leid de clausule (C₁ \ {L}) ∪ (C₂ \ {¬L}) af.
Herhaal tot een lege clausule (contradictie) wordt afgeleid of geen nieuwe clausules mogelijk zijn.

Voorbeeld: Bewijs dat ∀x(P(x) → Q(x)), ∃xP(x) ⊢ ∃xQ(x) via resolutie:

Converteer naar clausulevorm:
- ∀x(¬P(x) ∨ Q(x)) → {¬P(x), Q(x)}
- ∃xP(x) → {P(a)} (na Skolemisatie)
- Doel: ∃xQ(x) → {¬Q(x)} (negatie voor contradictie)
Resolutie:
1. {¬P(x), Q(x)} en {¬Q(x)} → {¬P(x)}
2. {¬P(x)} en {P(a)} → {} (lege clausule, contradictie)
Conclusie: Het doel volgt.

# Bewijs door Contradictie

Procedure:

Neem aan dat de te bewijzen conclusie onwaar is.
Leid een contradictie af (bijvoorbeeld φ ∧ ¬φ).
Concludeer dat de aanname onwaar is, dus de conclusie waar.

Voorbeeld: Bewijs ∀x(P(x) → Q(x)) ⊢ ∀x(¬Q(x) → ¬P(x)):

∀x(P(x) → Q(x)) [Premisse]

¬∀x(¬Q(x) → ¬P(x)) [Aanname voor contradictie]

∃x¬(¬Q(x) → ¬P(x)) [De Morgan, 2]

¬(¬Q(c) → ¬P(c)) [∃E, 3]

¬Q(c) ∧ ¬¬P(c) [¬(A → B) ≡ A ∧ ¬B]

¬Q(c) [∧E, 5]

P(c) [Dubbele negatie, 5]

P(c) → Q(c) [∀E, 1]

Q(c) [MP, 8, 7]

Q(c) ∧ ¬Q(c) [∧I, 9, 6]

∀x(¬Q(x) → ¬P(x)) [RAA, 2-10]

# Toepassingen in de Informatica

# Kennisrepresentatie in Kunstmatige Intelligentie

Predicaatlogica wordt veel gebruikt in AI voor kennisrepresentatie en redeneren.

Voorbeeld: In een expertsysteem voor een universiteit:

Feiten: Student(jan), Vak(logica), Volgt(jan, logica).
Regel: ∀x∀y(Student(x) ∧ Vak(y) ∧ Volgt(x, y) → Studeert(x)).
Query: Studeert(jan)? (bewijsbaar via resolutie of deductie).

Toepassingen:

Semantisch web: RDF en OWL gebruiken predicaatlogica om relaties tussen entiteiten te modelleren.
Plannen: Planningsproblemen worden geformuleerd als predicaatlogische formules.
Natuurlijke taalverwerking: Betekenisrepresentaties van zinnen worden vaak in predicaatlogica uitgedrukt.

# Database Query's en Relationele Algebra

Relationele databases gebruiken predicaatlogica als basis voor query-talen zoals SQL.

Voorbeeld: Beschouw een tabel Studenten(id, naam, vak):

SQL-query: SELECT naam FROM Studenten WHERE vak = 'Logica'
Predicaatlogica: ∃id(Studenten(id, naam, logica))

Relationele algebra:

Selectie ( σ): Equivalent aan existentiële kwantificatie.
Join (⋈): Combineert predicaten over meerdere relaties.
Projectie (π): Selecteert specifieke termen uit een predicaat.

Optimalisatie: Logische equivalenties worden gebruikt om query’s efficiënter te maken, zoals het herschrijven van geneste kwantoren.

# Formele Specificatie en Verificatie

Predicaatlogica wordt gebruikt om systeemgedrag te specificeren en te verifiëren.

Voorbeeld: Een specificatie voor een besturingssysteem:

Predicaat: Toegang(user, resource) (gebruiker heeft toegang tot resource).
Regel: ∀u∀r(Admin(u) ∨ Eigenaar(u, r) → Toegang(u, r)).
Verificatie: Bewijs dat ¬(Toegang(u, r) ∧ ¬Admin(u) ∧ ¬Eigenaar(u, r)) altijd waar is.

Tools: Systemen zoals TLA+ en Alloy gebruiken predicaatlogica voor specificatie en model checking.

# Type-systemen in Programmeertalen

Geavanceerde typesystemen in talen zoals Haskell en Coq gebruiken predicaatlogica.

Voorbeeld: In Coq:


Theorem plus_comm: forall n m: nat, n + m = m + n.

Dit komt overeen met een predicaatlogische uitspraak: ∀n∀m(Plus(n, m, s)  Plus(m, n, s)).
Afhankelijke types: Predicaten worden gebruikt om eigenschappen van waarden te specificeren, zoals Vector(n, T) voor lijsten van lengte n.
Automatisch Theorembewijs
Automatische theorembewijzers zoals Z3 en Vampire gebruiken predicaatlogica om stellingen te bewijzen.
Toepassingen:
Software-verificatie: Bewijzen dat een programma aan zijn specificaties voldoet.

Wiskundige bewijzen: Assisteren bij het bewijzen van complexe stellingen.

Synthese: Genereren van programma’s uit predicaatlogische specificaties.

Voorbeeld: Z3 kan de satisfiability van ∀x(P(x) → ∃yQ(x, y)) ∧ ∃xP(x) → ∃x∃yQ(x, y) controleren.
Geavanceerde Concepten
Herbrand-semantiek
Definitie 6.1: De Herbrand-semantiek beperkt interpretaties tot het Herbrand-universum, de verzameling van alle termen die kunnen worden gevormd uit constanten en functies in de taal.
Toepassing: Herbrand-semantiek vereenvoudigt het testen van satisfiability door het domein te beperken tot een telbare verzameling.
Voorbeeld: Voor de formule ∀xP(x) → ∃yP(y) met constante a:
Herbrand-universum: {a, f(a), f(f(a)), ...}.

Controleer satisfiability door substitutie van deze termen.

Onbeslisbaarheid in Predicaatlogica
Stelling 6.2 (Church-Turing): Het satisfiability-probleem voor predicaatlogica is onbeslisbaar; er bestaat geen algoritme dat voor elke formule in eindige tijd bepaalt of deze satisfiable is.
Gevolg: In tegenstelling tot propositielogica (waar SAT NP-compleet is), vereist predicaatlogica vaak heuristische of semi-automatische methoden.
Relatie met Hogere-orde Logica
Hogere-orde logica breidt predicaatlogica uit door kwantificatie over predicaten en functies toe te staan.
Voorbeeld:
Eerste-orde: ∀xP(x).

Hogere-orde: ∀P∃xP(x) (kwantificeert over predicaat P).

Toepassing: Hogere-orde logica wordt gebruikt in systemen zoals Coq voor geavanceerde bewijzen, maar is computationeel complexer.
Oefeningen
Oefening 1: Syntaxis en Semantiek
Geef een interpretatie en waardetoekenning die de volgende formules waar of onwaar maakt:
a) ∀x(P(x) → Q(x))
b) ∃x(P(x) ∧ ¬Q(x))
c) ∀x∃y(R(x, y))
d) ∃y∀x(R(x, y))
e) ∀x(P(x)  ¬P(x))
Oefening 2: Logische Equivalentie
Bewijs of weerleg de volgende equivalenties:
a) ∀x(P(x) ∧ Q(x)) ≡ ∀xP(x) ∧ ∀xQ(x)
b) ∃x(P(x) → Q(x)) ≡ ∀xP(x) → ∃xQ(x)
c) ¬∀xP(x) ≡ ∃x¬P(x)
d) ∀x∃yR(x, y) ≡ ∃y∀xR(x, y)
e) ∀x(P(x) ∨ Q) ≡ ∀xP(x) ∨ Q (waarbij Q geen x bevat)
Oefening 3: Normaalvormen
Converteer de volgende formules naar prenex normaalvorm en vervolgens naar Skolem-vorm:
a) ∀x(P(x) → ∃yQ(x, y))
b) ∃x(P(x) ∧ ∀yR(x, y))
c) ¬∃x(P(x) → Q(x))
d) ∀x∃y(P(x, y)  Q(y))
e) (∀xP(x) ∨ ∃yQ(y))
Oefening 4: Bewijzen
Gebruik natuurlijke deductie of resolutie om de volgende afleidingen te bewijzen:
a) ∀x(P(x) → Q(x)), ∃xP(x) ⊢ ∃xQ(x)
b) ∀x(P(x) → Q(x)) ⊢ ∀x(¬Q(x) → ¬P(x))
c) ∀x∀y(R(x, y) → R(y, x)) ⊢ ∀xR(x, x)
d) ∃x∀yR(x, y) ⊢ ∀y∃xR(x, y)
e) ∀x(P(x) → Q(x)), ∀x(Q(x) → R(x)) ⊢ ∀x(P(x) → R(x))
Oefening 5: Toepassingen
a) Formuleer een kennisbasis in predicaatlogica voor een eenvoudig familiesysteem (bijv. ouder-kind relaties) en bewijs een query zoals "Iedereen heeft een ouder".
b) Schrijf een SQL-query die overeenkomt met de predicaatlogische formule ∃x(Student(x) ∧ Volgt(x, logica)) en leg de relatie uit.
c) Specificeer een eenvoudige eigenschap van een software-systeem (bijv. "Geen twee gebruikers hebben dezelfde ID") in predicaatlogica en beschrijf hoe je dit zou verifiëren.
d) Definieer een afhankelijk type in een programmeertaal zoals Coq dat een lijst met een specifieke lengte garandeert.
e) Gebruik een theorembewijzer zoals Z3 om te controleren of ∀x∃y(P(x, y) ∧ Q(y)) → ∃y∀x(P(x, y) → Q(y)) satisfiable is.
Verder Lezen
Boeken:

Logic in Computer Science door Michael Huth en Mark Ryan.

Mathematical Logic door Herbert B. Enderton.

Automated Theorem Proving door Larry Wos en Gail W. Pieper.

Handbook of Automated Reasoning door Alan Robinson en Andrei Voronkov.

Online Bronnen:

Stanford Encyclopedia of Philosophy: First-Order Logic.

MIT OpenCourseWare: Logic and Proofs.

Coursera: Logic for Computer Science.

Tools:

Theorembewijzers: Z3, Vampire, Coq, Isabelle.

Model Checkers: Alloy, TLA+.

Database-systemen: PostgreSQL, MySQL (voor SQL en predicaatlogica).

Artikelen:

Church, A. (1936). A Note on the Entscheidungsproblem.

Robinson, J. A. (1965). A Machine-Oriented Logic Based on the Resolution Principle.

Fitting, M. (1996). First-Order Logic and Automated Theorem Proving.

Gemeenschappen:

Stack Exchange: Computer Science en Mathematics.

Reddit: r/logic, r/compsci.

Referenties
Huth, M., & Ryan, M. (2004). Logic in Computer Science. Cambridge University Press.

Enderton, H. B. (2001). A Mathematical Introduction to Logic. Academic Press.

Wos, L., & Pieper, G. W. (2000). Automated Theorem Proving. Springer.

Robinson, J. A. (1965). A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM, 12(1), 23–41.

Church, A. (1936). A Note on the Entscheidungsproblem. Journal of Symbolic Logic, 1(1), 40–41 .

Fitting, M. (1996). First-Order Logic and Automated Theorem Proving. Springer.

Stanford Encyclopedia of Philosophy. (2023). First-Order Logic. https://plato.stanford.edu/entries/logic-firstorder/

Robinson, A., & Voronkov, A. (Eds.). (2001). Handbook of Automated Reasoning. Elsevier.

Propositielogica: Formele Grondslagen en Toepassingen in de Informatica