:- op(500,yfx,&), op(600,yfx,'\/'),
    op(600,xfx,'=>'), op(600,xfx,'<=>').

wahr(astronom(X)) :-
    datenbank:astronom(X),!.
wahr(stern(X)) :-
    datenbank:stern(X),!.
wahr(sonne(X)) :-
    datenbank:sonne(X),!.

wahr(planet(X,Y)) :-
    datenbank:planet(X,Y),!.
wahr(mond(X,Y)) :-
    datenbank:mond(X,Y),!.
wahr(durchmesser(X,Y)) :-
    datenbank:durchmesser(X,Y),!.

wahr(entdecken(X,Y)) :-
    datenbank:entdecken(X,Y),!.
wahr(umkreisen(X,Y)) :-
    datenbank:umkreisen(X,Y),!.

wahr(mond(X)) :- wahr(ex(Y,mond(X,Y))).
wahr(planet(X)) :- wahr(ex(Y,planet(X,Y))).
wahr((F & G)) :- wahr(F) , wahr(G).
wahr((F \/ G)) :- wahr(neg(neg(F) & neg(G))). 
wahr((F => G)) :-  wahr(neg(F) \/ G).
wahr((F <=> G)) :- wahr((F => G) & (G => F)).
wahr(neg(F)) :- falsch(F).

falsch(F) :- (wahr(F) -> fail ; true).

wahr(all(Var,F)) :-
    wahr(neg(ex(Var,neg(F)))).

wahr(ex(Var,Formel)) :-
    objekt(Var), wahr(Formel), !.
objekt(X) :-
    datenbank:stern(X)
    ; datenbank:astronom(X)
    ; datenbank:durchmesser(X,_).

wahr((X < Y))  :- X < Y.
wahr((X =< Y)) :- X =< Y.
wahr(eq(X,Y))  :- X = Y.
wahr(anzahl(Var,Formel,Zahl)) :-
    antworten(qu(Var,Formel),Objekte),
    length(Objekte,N),
    Zahl =< N.
beantworte(PL_Aussage,Wert) :-
    wahr(PL_Aussage) -> Wert = ja ; Wert = nein.

antworten(qu(Var,Formel), As) :-
    findall(Var,(objekt(Var), wahr(Formel)),Ws),
    sort(Ws,As).