Blackburn and Bos: Representation and Inference of Natural Language

Chapter 4: Propositional Inference

<style>
pre code.bash {
  background: lightyellow;
}
</style>  

Wiederholung Kapitel 1:

The Querying Task

Erfüllt ein Modell eine Aussage?

The Querying Task: Given a model M and a first-order formula \(\phi\) and a variable assignment, is \(\phi\) satisfied in M or not?

• Querrying Task for first-order logic is decidable (Solution: Model Checker)

% satisfy/4
% statisfy(Formula,Model,Assignment,Polarity)

The Consistency Checking Task

Ist eine Aussage konsistent, sprich erfüllbar, sprich in wenigstens einem Modell erfüllt?

• consistency \(\approx\) makes sense
  
• inconsistency \(\approx\) does not make sense

A first-order formula is called satisfiable if it is satisfied in at least one model. A formula that is not satisfiable in any model is called unsatisfiable.

The Consistency Checking Task: Given a first-order formula \(\phi\), is \(\phi\) consistent (that is: satisfiable) or inconsistent (that is: unsatisfiable)?

• Consistency checking for first-order logic is undecidable

The Informativity Checking Task

Ist eine Aussage informativ, sprich nicht trivial, sprich nicht in jedem Modell erfüllt?

• informative = invalid
• uninformative (=trivial) = valid

A valid formula is a formula that is satisfied in all models (of the appropriate vocabulary) given any variable assignment. If \(\phi\) is a valid formula we write \(\models \phi\). A formula that is not valid is called invalid (\(\not\models \phi\)).

• Informativity checking for first-order logic is undecidable

Zusammenfassung

• Die Überprüfung auf Konsistenz und Informativität einer Aussage lässt sich jeweils auf die (Nicht)-Erfüllbarkeit der Aussage zurückführen:

  * eine Aussage ist informativ, wenn es ein Modell gibt, in dem sie nicht erfüllt ist. 
  * eine Aussage ist informativ, wenn ihre Negation erfüllbar ist. 
  * eine Aussage ist konsistent, wenn sie erfüllbar ist.

• Die Erfüllbarkeit einer Aussage ist im Allgemeinen für POL unentscheidbar, für das Fragment ohne Quantifikatoren ist sie aber entscheidbar.

• \(\psi\) ist inkonsistent mit den Aussagen \(\phi_1,\ldots \phi_n\), wenn \[ \phi_1, \ldots \phi_n \models \neg\psi\] gilt.
• \(\psi\) ist uninformativ in Bezug auf die Aussagen \(\phi_1,\ldots \phi_n\), wenn \[ \phi_1, \ldots \phi_n \models \psi\] gilt.
• \(\phi_1, \ldots \phi_n \models \psi\) gilt, wenn \(\phi_1 \wedge \ldots \wedge \phi_n \rightarrow \psi\) eine gültige Aussage ist (also eine Aussage, die in allen Modellen gilt)

• \(\phi_1, \ldots \phi_n \models \psi\) gilt, wenn \(\phi_1 \wedge \ldots \wedge \phi_n \rightarrow \neg\psi\) eine unerfüllbare Aussage ist (also eine Aussage, die in keinem Modell gilt)

4.1 From Models to Proofs

• Informativität und Konsistenz sind semantische Konzepte, die Aussagen über Modelle machen.
• Automatisch lassen sich Aussagen über alle Modelle nicht direkt überprüfen.
• Stattdessen verwenden wir einen beweistheoretischen Ansatz, der rein syntaktisch auf Formeln operiert, um die Gültigkeit einer Aussage zu beweisen.

4.2 Propositional Tableaus

Die Tableau-Methode ist eine Wiederlegungsmethode: Statt zu zeigen, dass eine Formel \(\phi\) gültig ist, zeigen wir, dass die negierte Formel \(\neg \phi\) ungültig ist (also in keinem Modell erfüllbar).

FRAGE: Warum verwenden wir nicht einfach Wahrheitstafeln?

Examples

Im folgenden soll die Gültigkeit von \(p \vee \neg p\) gezeigt werden:

Beispiel 2:

Beispiel 3:

Tableau rules

Procedure

Tableau-provability

Informativity Check

Implementing Tableau Method

Central predicates

tprove(F):-
   (
    closedTableau([[f(F)]]), !,
    write('Theorem.'), nl
   ;  
    write('Not a theorem.'), nl
   ).

closedTableau([]).

closedTableau(OldTableau):-
   expand(OldTableau,TempTableau),
   removeClosedBranches(TempTableau,NewTableau),
   closedTableau(NewTableau).

Expanding tableau

expand([Branch|Tableau],[NewBranch|Tableau]):-
   unaryExpansion(Branch,NewBranch), !.

expand([Branch|Tableau],[NewBranch|Tableau]):-
   conjunctiveExpansion(Branch,NewBranch), !.

expand([Branch|Tableau],[NewBranch1,NewBranch2|Tableau]):-
   disjunctiveExpansion(Branch,NewBranch1,NewBranch2), !.

expand([Branch|Rest],[Branch|Newrest]):-
   expand(Rest,Newrest).
   
unaryExpansion(Branch,[Component|Temp]):-
   unary(SignedFormula,Component),
   removeFirst(SignedFormula,Branch,Temp).

conjunctiveExpansion(Branch,[Comp1,Comp2|Temp]):-
   conjunctive(SignedFormula,Comp1,Comp2),
   removeFirst(SignedFormula,Branch,Temp).

disjunctiveExpansion(Branch,[Comp1|Temp],[Comp2|Temp]):-
   disjunctive(SignedFormula,Comp1,Comp2),
   removeFirst(SignedFormula,Branch,Temp).
   
conjunctive(t(and(X,Y)),t(X),t(Y)).
conjunctive(f(or(X,Y)),f(X),f(Y)).
conjunctive(f(imp(X,Y)),t(X),f(Y)).

disjunctive(f(and(X,Y)),f(X),f(Y)).
disjunctive(t(or(X,Y)),t(X),t(Y)).
disjunctive(t(imp(X,Y)),f(X),t(Y)).

unary(t(not(X)),f(X)).
unary(f(not(X)),t(X)).    

Remove closed branches

removeClosedBranches([],[]).

removeClosedBranches([Branch|Rest],Tableau):-
   closedBranch(Branch), !,
   removeClosedBranches(Rest,Tableau).

removeClosedBranches([Branch|Rest],[Branch|Tableau]):-
   removeClosedBranches(Rest,Tableau).

closedBranch(Branch):-
    memberList(t(X),Branch),
    memberList(f(X),Branch).

Modifizieren sie die Prädikate so, dass ihnen die Regeln und die Ableitungsschritte angezeigt werden (siehe auch Aufgabe 4.3.1).

4.4 Resolution

Terminologie: Wie heißen die ersten beiden Regeln?

Terminologie: Nach Anwendung der obenstehenden Regeln ist die Formel in negation normal form (NNF) (es erscheinen nur noch die Operatoren \(\wedge\) und \(\vee\), Literale und Klammern)

Terminologie: Wie heißen die Gesetze für die ersten beiden und die zweiten beiden Regeln?

Eine Formel ist in set CNF, wenn in keiner Klausel ein Literal zweimal auftritt und keine Klausel zweimal vorkommt. Wenn \(C\) eine Klausel ist, schreiben wir \(set(C)\) für die Klausel in set CNF Form.

Aufgabe: Wandle die folgende Formel in set CNF um:

\[p \rightarrow (p\wedge (q \vee \neg p))\]

Warum kann man die Vereinfachung vornehmen?

Terminologie \(R\) und $R $ heißen complementary pair und die beiden Klauseln complementary clauses

Aufgaben:

1. Zeige mit der Resolutionsmethode, dass \(p\rightarrow (p\vee q)\) gilt.
2. Zeige mit der Resolutionsmethode, dass \(p\rightarrow (q\rightarrow p)\) gilt.
3. Wende die Resolutionsmethode auf \((p\vee q) \rightarrow p\) an.

Implementing Resolution

Formula to SetCNF

% cnf.pl

cnf(Formula,SetCNF):-
   nnf(Formula,NNF),
   nnf2cnf([[NNF]],[],CNF),
   setCnf(CNF,SetCNF).

Formula to NNF

% cnf.pl

nnf(not(and(F1,F2)),or(N1,N2)):- 
   nnf(not(F1),N1), 
   nnf(not(F2),N2).
   
nnf(and(F1,F2),and(N1,N2)):- 
   nnf(F1,N1),
   nnf(F2,N2).
   
nnf(not(or(F1,F2)),and(N1,N2)):-
   nnf(not(F1),N1),
   nnf(not(F2),N2).
   
nnf(or(F1,F2),or(N1,N2)):-
   nnf(F1,N1),
   nnf(F2,N2).

nnf(not(imp(F1,F2)),and(N1,N2)):- 
   nnf(F1,N1),
   nnf(not(F2),N2).
   
nnf(imp(F1,F2),or(N1,N2)):- 
   nnf(not(F1),N1),
   nnf(F2,N2).
   
nnf(not(not(F1)),N1):-
   nnf(F1,N1).
   
nnf(F1,F1):-
   literal(F1).


literal(not(F)):- atomic(F).
literal(F):- atomic(F).

NNF to CNF

% cnf.pl

nnf2cnf([],_,[]).

nnf2cnf([[]|Tcon],Lit,[Lit|NewTcon]):-
   !,
   nnf2cnf(Tcon,[],NewTcon).

nnf2cnf([[and(F1,F2)|Tdis]|Tcon],Lits,Output):-
   !,
   appendLists(Tdis,Lits,Full),
   nnf2cnf([[F1|Full],[F2|Full]|Tcon],[],Output).

nnf2cnf([[or(F1,F2)|Tdis]|Tcon],Lits,Output):-
   !,
   nnf2cnf([[F1,F2|Tdis]|Tcon],Lits,Output).

nnf2cnf([[Lit|Tdis]|Tcon],Lits,Output):-
   nnf2cnf([Tdis|Tcon],[Lit|Lits],Output).

CNF to setCNF

setCnf(Cnf1,Cnf2):-
   setCnf(Cnf1,[],Cnf2).

setCnf([],Cnf1,Cnf2):-
   removeDuplicates(Cnf1,Cnf2).

setCnf([X1|L1],L2,L3):-
   removeDuplicates(X1,X2),
   setCnf(L1,[X2|L2],L3).

Resolution Rule

% propResolution.pl

rprove(Formula):-
   cnf(not(Formula),CNF),
   refute(CNF).

refute(C):-
   memberList([],C).

refute(C):-
   \+ memberList([],C),
   resolveList(C,[],Output),
   unionSets(Output,C,NewC),
   \+ NewC = C, 
   refute(NewC).


resolveList([],Acc,Acc).

resolveList([Clause|List],Acc1,Acc3):-
   resolveClauseList(List,Clause,Acc1,Acc2),
   resolveList(List,Acc2,Acc3).


resolveClauseList([],_,Acc,Acc).

resolveClauseList([H|L],Clause,Acc1,Acc3):-
   resolve(Clause,H,Result), 
   unionSets([Result],Acc1,Acc2),
   resolveClauseList(L,Clause,Acc2,Acc3).

resolveClauseList([H|L],Clause,Acc1,Acc2):-
   \+ resolve(Clause,H,_),
   resolveClauseList(L,Clause,Acc1,Acc2).

resolve(Clause1,Clause2,NewClause):-
   selectFromList(Lit,Clause1,Temp1),
   selectFromList(not(Lit),Clause2,Temp2), 
   unionSets(Temp1,Temp2,NewClause).

resolve(Clause1,Clause2,NewClause):-
   selectFromList(not(Lit),Clause1,Temp1),
   selectFromList(Lit,Clause2,Temp2),
   unionSets(Temp1,Temp2,NewClause).

Theoretical Remarks

Soundness: Ein Beweissystem ist sound, wenn jede Aussage, die beweisbar ist, auch gültig ist.

\[ \text{wenn } \vdash \phi \text{ dann } \models \phi\] Completeness: Ein Beweissystem ist complete, wenn jede Aussage, die gültig ist, auch beweisbar ist.

\[ \text{wenn } \models \phi \text{ dann } \vdash \phi\]