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

wahr((F & G)) :- !, wahr(F) , wahr(G).
wahr((F \/ G)) :- !, (wahr(F), ! ; wahr(G)). 
wahr((F => G)) :-  !, wahr(neg(F) \/ G).
wahr((F <=> G)) :- !, wahr((F => G) & (G => F)).
wahr(neg(F)) :- !, (wahr(F) -> fail ; true).

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

wahr(ex(Var,Formel)) :-
    !, (debugging(typisieren) % aktivieren mit ?- debug(typisieren). 
       -> ( var(Var) ->
              type([],ex(Var,Formel),Getypt,_),
              wahr(Getypt)
          ; Var = V:Typ,
              objekt(V:Typ), wahr(Formel), !
          )
       ; objekt(Var:_), wahr(Formel), !
       ).

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.

wahr(Formel) :-
    functor(Formel,_Fn,_Arity),
%     predicate_property(Formel,  % unguenstig, wenn man Module hat
%                        imported_from(datenbank)),
    call(Formel), !.

beantworte(PL_Aussage,Wert) :-
    wahr(PL_Aussage) -> Wert = ja ; Wert = nein.

antworten(qu(Var,Formel), As) :-
    (debugging(typisieren) % aktivieren mit ?- debug(typisieren).
    -> ( var(Var) 
       -> type([],qu(Var,Formel),qu(Var:Typ,Fml),_),
           antworten(qu(Var:Typ,Fml), As)
       ; Var = V:Typ,
           findall(V,(objekt(V:Typ), wahr(Formel)),Ws),
           sort(Ws,As)
       )
    ; findall(Var,(objekt(Var:_), wahr(Formel)),Ws),
        sort(Ws,As)
    ).