First-Order Inference

Wiederholung: Propositional Inference
Free Variable Tableaux

FOL Resolution

Implementing FOL Resolution

Theorem Provers and Model Builders

Off-the-Shelf Theorem Provers
Off-the-Shelf Model Builder

First-Order Inference

Wiederholung: Propositional Inference

Da die Aussagenlogik entscheidbar ist, ist es möglich einen Theorem Prover zu bauen, der für jede Formel entscheidet, ob sie gültig ist.

Ein solcher Beweiser ist jedoch nie effizient, da das Problem NP-Vollständig ist.

Beispiel: Schubfachprinzip

/*------------------------------------------------------------------------
     Pigeonehole principle with 3 pigeons and 2 pigeonholes. 
------------------------------------------------------------------------*/

formula(imp(and(and(or(p11,p12),or(p21,p22)),or(p31,p32)),
            or(or(or(or(or(and(p11,p21),and(p11,p31)),and(p21,p31)),
               and(p12,p22)),and(p12,p32)),and(p22,p32))), 'Theorem').

pijTaube i in Loch j
$A \rightarrow B$ ; A: jede Taube ist in einem Loch; B: in einem Loch sitzt mehr als eine Taube.

Wenn $\sigma= \{x/a,y/g(b)\}$ was ist dann

$g(x)\sigma$ ?
$y\sigma$ ?
$b\sigma$ ?
$z\sigma$ ?

$\sigma_x$ ist die folgende Substitution: $x\sigma_x = x$ und $v\sigma_x=v\sigma$ für alle $v\neq x$ .

Wenn $\sigma= \{x/a,y/g(b)\}$ was ist dann

$[\forall y \exists x ((P(y) \wedge Q(x,y) \rightarrow P(x))]\sigma$ ?

disagreement pair: w and k(u,v)

Ein “disagreement pair” $(d_1,d_2)$ heißt “simple”, genau dann wenn der Ausdruck $d_1$ oder $d_2$ (oder beide) eine Variable ist, die nicht in dem anderen Ausdruck vorkommt.

Term Unification:

input terms t1 and t2
let s:={}
while t1s \= t2s
    choose a disagreement pair (d1,d2) for t1s, t2s
    if (d1,d2) is not simple then
         write t1 and t2 are not unifiable and HALT
else
    let s := s U r, where r is the relevant repair
endif
endwhile

The algorithm always terminates and if it outputs a substitution, it outputs an idempotent substitution ( $\sigma\sigma=\sigma$ ) that leads to the mgu of t1 and t2.

Vorsicht, gewöhnliche Prolog-Unifikation verzichtet auf den occurs-check. Es gibt aber das eingebaute unify_with_occurs_check/2-Prädikat, das eine Unifikation mit occurs-check durchführt.

Frage: Warum müssen die Substitutionen idempotent sein?

Free Variable Tableaux

Beispiel für die Wichtigkeit der Skolem-Terme als Funktionsterme über den freien Variablen: $\exists y(\neg R(x,y)\wedge R(x,x))$ Die Formel enthält die freie Variable $x$ , daher muss die existenzgebundene Variable $y$ durch den Skolemterm $s(y)$ substituiert werden: $\neg R(x,s(x))\wedge R(x,x)$ Nur so wird sichergestellt, dass $x$ und $y$ nicht unifiziert werden können.

Hätte man $x$ durch eine einfache Skolemkonstante $s$ substituiert, dann könnte man später $y$ ebenfalls durch $s$ substituieren und käme dann zur nicht erfüllbaren Formel $\neg R(s,s)\wedge R(s,s).$

Der folgende Code ist in freeVarTabl.pl. Lediglich die Reihenfolge der Prädikate wurde verändert:


/*========================================================================
   Try to create a tableau expansion for f(X) that is closed allowing 
   Qdepth applications of the universal rule.
========================================================================*/

tprove(X,Qdepth):-
   notatedFormula(NotatedFormula,[],f(X)),
   closedTableau([[NotatedFormula]],Qdepth).

/*========================================================================
   Notate the free variables of a formula
========================================================================*/

notatedFormula(n(Free,Formula),Free,Formula).

Der Zähler Qdepth kontrolliert, wie oft eine universal rule angewandt werden darf. Ein solcher Zähler ist notwendig, um den kontrollierten Abbruch zu erzwingen, da die Prädikatenlogik nicht entscheidbar ist. Bei einem Abbruch wissen wir aber nicht, ob kein Beweis für die Gültigkeit einer Formel existiert, oder ob wir nur noch keinen gefunden haben.

Für jede Formel wird explizit die Liste der freien Variablen angegeben (notatedFormula). Statt mit einer Formel wie love(X,Y) arbeiten wir mit der notated Formel n([X,Y],love(X,Y)).

Der folgende Code unterscheidet sich kaum von der Tableau-Implementierung für die Aussagenlogik:

/*========================================================================
   Expand Tableau until it is closed, allowing Qdepth 
   applications of the universal rule.
========================================================================*/

closedTableau([],_Q):- !.

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


/*========================================================================
   Remove all closed branches
========================================================================*/

removeClosedBranches([],[]).

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

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


/*========================================================================
   Check whether a branch is closed
========================================================================*/

closedBranch(Branch):-
   memberList(n(_,t(X)),Branch),
   memberList(n(_,f(Y)),Branch),
   basicFormula(X), 
   basicFormula(Y),
   unify_with_occurs_check(X,Y).

basicFormula/1 ist in comsemPredicates.pl definiert und überprüft, ob eine Formel ein Basisausdruck der Form p(t1,...,tn) ist, wobei p keine logische Konstante ist und alle ti simple Terme sind. Teste: ?- basicFormula(imp(a,b)), ?- basicFormula(love(a,X)), ?- basicFormula(X), ?- basicFormula(love(a,father(X))).

Die folgenden Zeilen sind wieder völlig analog zu der Implementierung für die Aussagenlogik:

/*========================================================================
   Newtableau with Q-depth NewQdepth is the result of applying  
   a tableau expansion rule to Oldtableau with a Q-depth of OldQdepth.
========================================================================*/

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

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

expand([Branch|Tableau],QD,[NewBranch|Tableau],QD):-
   existentialExpansion(Branch,NewBranch).

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


% da universalExpansions mehrfach auf dieselbe Formel angewandt werden kann,
% schieben wir die Formeln immer wieder nach hinten im Tableau 
% (sonst droht Endlosschleife):
expand([Branch|Tableau],OldQD,NewTableau,NewQD):-
   universalExpansion(Branch,OldQD,NewBranch,NewQD),
   appendLists(Tableau,[NewBranch],NewTableau).

expand([Branch|Rest],OldQD,[Branch|Newrest],NewQD):-
   expand(Rest,OldQD,Newrest,NewQD).


/*========================================================================
   Take Branch as input, and return NewBranches if a tableau rule
   allows unary expansion.
========================================================================*/

unaryExpansion(Branch,[NotatedComponent|Temp]) :-
   unary(SignedFormula,Component),
   notatedFormula(NotatedFormula,Free,SignedFormula),
   removeFirst(NotatedFormula,Branch,Temp),
   notatedFormula(NotatedComponent,Free,Component).


/*========================================================================
   Take Branch as input, and return the NewBranch if a tableau rule 
   allows conjunctive expansion. 
========================================================================*/

conjunctiveExpansion(Branch,[NotatedComp1,NotatedComp2|Temp]):-
   conjunctive(SignedFormula,Comp1,Comp2),
   notatedFormula(NotatedFormula,Free,SignedFormula),
   removeFirst(NotatedFormula,Branch,Temp),
   notatedFormula(NotatedComp1,Free,Comp1),
   notatedFormula(NotatedComp2,Free,Comp2).


/*========================================================================
   Take Branch as input, and return the NewBranch1 and NewBranch2 
   if a tableau rule allows disjunctive expansion. 
========================================================================*/

disjunctiveExpansion(Branch,[NotComp1|Temp],[NotComp2|Temp]):-
   disjunctive(SignedFormula,Comp1,Comp2),
   notatedFormula(NotatedFormula,Free,SignedFormula),
   removeFirst(NotatedFormula,Branch,Temp),
   notatedFormula(NotComp1,Free,Comp1),
   notatedFormula(NotComp2,Free,Comp2).


/*========================================================================
   Take Branch as input, and return the NewBranch if a tableau rule 
   allows existential expansion.
========================================================================*/

existentialExpansion(Branch,[NotatedInstance|Temp]):-
   notatedFormula(NotatedFormula,Free,SignedFormula),
   existential(SignedFormula),
   removeFirst(NotatedFormula,Branch,Temp),
   skolemFunction(Free,Term),
   instance(SignedFormula,Term,Instance),
   notatedFormula(NotatedInstance,Free,Instance).

Das Prädikat existentialExpansion/2 greift auf das Prädikat skolemFunction/2 zu, das einen neuen Skolemterm zu einer liste von freien Variablen generiert:

/*========================================================================
   VarList is a list of free variables, and SkolemTerm is a previously 
   unused Skolem function symbol fun(N) applied to those free variables.
========================================================================*/
% Teste mit '?- freeVarTabl:skolemFunction([X,Y,Z],S)'

skolemFunction(VarList,SkolemTerm):-
   newFunctionCounter(N),
   compose(SkolemTerm,fun,[N|VarList]).

Weiter geht es mit der universalExpansion. Hier wird bei jedem Aufruf der Zähler QDepth um eins runtergesetzt.

/*========================================================================
   Take Branch and OldQD as input, and return the NewBranch and 
   NewQDepthif a tableau rule allow universal expansion.
========================================================================*/

universalExpansion(Branch,OldQD,NewBranch,NewQD):-
   OldQD > 0, 
   NewQD is OldQD - 1,
   memberList(NotatedFormula,Branch),
   notatedFormula(NotatedFormula,Free,SignedFormula),
   universal(SignedFormula),
   removeFirst(NotatedFormula,Branch,Temp),
   instance(SignedFormula,V,Instance),
   notatedFormula(NotatedInstance,[V|Free],Instance),
   appendLists([NotatedInstance|Temp],[NotatedFormula],NewBranch).

Das Prädikat universalExpansion/2 ruft das Prädikat instance/3 auf (substitute/4 ist in comsemPred.pl` definiert):


/*========================================================================
   Remove quantifier from signed quantified formula, and replacing all
   free occurrences of the quantified variable by occurrences of Term.
========================================================================*/
% ?- freeVarTabl:instance(t(all(X,love(X,vincent))),Y,F).

instance(t(all(X,F)),Term,t(NewF)):- substitute(Term,X,F,NewF).
instance(f(some(X,F)),Term,f(NewF)):- substitute(Term,X,F,NewF).
instance(t(some(X,F)),Term,t(NewF)):- substitute(Term,X,F,NewF).
instance(f(all(X,F)),Term,f(NewF)):- substitute(Term,X,F,NewF).

Der Rest ist analog zur Implementierung der Aussagenlogik:

/*========================================================================
   Decompose conjunctive signed formula
========================================================================*/

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


/*========================================================================
   Decompose disjunctive signed formula
========================================================================*/

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


/*========================================================================
   Decompose unary signed formula
========================================================================*/

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


/*========================================================================
   Universal Signed Formulas
========================================================================*/

universal(t(all(_,_))).
universal(f(some(_,_))).


/*========================================================================
   Existential Signed Formulas
========================================================================*/

existential(t(some(_,_))).
existential(f(all(_,_))).

FOL Resolution

FOL Resolution (Grundidee)

Umwandlung der Formel in CNF (Clause Normal Form)

Umwandlung in NNF (Negation Normal Form), d.h. es erscheinen nur noch die Operatoren ∧ und ∨, die Quantoren, Literale und Klammern.
Eliminiere die Existenzquantoren durch Skolemisierung.
Lösche alle Allquantoren.
Wandle die resultierende quantorenfreie Formel in (set) conjunctive normal form um.

Hinweise

Bei der Umwandlung in NNF wenden wir folgende Regeln an, um die Negation nach innen zu schieben: $\neg \forall x P(x)$ wird zu $\exists x \neg P(x)$ und $\neg \exists x P(x)$ wird zu $\forall x \neg P(x)$ .
Bei der Skolemisierung müssen wir einen Fall besonders betrachten: Existenzquantoren im Skopus von Allquantoren.

Ist ein Existenzquantor im Skopus eines Allquantors, setzen wir statt Skolemkonstanten komplexe Skolemterme (sprich Skolemfunktionen) ein. Bsp.: $\forall x \exists y R(x,y)$ wird skolemisiert zu $\forall x R(x,s(x))$ . Der komplexe Skolemterm drückt die Abhängigkeit der existenzgebundenen Variablen von der allgebundenen aus. $s(x)$ kann also als Funktion betrachtet werden, die jedem Element des Models ein Element zuordnet, zu dem es in der Relation $R$ steht.

Beispiel: Bringe $(\forall x B(x) \wedge \exists y A(y,x)) \rightarrow \exists z \forall x \exists y C(x,z) \vee B(z,y)$ in setCNF

Wir sorgen also per $\alpha$ -Konversion zunächst dafür, dass die Variablenmengen in den beiden Klauseln disjunkt sind.

Non-redundant Factors:

Zur Erinnerung in PL Resolution haben wir mit Mengen-Klauseln gearbeitet $[[p],[\neg p]]$ statt $[[p,p],[\neg p,\neg p]]$ .
In POL-Resolution müssen wir mit nichtredundanten Faktoren arbeiten.
Zwei Formeln in einer Klausel sind redundant, wenn sie unifizierbar sind.

Beispiel: Seien $w,x,y,z$ Variablen und $a,b,c$ Konstanten. Die Klausel $[P(a),P(x),R(y,b),R(z,x),\neg Q(w),\neg Q(f(z))]$ kann reduziert werden zu

$[P(a),R(y,b),R(z,a),\neg Q(f(z))]$ (unifiziere $P(a)$ und $P(x)$ und anschließend $\neg Q(w)$ und $\neg Q(f(z))$ ).
oder zu $[P(a),P(b),R(y,b),\neg Q(f(y))]$ (unifiziere $R(y,b)$ und $R(z,x)$ und anschließend $\neg Q(w)$ und $\neg Q(f(y))$ ).

Wir müssen jeweils alle nichtredundanten Faktoren einer Klausel behalten, da wir sonst möglicherweise keinen Beweis finden, obwohl es einen gäbe.

Implementing FOL Resolution

FOL in CNF umwandeln:

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

Abweichungen zur Aussagenlogik (nnf)

nnf(not(all(X,F)),some(X,N)):-
   nnf(not(F),N).

nnf(all(X,F),all(X,N)):-
   nnf(F,N).

nnf(not(some(X,F)),all(X,N)):-
   nnf(not(F),N).

nnf(some(X,F),some(X,N)):-
   nnf(F,N).

Resolution

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

Abweichungen und Erweiterungen

/*========================================================================
   Resolve two clauses
========================================================================*/

resolve(Clause1,Clause2,NewClause):-
   selectFromList(Lit1,Clause1,Temp1),
   selectFromList(not(Lit2),Clause2,Temp2), 
   unify_with_occurs_check(Lit1,Lit2),
   unionSets(Temp1,Temp2,NewClause).

resolve(Clause1,Clause2,NewClause):-
   selectFromList(not(Lit1),Clause1,Temp1),
   selectFromList(Lit2,Clause2,Temp2),
   unify_with_occurs_check(Lit1,Lit2),
   unionSets(Temp1,Temp2,NewClause).

/*========================================================================
   Compute Non-Redundant Factors for a list of clauses
========================================================================*/

nonRedundantFactors([],[]).

nonRedundantFactors([C1|L1],L4):-
   findall(C2,nonRedFact(C1,C2),L3),
   nonRedundantFactors(L1,L2),
   appendLists(L3,L2,L4).


/*========================================================================
   Compute Non-Redundant Factors for a Clause
========================================================================*/

nonRedFact([],[]).
   
nonRedFact([X|C1],C2):-
   memberList(Y,C1),
   unify_with_occurs_check(X,Y),
   nonRedFact(C1,C2).

nonRedFact([X|C1],[X|C2]):-
   nonRedFact(C1,C2).

Bearbeiten Sie die Aufgaben 5.6.1 bis 5.6.3.

Theorem Provers and Model Builders

Zusammenfassung

Theorembeweiser ermöglichen es die Nichtkonsistenz einer Aussage in Bezug auf andere Aussagen nachzuweisen.
Model Builder ermöglichen es (partiell) die Konsistenz einer Aussage in Bezug auf andere Aussagen nachzuweisen.
Theorembeweiser ermöglichen es die Uninformativität einer Aussage in Bezug auf andere Aussagen nachzuweisen.
Model Builder ermöglichen es (partiell) die Informativität einer Aussage in Bezug auf andere Aussagen nachzuweisen.

Off-the-Shelf Theorem Provers

Die Resolutionsmethode ist sehr einfach, allerdings in der plumpen Form, in der wir sie implementiert haben auch sehr ineffizient.
Auch haben wir die Behandlung von Gleichheit bisher nicht implementiert. Man könnte sie theoretisch hinzufügen, indem man jedem Aufruf die Axiome des Gleichheitsprädikats hinzufügt:
- $\forall x (x=x)$
- $\forall x \forall y (x=y \rightarrow y=x)$
- $\forall x \forall y \forall z (x=y \wedge y=z \rightarrow x=z)$
Wenn man das macht, wird man feststellen, dass die Verarbeitung sehr langsam wird. Teste zum Beispiel die Inkonsistenz von “Mia does not snort” in Bezug auf die Sätze “Every woman snorts” und “Mia is a woman”.
Viele moderne Theorembeweiser beruhen auf der Resolutionsmethode. Sie verwenden aber wesentlich effizientere Methoden zur Verarbeitung von Gleichheit und implementieren diverse Strategien zur Wahl möglichst effektiver Resolutionsschritte.

Teste

?- EQ = and(and(all(X,gleich(X,X)),all(X,forall(Y,imp(gleich(X,Y),gleich(Y,X))))),all(X,all(Y,all(Z,imp(and(gleich(X,Y),gleich(Y,Z)),gleich(X,Z)))))),
  Kontext = and(all(X,imp(woman(X),snort(X))),some(X,and(woman(X),gleich(mia,X)))),
  New = not(snort(mia)),
rprove(imp(and(EQ,Kontext),not(New))).

Im folgenden konzentrieren wir uns auf den Theorembeweiser Otter:

Folgt bitte den Anweisungen in How_to_Curt.html (Link siehe Kurswebsite) bis einschließlich “Testen” oder installiert euch die Virtual Box, die ebenfalls auf der Kursseite verlinkt ist.

Beispiel: $\forall x dance(x) \rightarrow \neg\exists x \neg dance(x)$

?- fol2otter(imp(all(X,dance(X)),not(some(Y,not(dance(Y))))),user).

set(auto).
assign(max_seconds,30).
clear(print_proofs).
set(prolog_style_variables).
formula_list(usable).
((all A dance(A)) -> -((exists B -(dance(B))))).
end_of_list.

?- callTP(imp(all(X,dance(X)),not(some(Y,not(dance(Y))))),P,E).

Off-the-Shelf Model Builder

Im folgenden fokussieren wir uns auf den Model Builder MACE.

Beispiel: $\forall x boxer(x)\rightarrow slow (x) \wedge boxer(butch) \wedge likes(mia,butch)$

?- fol2mace(and(all(X,imp(boxer(X),slow(X))),and(boxer(butch),likes(mia,butch))),user).

set(auto).
clear(print_proofs).
set(prolog_style_variables).
formula_list(usable).
((all A (boxer(A) -> slow(A))) & 
     (boxer(butch) & 
          likes(mia,butch))).
end_of_list.

callMB/4
callMB(Problem,DomainSize, Model, ModelBuilder).

?- callMB(and(all(X,imp(boxer(X),slow(X))),and(boxer(butch),likes(mia,butch))),5,Model,MB).


Model = D=[d1]
  f(1,boxer,[d1])
  f(1,slow,[d1])
  f(0,butch,d1)
  f(0,mia,d1)
  f(2,likes,[(d1,d1)])
,
MB = mace.

Blackburn and Bos: Representation and Inference of Natural Language

Chapter 5: First-Order Inference

Wiebke Petersen