| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/pvs-patches/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 10 kB |
|
Quellcode-Bibliothek rewrite_rules.pvs Sprache: PVS |
|||||||||
|
%%-------------------** Term Rewriting System (TRS) **------------------------
%% %% Authors : Andre Luiz Galdino %% Universidade Federal de Goiás - Brasil %% %% and %% %% Mauricio Ayala Rincon %% Universidade de Brasília - Brasil %% %% Last Modified On: September 29, 2009 %% %%---------------------------------------------------------------------------- rewrite_rules[variable: TYPE+, symbol: TYPE+, arity: [symbol -> nat]]: THEORY BEGIN ASSUMING IMPORTING variables_term[variable,symbol, arity], sets_aux@countability[term], sets_aux@countable_props[term] var_countable: ASSUMPTION is_countably_infinite(V) ENDASSUMING IMPORTING substitution[variable,symbol, arity] l, r: VAR term rho: VAR Ren %%%% Defining rewriting rules in agreement with Baader and Terese %%%%%%%%%%%% rewrite_rule?(l,r): bool = (NOT vars?(l)) & subset?(Vars(r), Vars(l)) rewrite_rule: TYPE = (rewrite_rule?) ren_rewrite: LEMMA rewrite_rule?(l,r) => rewrite_rule?(ext(rho)(l),ext(rho)(r)) %%%% A subset of rewrite rules %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% E: VAR set[rewrite_rule] e: VAR rewrite_rule lhs(e): term = e`1 rhs(e): term = e`2 END rewrite_rules ¤ 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.0.9Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28