% original version at http://www.ii.uib.no/~bezem/GL/drinker.in

:- op(1200,xfx,':=').
:- op(1199,xfx,'=>').

:- dynamic(d/1).
:- dynamic(notd/1).
:- dynamic(neg_psi/0).
:- dynamic(dom/1).

flag(keywords).
flag(quiet).
flag(quick).

% 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:

[d_cons,X]    := d(X),notd(X) => false.
[neg_phi,X]   := dom(X) => d(X),neg_psi.
[neg_psi_ax]  := neg_psi => dom(Y),notd(Y).

% NB inconsistency is proved without a clause for goal!