The Querying Task

Erfüllt ein Modell eine Aussage?

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

• Querying 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.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:

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).

Implementing Resolution

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

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).

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).

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).

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$$