Top File of PVS TU_Games Library

 
%---------------------------------------------------------------------
% A formal theory of cooperative TU-games in PVS 4.2
%
% Author: Erik Martin-Dorel,
% University Montpellier 2 & University of Perpignan
%
%   Version 1.0    2009/06/30    Initial version
%
% This work has been done at the University of Perpignan
% within the Master's Thesis, under the supervision of
% Marc Daumas and Annick Truffert, with the help of Michel Ventou
%
% Presented at the 6th conference on Modeling Decisions for 
% Artificial Intelligence (MDAI 2009 in Awaji Island, Japan)
% and a report appears in Volume 5861/2009 of the Lecture Notes in
% Computer Science (Springer).
% A Formal Theory of Cooperative TU-Games
% DOI	 10.1007/978-3-642-04820-3_8
% Pages	 81-91
%
% This library is available under GNU Lesser General Public License,
% either version 3 of the Licence, or any later version  (cf. infra)
%---------------------------------------------------------------------


top: THEORY

 BEGIN

  % The first parameter of each THEORY (U:TYPE+) represents
  % the Universe of players that are likely to participate.

  IMPORTING players_set,   % (param. by [U]    ) first TYPE to be defined
            coalition_fun, % (param. by [U,N]  ) finite_sets imported here
            imputations,   % (param. by [U,N,v]) payoffs, imputations, core

            tu_game        % from tu_game TYPE to solution_concept Properties

 END top


%---------------------------------------------------------------------
% License for use and distribution
%
% Copyright (C) 2009 Erik Martin-Dorel.
%
% GNU LGPL information:
% ---------------------
%
% This library is free software: you can redistribute it and/or
% modify it under the terms of the GNU Lesser General Public License
% as published by the Free Software Foundation, either version 3 of
% the License, or (at your option) any later version.
%
% This library is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
% GNU General Public License for more details.
%
% You should have received a copy of the GNU Lesser General Public
% License along with this library.
% If not, see .
%---------------------------------------------------------------------

The tag identifies links that are outside the NASA domain