Övning 1: Använd resolution för att bevisa: {P → Q, Q → R, P, ¬R} ⊢ ⊥

Klausuler: {¬P ∨ Q}, {¬Q ∨ R}, {P}, {¬R} Resolera {P} och {¬P ∨ Q}: få {Q} Resolera {Q} och {¬Q ∨ R}: få {R} Resolera {R} och {¬R}: få □ Svar: Motsägelse härledas genom systematisk resolution

Avancerad

Automatisk bevisföring

Resolution, tableauxmetoden och automatiserade bevisverktyg.

resolution tableaux CNF unifiering SAT-lösare

Tänk dig att du kunde få en dator att bevisa matematiska satser åt dig, eller kontrollera om dina egna bevis är korrekta. Det är precis vad automatisk bevisföring handlar om! Medan människor är kreativa och intuituiva när de konstruerar bevis, är datorer systematiska och uttömmande. Genom algoritmer som resolution och tableaux kan datorer automatiskt söka igenom logiska möjligheter för att hitta bevis - eller bevisa att inget bevis finns.

Fördjupning

Automatisk bevisföring (automated theorem proving) använder algoritmer för att mekaniskt konstruera eller verifiera logiska bevis. Huvudmetoder inkluderar resolution (för klausuler), tableaux-metoden (systematisk sökning) och SAT-lösare (satisfiabilitet). Modern utveckling inkluderar SMT-lösare (Satisfiability Modulo Theories) som kombinerar propositionslogik med specifika teorier. Tillämpningar sträcker sig från programverifiering till matematisk forskning.

Resolution

Resolution är en refutationsmetod som arbetar med formler i klausulform (disjunktioner av literaler).

Resolutionsregeln

Från klausuler C₁ ∨ P och C₂ ∨ ¬P

Härleda C₁ ∨ C₂ (resolventen)

P kallas resolved literal

Målet är att härleda den tomma klausulen □ (motsägelse)

Resolutionsbevis

Bevisa: P ∨ Q, ¬P ∨ R, ¬Q ∨ ¬R ⊢ ⊥

1. P ∨ Q (given)

2. ¬P ∨ R (given)

3. ¬Q ∨ ¬R (given)

4. Q ∨ R (från 1,2 resolera P)

5. ¬Q (från 3,4 resolera R)

6. Q (från 1,5 resolera P)

7. □ (från 5,6 resolera Q)

Tableaux-metoden

Tableaux-metoden bygger systematiskt ett träd av alla möjliga sanningsfördelningar för att testa satisfiabilitet.

Tableau-regler

α-regler: konjunktiva formler delas upp

β-regler: disjunktiva formler skapar förgreningar

En gren stängs om den innehåller P och ¬P

Tableaux är stängd om alla grenar är stängda

SAT-lösare

SAT-lösare avgör om booleska formler i CNF har satisfierande tilldelningar.

DPLL-algoritmen

Unit propagation: tillskriva värden till ensamstående literaler

Pure literal elimination: eliminera rena literaler

Backtracking: prova olika tilldelningar systematiskt

Moderna förbättringar: CDCL, clause learning

Vanliga misstag

❌ Fel klausulomvandling

Omvandling till CNF måste bevaras ekvivalens eller satisfiabilitet

Exempel: Tseitin-transformation för att undvika exponentiell explosion

Tillämpningar

Programverifiering

Verifiera att program uppfyller specifikationer

Exempel: Bounded model checking för att hitta buggar

Hårdvaruverifiering

Kontrollera att kretsar fungerar korrekt

Exempel: Formell verifiering av processorkärnor

Övningar

1 Medel

Använd resolution för att bevisa: {P → Q, Q → R, P, ¬R} ⊢ ⊥

Tips

Omvandla först till klausulform

Visa facit

Klausuler: {¬P ∨ Q}, {¬Q ∨ R}, {P}, {¬R}
Resolera {P} och {¬P ∨ Q}: få {Q}
Resolera {Q} och {¬Q ∨ R}: få {R}
Resolera {R} och {¬R}: få □

Svar: Motsägelse härledas genom systematisk resolution

Sammanfattning

Automatisk bevisföring använder algoritmer som resolution, tableaux och SAT-lösare för att mekaniskt konstruera bevis. Resolution arbetar med klausuler och refutation. Tableaux bygger systematiskt träd av möjligheter. SAT-lösare är optimerade för booleska satisfiabilitetsproblem. Modern utveckling fokuserar på SMT-lösare som kombinerar olika teorier. Tillämpningar inkluderar program- och hårdvaruverifiering.