EtherPad der PhilFak Etherpad is Freie Software
Vollbild

Server Notice:

hide

Public Pad Latest text of pad jfYuHkAprP Saved Aug 1, 2018

 
imp(and(not(p),not(q)),not(or(p,q)))
 
 
 
 
 
 
 
imp(or(r,and(p,q)),and(or(r,p),or(r,q)))
 
 
 
 
 
 
 
 
 
 
 
callTP(imp(all(X,dance(X)),not(some(Y,not(dance(Y))))),Proof,Engine).
 
cmd.exe /C perl C:/Curt/interfaceTP.perl C:/Curt ottermace
 
 
mia is a wife
mia does not love a boxer.
every married woman loves a boxer.
 
1 D=[d1,d2]
  f(1,event,[])
  f(1,thing,[d1,d2])
  f(1,entity,[d1,d2])
  f(1,object,[])
  f(1,organism,[d1,d2])
  f(1,animal,[])
  f(1,person,[d1,d2])
  f(1,man,[])
  f(1,woman,[d1])
  f(1,boxer,[d1,d2])
  f(1,wife,[d1])
  f(1,married,[d1])
  f(0,mia,d1)
  f(0,c1,d1)
  f(0,c2,d1)
  f(2,love,[(d1,d2)])
  f(0,c3,d2)
 
d1: woman, boxer, wife, married, mia
d2: boxer
love(d1,d2)
 
Aufgabe: Wandle in setCNF um:
 (∀xB(x)∧∃yA(y,x))→∃z∀x∃yC(x,z)∨B(z,y)
 
~ (∀xB(x)∧∃yA(y,x)) v ∃z∀x∃yC(x,z)∨B(z,y)
 
[[not B(x), not A(y,x), C(w,s2),B(s2,s1(w))
 
//cnf(imp(all(X,and(b(X),some(Y,a(Y,X)))),some(Z,all(X,some(Y,or(c(X,Z),b(Z,Y)))))),SetCNF).
 
Ouptut:
SetCNF = [[not(b(fun(4))),not(a(Y,fun(4))),b(fun(5),fun(6,X)),c(X,fun(5))]] 
 
 
nnf(imp(all(X,and(b(X),some(Y,a(Y,X)))),some(Z,all(X,some(Y,or(c(X,Z),b(Z,Y)))))),NNF).
 
#nnf(imp(all(X,and(b(X),some(Y,a(Y,X)))),some(Z,all(X,some(Y,or(c(X,Z),b(Z,Y)))))),NNF).
NNF = or(some(X,or(not(b(X)),all(Y,not(a(Y,X))))),some(Z,all(X,some(Y,or(c(X,Z),b(Z,Y)))))) ;
NNF = (some X (~ b(X) v all Y ~ a(Y,X)) v some Z all X some Y (c(X,Z) v b(Z,Y)))
 
 
########
cnf(imp(all(X,and(b(X),some(Y,a(Y,X))))),some(Z,all(X,some(Y,or(c(X,Z),b(Z,Y))))),SetCNF).
 
SetCNF = [[not(b(fun(1))),not(a(Y,X)),b(Z,Y),c(X,fun(2))]]
 
####das von uns
cnf( imp(all(X,and(b(X),some(Y,a(Y,X)))),some(Z,all(X,some(Y,or(c(X,Z),b(Z,Y)))))),SetCNF).
 
 
nonRedFact([p(a),p(X),r(Y,b),r(Z,X),not(q(W)),not(q(f(Z)))],NRFL).
 
 
 
g(a,X)   g(a,f(U))
{X\f(U)}
 
g(a,f(U))
 
g(X,Y)
{X\Y,Y\X}
g(Y,X)
g(X,Y)
 
 
 
 
 
R(X,Y,g(f(Y),a),b,f(Y))     R(U,f(X),g(X,U),W,f(b))
s1={X\U}
R(U,Y,g(f(Y),a),b,f(Y))     R(U,f(U),g(U,U),W,f(b))
s2={Y\f(U)} 
s2 s1
R(U,f(U),g(f(f(U)),a),b,f(f(U)))     R(U,f(U),g(U,U),W,f(b))
 
R(X,Y,g(f(Y),a),b,f(Y))     R(U,f(X),g(X,U),W,f(b))
{X\f(Y),U\a)
R(f(Y),Y,g(f(Y),a),b,f(Y))     R(a,f(f(Y)),g(f(Y),a),W,f(b))
 
 
[debug] 19 ?- consistent([[vincent, is, a, man],[mia,smokes],[vincent,does,not,smoke]]).
(~ smoke(vincent) & (smoke(mia) & some _7628 (man(_7628) & vincent = _7628)))
no more consistent readings
 
[debug] 20 ?- consistent_with_equality([[vincent,is,a,man]]).
(some _7226 (man(_7226) & vincent = _7226) & (all _7792 _7792=_7792 & (all _7792 all _7816 (_7792=_7816 > _7816=_7792) & all _7792 all _7816 all _7852 ((_7792=_7816 & _7816=_7852) > _7792=_7852))))
no more consistent readings
 
[debug] 21 ?- consistent_with_equality([[vincent,is,a,man],[every,man,smokes],[vincent,does ,not,smoke]]).
(~ smoke(vincent) & (all _8528 (man(_8528) > smoke(_8528)) & (some _7870 (man(_7870) & vincent = _7870) & (all _9090 _9090=_9090 & (all _9090 all _9114 (_9090=_9114 > _9114=_9090) & all _9090 all _9114 all _9150 ((_9090=_9114 & _9114=_9150) > _9090=_9150))))))
no more consistent readings
 
 
 
 
:- use_module(kellerStorage,[kellerStorage/2]).
:- use_module(foResolution,[rprove/1]).
 
consistent(Context):-
    readings(Context,[R|Readings]),
    check_consistency(Readings,R,ConsReadings),
    pettyprint_readings(ConsReadings).
 
consistent_with_equality(Context):-
    readings(Context,Readings),
    Eq = and(all(X,=(X,X)),and(all(X,all(Y,imp(=(X,Y),=(Y,X)))),all(X,all(Y,all(Z,imp(and(=(X,Y),=(Y,Z)),=(X,Z) ) ) ) ) )),
    check_consistency(Readings,[Eq],ConsReadings),
    prettyprint_readings(ConsReadings).
 
 
readings([],[]).
 
readings([S|T],[R|Readings]):-
    kellerStorage(S,R),
    readings(T,Readings).
 
prettyprint_readings([]):-
    prettyprint('no more consistent readings').
 
prettyprint_readings([R|Readings]):-
    prettyprint(R),nl,
    prettyprint_readings(Readings).
 
% check_consistency(ListOfListofFormulas, OldListOfFormulas, NewListOfFormulas)
 
check_consistency([],Acc,Acc).
 
check_consistency([R|Readings],Acc,ConReadings):-
    consistent_readings(R,Acc,ConsAcc),
    check_consistency(Readings,ConsAcc,ConReadings).
 
% consistent_readings(ListOfReadings,ListOfOldReadings,ListOFNewReadings)
consistent_readings([],_,[]).
 
consistent_readings([R|RT],FormerReadings,ConsAccNew):-
    consistent(R,FormerReadings,NewReadings),
    append(NewReadings,ConsAcc,ConsAccNew),
    consistent_readings(RT,FormerReadings,ConsAcc).
 
%consistent(Formula,ListOfFormulas,NewListOfFormulas)
 
consistent(_F,[],[]).
consistent(F,[FO|TO],ConsNew):-
    rprove(not(and(F,FO))),!,
    consistent(F,TO,ConsNew).
 
consistent(F,[FO|TO],[and(F,FO)|ConsNew]):-
    consistent(F,TO,ConsNew).
 
 
 
 
 
Wenn p1 & p2 & p3 -> q gültig, dann ist q uniformativ in Bezug auf p1,p2,p3
 
 
T(p1 & p2 & p3 )
F q
 
 
 
[[S1a,S1b,S1c],[S2],[S3a,S3b]]
 
[S1a&S2,  S1c&S2]
 
 
 
 
:- use_module(foResolution,[rprove/1]).
:- use_module(kellerStorage,[kellerStorage/2]).
 
 
 
consistent(ListOfSentences):-
     readings(ListOfSentences,Readings),
     consistent_propositions(Readings,ConsistentPropositions),
     pp_output(ConsistentPropositions).
     
readings([],[]).
readings([S|ListSentences],[R|ListSentences]):-
      kellerStorage(S,R),
      readings(ListeSentences, ListReadings).
            
 
prettyprint([]).
 
prettyprint([H|T]):-
      print(H), nl,
      pp_output(T).
     
 
 
 
 
 
?- kellerStorage.
 
> every boxer does not love every person.
 
 
1 all(A,imp(boxer(A),not(all(B,imp(person(B),love(A,B))))))
für alle Boxer gilt, es gibt eine Person, die der Boxer nicht liebt.
2 all(A,imp(boxer(A),all(B,imp(person(B),not(love(A,B))))))
für alle Boxer gilt, dass alle Personen von dem Boxer nicht geliebt werden.
alle Boxer lieben keine Person
3 all(A,imp(person(A),all(B,imp(boxer(B),not(love(B,A))))))
alle Personen werden von allen Boxern nicht geliebt.
alle Boxer lieben keine Person
 
true.
 
HoleSemantics.
1 some(A,and(hole(A),some(B,and(label(B),some(C,some(D,some(E,some(F,some(G,and(hole(C),and(label(D),and(label(E),and(label(F),and(all(E,G,F),and(imp(F,D,C),and(leq(B,C),and(leq(E,A),and(and(pred1(D,boxer,G),leq(D,A)),some(H,some(I,and(hole(H),and(label(I),and(not(I,H),and(leq(I,A),and(leq(B,H),some(J,some(K,some(L,some(M,some(N,and(hole(J),and(label(K),and(label(L),and(label(M),and(all(L,N,M),and(imp(M,K,J),and(leq(B,J),and(leq(L,A),and(and(pred1(K,person,N),leq(K,A)),and(pred2(B,love,G,N),leq(B,A)))))))))))))))))))))))))))))))))))))))))
 
1 not(all(G,imp(boxer(G),all(N,imp(person(N),love(G,N))))))
Es ist nicht wahr, dass alle Boxer jede Person lieben
Es gibt einen Boxer, der nicht alle Personen liebt  [nicht bei Keller]
2 not(all(N,imp(person(N),all(G,imp(boxer(G),love(G,N))))))
Es gilt nicht, dass alle Personen von allen Boxern geliebt werden.
Es gibt eine Person, die nicht von allen Boxern geliebt wird.  [nicht bei Keller]
3 all(G,imp(boxer(G),not(all(N,imp(person(N),love(G,N))))))
für alle Boxer gilt, es gibt eine Person, die der Boxer nicht liebt. [Keller 1]
4 all(G,imp(boxer(G),all(N,imp(person(N),not(love(G,N))))))
alle Boxer lieben keine Person [Keller 2]
5 all(N,imp(person(N),not(all(G,imp(boxer(G),love(G,N))))))
Alle Personen werden von nicht allen Boxern geliebt [nicht bei Keller]
Für alle Personen gilt, es gibt einen Boxer, der sie nicht liebt.
6 all(N,imp(person(N),all(G,imp(boxer(G),not(love(G,N))))))
alle Personen werden von allen Boxern nicht geliebt. [Keller 3]
true.
 
 
 
 
 
 
 
Spannende Sätze
 
every criminal shoots a criminal in a restaurant.  (9)
every criminal loves every criminal.
every boxer does not know a owner of every hash bar 
mia does not love every criminal. (2)
every boxer does not love every owner of a big hash bar that collapses. (24)
every boxer or a woman does not love every owner and criminal of a big hash bar that collapses. (130)
every owner of a hash bar loves every criminal with a five dollar shake in a plant. (536)
every owner of a hash bar loves every criminal and a five dollar shake and a plant. (261)
every boxer and a woman know every owner of a restaurant or every hash bar. (652 Lesarten)
 
mia loves every boxer that has a hash bar. (3)
 
every boxer does not love every person.
 
------------------------------------------------------------------------------------------------------------------------
 
 
 
cooperStorage: np(M,[a,criminal],[]).
 
 
------------------------------------------------------------------------------------------------------------------------
 
 
?- cooperStorage.
 
> A criminal knows every owner of a hash bar.
 
1 all A ((of(A,B) & owner(A)) > some C (hashbar(C) & some D (criminal(D) & know(D,A))))
2 all A ((some B (hashbar(B) & of(A,B)) & owner(A)) > some C (criminal(C) & know(C,A)))
3 all A ((of(A,B) & owner(A)) > some C (criminal(C) & some D (hashbar(D) & know(C,A))))
4 all A ((of(A,B) & owner(A)) > some C (hashbar(C) & some D (criminal(D) & know(D,A))))
5 some A (criminal(A) & all B ((some C (hashbar(C) & of(B,C)) & owner(B)) > know(A,B)))
6 some A (criminal(A) & all B ((of(B,C) & owner(B)) > some D (hashbar(D) & know(A,B))))
7 some A (criminal(A) & some B (hashbar(B) & all C ((of(C,B) & owner(C)) > know(A,C))))
8 some A (hashbar(A) & some B (criminal(B) & all C ((of(C,A) & owner(C)) > know(B,C))))
9 some A (hashbar(A) & all B ((of(B,A) & owner(B)) > some C (criminal(C) & know(C,B))))
true.
 
-----------------------------------
 
?- kellerStorage.
 
> A criminal knows every owner of a hash bar.
 
1 all A ((some B (hashbar(B) & of(A,B)) & owner(A)) > some C (criminal(C) & know(C,A)))
2 some A (criminal(A) & all B ((some C (hashbar(C) & of(B,C)) & owner(B)) > know(A,B)))
3 some A (hashbar(A) & some B (criminal(B) & all C ((of(C,A) & owner(C)) > know(B,C))))
4 some A (criminal(A) & some B (hashbar(B) & all C ((of(C,B) & owner(C)) > know(A,C))))
5 some A (hashbar(A) & all B ((of(B,A) & owner(B)) > some C (criminal(C) & know(C,B))))
true.
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
lesart 3
Für jeden Besitzer einer HBAR gibt es einen BKB, der jedem Kriminellen gegeben wird
 
lesart 6
Jeder Kriminelle hat eine Hashbar und einen BKB für die gilt, dass er von jedem Besitzer dieser Hashbar diesen BKB bekommt.
<=>
lesart 7
Jeder Kriminelle hat eine Hashbar und einen BKB für die gilt, dass er von jedem Besitzer dieser Hashbar diesen BKB bekommt.
 
lesart 11
Es gibt eine Hashbar und für jeden Kriminellen und jeden Besitzer der Hashbar gibt es einen Big Kahuna Burger, den der Besitzer dem Kriminellen gibt.
 
lesart 15
Es gibt eine Hashbar und allen Kriminellen wird ein Big Kahuna Burger von allen Besitzern dieser gegeben.
 
Es gibt eine Hashbar und für jeden kriminellen gibt es einen Big Kahuna Burger, der dem kriminellen von jedem Besitzer der Hashbar gegeben wird.
 
 
 
 
Jeder Hund (x) jagt eine Katze (y) in jedem Zimmer (z).
 
(1) 
forall x [hund(x) -> some y  [katze(y)  forall z [zimmer(z) -> jiz(x,y,z)]]]
 
jiz(h1,k1,z1)
jiz(h1,k1,z2)
jiz(h2,k2,z1)
jiz(h2,k2,z2)
 
 
(2) eine Katze wird von jedem Hund in jedem Zimmer gejagt
exists y(katze(y) AND forall x(hund(x) -> forall z(zimmer(z) -> jiz(x,y,z))))
exists y. [katze(y) and forall z. [zimmer(z) -> forall x. [hund(x) -> jiz(x,y,z)]]]
jiz(h1,k1,z1)
jiz(h1,k1,z2)
jiz(h2,k1,z1)
jiz(h2,k1,z2)
 
 
(3)
 
forall x hund(x) -> forall z. zimmer(z) -> exists y. [katze(y) and jiz(x,y,z)]]
jiz(h1,k1,z1)
jiz(h1,k2,z2)
jiz(h2,k2,z1)
jiz(h2,k1,z2)
 
 
 
 
forall x [hund(x) -> katze(y) forall z [zimmer(z) -> jiz(x,y,z)]]
 
 
 
forall z(zimmer(z) -> forall x(hund(x) -> exists y(katze(y) AND jiz(x,y,z))))
jiz(h1,k1,z1)
jiz(h2,k2,z1)
jiz(h1,k1,z2)
jiz(h2,k2,z2)
 
forall z. [zimmer(z) -> exists y.[katze(y) and forall x. [hund(x) -> jiz(x,y,z)]]]
 
Beispielaufrufe, die zeigen, warum alpha-Konversion wichtig ist:
 
 
lam x snort(x)@ mia AND lam x laugh(x) @ vincent
 
snort(mia) AND laugh(vincent)
 
betaConvert(and(app(lam(X,snort(X)),mia),app(lam(X,laugh(X)),vincent)),Conv).
 
every woman loves every woman
(lam x forall y woman(y) -> x@y) @ lam u forall y woman(y) -> love(u,y)
betaConvert(app(lam(X,all(Y,imp(woman(Y),app(X,Y)))), lam(U,all(Y,imp(woman(Y),love(U,Y)))) ), Conv).
 
 
 
 
 
s --> np, vp, {mia(X)}.
 
s(A,C):- np(A,B), vp(B,C), mia(X).