products/sources/formale Sprachen/PVS/orders/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: lifted_orders.prf   Sprache: PVS

Original von: PVS©
% two rewrite rules that allow to do skolemization, i.e., to exchange
% quantifiers. These rules come in handy when the outermost quantifier has
% the wrong polarity.
%
% Author: Alfons Geser ([email protected]), National Institute of Aerospace
% Date: Dec 2004

skolemization[D, R: TYPE]: THEORY

BEGIN

  d: VAR D
  r: VAR R
  f: VAR [D -> R]
  p: VAR pred[[D, R]]

  skolemize_exists: THEOREM
    (FORALL d: EXISTS r: p(d,r)) <=> (EXISTS f: FORALL d: p(d,f(d)))

  skolemize_forall: THEOREM
    (EXISTS d: FORALL r: p(d,r)) <=> (FORALL f: EXISTS d: p(d,f(d)))

END skolemization

¤ Dauer der Verarbeitung: 0.17 Sekunden  (vorverarbeitet)  ¤



Druckansicht
unsichere Verbindung
Druckansicht
sprechenden Kalenders

in der Quellcodebibliothek suchen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff