name(drinker). :- dynamic d/1,notd/1. % The Drinker Paradox: in a non-empty group there is somebody such that, % if (s)he is drunk then everybody is drunk. % Since the Drinker Paradox heavily relies on classical logic it is not % a natural example for GL. However, it is possible. % First of all the domain should be non-empty: dom(a). % The goal is: % there exists x such that d(y) for all y whenever d(x). % This is not a geometric formula. The systematic translation % based on the tableaux method yields that the Drinker Paradox is % a tautology iff the following geometric theory is inconsistent: _ axiom d_cons(X) : (d(X),notd(X) => false). _ axiom neg_phi(X) : (dom(X) => d(X),neg_psi). _ axiom neg_psi_ax : (neg_psi => dom(Y),notd(Y)). % NB inconsistency is proved without a clause for goal!