Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/TRS/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 28.9.2014 mit Größe 3 kB

Quellcode-Bibliothek top_field.pvs Sprache: unbekannt

%------------------------------------------------------------------------------
% Mathematical Structures (Part II)
%
% Ring/Field-like Mathematical Structures with signatures:
%     [T:Type+,+,*:[T,T->T],zero:T]  or   [T:Type+,+,*:[T,T->T],zero,one:T]
%
%     Author: David Lester, Manchester University & NIA
%             Rick Butler
%
%     Version 1.0            3/1/02
%     Version 1.1           12/3/03   New library structure
%     Version 1.2            5/5/04   Reworked for definition files DRL
%------------------------------------------------------------------------------

top_field: THEORY

BEGIN
%----------------------------------------+------------------------------------
%             File                       | Mathematical Structure of *
%----------------------------------------+------------------------------------

    IMPORTING ring,                      % semigroup[T,*]
              commutative_ring,          % commutative_semigroup[T,*]
              ring_nz_closed,            % semigroup[T,*], semigroup[nz_T,*]
              ring_with_one,             % monoid[T,*,one]
              commutative_ring_with_one, % commutative_monoid[T,*,one]
              integral_domain,           % commutative_semigroup[T,*]
                                         % commutative_semigroup[nz_T,*]
              division_ring,             % monoid[T,*,one], group[nz_T,*,one]
              field                      % commutative_monoid[T,*,one]
                                         % abelian_group[nz_T,*,one]
%             field_test

END top_field

quality92%