% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %
%                                                                           %
% File:            quantifi.dtr                                             %
% Purpose:         first order quantification on attribute sequences        %
% Author:          Gerald Gazdar, 24 August 1989                            %
% Email:           geraldg@cogs.sussex.ac.uk                                %
% Address:         COGS, Sussex University, Brighton BN1 9QH, UK            %
% Documentation:   see paper cited below                                    %
% Related files:   boolean1.dtr, boolean2.dtr                               %
% Version:         2.01                                                     %
%      Copyright (c) University of Sussex 1989.  All rights reserved.       %
%                                                                           %
% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %

% Johan van Benthem's (1986) "Semantic automata" in his Essays in Logical
% Semantics, Dordrecht: Reidel, 151-176, is highly pertinent to this example
% file.  He shows, inter alia, that all first order definable quantifiers
% are computable by finite state machines.  The examples given below are
% all first order, but, in the light of van Benthem's paper, readers may
% care to try their hands at DATR axiom sets for 'most', 'an even number of',
% 'at least one third' and 'at least two thirds'.

Q:      <all> == yes
        <all no> == no
        <all yes> == <all>
        <exactly_one> == no
        <exactly_one no> == <exactly_one>
        <exactly_one yes> == <none>
        <some> == no                        % <some> = "at least one"
        <some yes> == yes
        <some no> == <some>
        <none> == yes
        <none yes> == no
        <none no> == <none>
        <who> == "Ann:<>" "Beryl:<>" "Carl:<>" "Dana:<>" "Eric:<>"
        <are all>  == <all  Ann:<> Beryl:<> Carl:<> Dana:<> Eric:<>>
        <is exactly_one> == <exactly_one  Ann:<> Beryl:<> Carl:<>
                                          Dana:<> Eric:<>>
        <are some> == <some Ann:<> Beryl:<> Carl:<> Dana:<> Eric:<>>
        <are none> == <none Ann:<> Beryl:<> Carl:<> Dana:<> Eric:<>>.

Is:     <is> == <"<>">
        <no> ==
        <yes> == "<name>".

Ann:    <> == Is
        <old> == yes
        <ill> == no
        <tall> == yes
        <dead> == no
        <name> == 'Ann '. % The trailing space is to format <who is> answers.

Beryl:  <> == Is
        <old> == yes
        <ill> == no
        <tall> == no
        <dead> == no
        <name> == 'Beryl '.

Carl:   <> == Is
        <old> == yes
        <ill> == no
        <tall> == no
        <dead> == no
        <name> == 'Carl '.

Dana:   <> == Is
        <old> == yes
        <ill> == yes
        <tall> == yes
        <dead> == no
        <name> == 'Dana '.

Eric:   <> == Is
        <old> == yes
        <ill> == no
        <tall> == no
        <dead> == no
        <name> == 'Eric '.

% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %

% Some theorems:
%
%    Q: <are all old> = yes.
%    Q: <are all ill> = no.
%    Q: <are all tall> = no.
%    Q: <are all dead> = no.
%
%    Q: <is exactly_one old> = no.
%    Q: <is exactly_one ill> = yes.
%    Q: <is exactly_one tall> = no.
%    Q: <is exactly_one dead> = no.
%
%    Q: <are some old> = yes.
%    Q: <are some ill> = yes.
%    Q: <are some tall> = yes.
%    Q: <are some dead> = no.
%
%    Q: <are none old> = no.
%    Q: <are none ill> = no.
%    Q: <are none tall> = no.
%    Q: <are none dead> = yes.
%
%    Q: <who is old> = Ann Beryl Carl Dana Eric.
%    Q: <who is ill> = Dana .
%    Q: <who is tall> = Ann Dana .
%    Q: <who is dead> = .

% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % %

# show  <are all old>
        <are all ill>
        <are all tall>
        <are all dead>
        <is exactly_one old>
        <is exactly_one ill>
        <is exactly_one tall>
        <is exactly_one dead>
        <are some old>
        <are some ill>
        <are some tall>
        <are some dead>
        <are none old>
        <are none ill>
        <are none tall>
        <are none dead>
        <who is old>
        <who is ill>
        <who is tall>
        <who is dead>.

# hide Is Ann Beryl Carl Dana Eric.

% The next line is the Revision Control System Id: do not delete it.
% $Id: archive.dtr,v 1.1 1997/04/09 20:40:33 root Exp $