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