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.

disagreement pair: w and k

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.

Free Variable Tableaux

/*========================================================================
   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).


/*========================================================================
   VarList is a list of free variables, and SkolemTerm is a previously 
   unused Skolem function symbol fun(N) applied to those free variables.
========================================================================*/

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


/*========================================================================
   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).


/*========================================================================
   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).

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


/*========================================================================
   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).


/*========================================================================
   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(_,_))).


/*========================================================================
   Remove quantifier from signed quantified formula, and replacing all
   free occurrences of the quantified variable by occurrences of Term.
========================================================================*/

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

Hausaufgabe

Schreiben Sie eine kurze Zusammenfassung (maximal 2-3 Seiten, oder ca. 5-10 Sätze pro Kapitel), der ersten 5 Kapitel des Buches. Sie sollen natürlich nicht auf die Details eingehen, sondern den roten Faden sichtbar machen, dem die Argumentation in dem Buch folgt. Begriffe die vorkommen sollten sind: entscheidbar, model builder, theorem prover, …

Es kommt mir nicht darauf an, dass ihr Text besonders gut geschrieben ist (auf ordentliche Referenzen dürfen sie ausnahmsweise verzichten und sie können Englische Terminologie in Ihren Text mengen). Ziel ist, dass Sie den Stoff einmal in der Gesamtschau wiederholen und zeigen, dass Sie die wichtigsten Zusammenhänge verstanden haben.

Blackburn and Bos: Representation and Inference of Natural Language

Chapter 5: First-Order Inference

Wiebke Petersen

First-Order Inference

Wiederholung: Propositional Inference

Free Variable Tableaux

Hausaufgabe