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


products/sources/formale Sprachen/PVS/TRS/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 3 kB

Quelle relations_closure.pvs Sprache: PVS

%%-------------------** Abstract Reduction System (ARS) **-------------------
%%
%% Authors         : Andre Luiz Galdino
%%                   Universidade Federal de Goiás - Brasil
%%
%%                         and
%%
%%                   Mauricio Ayala Rincon
%%                   Universidade de Brasília - Brasil
%%
%% Last Modified On: December 02, 2006
%%
%%---------------------------------------------------------------------------

%%---------------------------------------------------------------------------
%%
%% We defined reflexive, symmetric, transitive, reflexive and transitive,
%% and equivalence closures of a binary relation in the same way that
%% Alfons Geser defined in .../lib/../closure_ops.pvs. We just changed
%% the names of the definitions and we proved some additional properties.
%%
%%---------------------------------------------------------------------------

relations_closure[T : TYPE] : THEORY
BEGIN

IMPORTING
    orders@closure_ops[T],
    sets_lemmas[T]

   S, R: VAR pred[[T, T]]
   n: VAR nat
   p: VAR posnat

   reflexive: TYPE = (reflexive?)

   symmetric: TYPE = (symmetric?)

   transitive: TYPE = (transitive?)

   reflexive_transitive?(R): bool = reflexive?(R) & transitive?(R)

   reflexive_transitive: TYPE = (reflexive_transitive?)

   equivalence: TYPE = (equivalence?)

% % Reflexive Closure (RC)

    RC(R): reflexive = union(R, =)

% %% Properties

   change_to_RC : LEMMA reflexive_closure(R) = RC(R)

   R_subset_RC : LEMMA subset?(R, RC(R))

   RC_idempotent : LEMMA  RC(RC(R)) = RC(R)

   RC_characterization : LEMMA  reflexive?(S) <=> (S = RC(S))

% % Symmetric Closure (SC)

    SC(R): symmetric = union(R, converse(R))

% %% Properties

   change_to_SC : LEMMA symmetric_closure(R) = SC(R)

   R_subset_SC : LEMMA subset?(R, SC(R))

   SC_idempotent : LEMMA  SC(SC(R)) = SC(R)

   SC_characterization : LEMMA  symmetric?(S) <=> (S = SC(S))

% % Transitive Closure (TC)

    TC(R): transitive = IUnion(LAMBDA p: iterate(R, p))

% %% Properties

   change_to_TC : LEMMA transitive_closure(R) = TC(R)

   R_subset_TC :LEMMA subset?(R, TC(R))

   TC_converse: LEMMA  TC(converse(R)) = converse(TC(R))

   TC_idempotent : LEMMA  TC(TC(R)) = TC(R)

   TC_characterization : LEMMA  transitive?(S) <=> (S = TC(S))



% % Reflexive Transitive Closure (RTC)

   RTC(R): reflexive_transitive = IUnion(LAMBDA n: iterate(R, n))

% %% Properties

   change_to_RTC : LEMMA preorder_closure(R) = RTC(R)

   R_subset_RTC: LEMMA subset?(R, RTC(R))

   iterate_RTC: LEMMA FORALL n : subset?(iterate(R, n), RTC(R))

   RTC_idempotent : LEMMA  RTC(RTC(R)) = RTC(R)

   RTC_characterization : LEMMA reflexive_transitive?(S) <=> (S = RTC(S))

% % Equivalence Closure (EC)

    EC(R): equivalence = RTC(SC(R))

% %% Properties

    change_to_EC : LEMMA equivalence_closure(R) = EC(R)

    R_subset_EC: LEMMA subset?(R, EC(R))

    RTC_subset_EC: LEMMA subset?(RTC(R), EC(R))

    EC_idempotent : LEMMA  EC(EC(R)) = EC(R)

    EC_characterization : LEMMA  equivalence?(S) <=> (S = EC(S))

END relations_closure

quality83%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.