--- pl:miw:miw08_xtt_rif [2008/05/21 20:42]
miw
+++ pl:miw:miw08_xtt_rif [2008/06/01 16:33]
gjn
@@ Linia 1: / Linia 1: @@
-====== Opis ======
-Mateusz Mazur, <m-a-t-i@o2.pl>
-translacja XTTML -> RIF
-====== Spotkania ======
-===== 08.02.26 =====
-wyszukać istniejące:
-  * podejścia do translacji do/z RIF
-  * rozw. translacji dla innych języków regułowych (ruleml?,r2ml?) do/z RIF
-  * [[http://www.w3.org/2005/rules/wg/wiki/R2ML|R2ML i RIF-BLD]] - plany
-  * [[http://www.w3.org/2005/rules/wg/wiki/Implementations/SWRL|SWRL-BLD]] - arkusz XSLT (SWRL->RIF-BLD)
-  * [[http://lists.w3.org/Archives/Public/public-rif-wg/2007Sep/att-0191/RIF-BLD-SyntaxTranslationTable.pdf|Syntax Translation Table]] - pomocne przy translacji pomiędzy zapisem semantycznym a XML'em w BLD
-  * [[http://www.w3.org/2005/rules/wg/wiki/UC10_Worked_Example|Publishing Rules for Interlinked Metadata]] - N3 and SPARQL construct statements (?)
-  * [[http://www.w3.org/2005/rules/wg/wiki/UC9_Worked_Example|BPEL Orchestration of Rule-Based Web Services]]
-  * [[http://www.w3.org/2005/rules/wg/wiki/UC8_Worked_Example|Vocabulary Mapping for Data Integration]]
-  * [[http://www.w3.org/2005/rules/wg/wiki/UC6_Worked_Example|Ruleset Integration for Medical Decision Support]]
-  * [[http://www.w3.org/2005/rules/wg/wiki/UC3_Worked_Example|Collaborative Policy Development for Dynamic Spectrum]]
-===== 08.03.11 =====
-  * zarys pozycji w projekcie
-  * próba bezpośredniego zapisu [[hekate:hekate_case_thermostat|thermostatu]] w RIF (XML)
-  * translacja w.w. przez XSLT do innych syntax
-===== 080401 =====
-  * translacja w.w. przez XSLT do innych syntax
-  * zbadanie mozliwości verbalizacji/wizualizacji [[http://oxygen.informatik.tu-cottbus.de/rewerse-i1/?q=R2ML|podobnie jak w R2ML]]?
-  * czy jest możliwe zapisanie w RIF reguły: if A<3+B then C=B  --- //[[wojnicki@agh.edu.pl|Igor Wojnicki]] 2008/03/12 13:08//
-===== 080408 =====
-  * therm w osobnym pliku upload do wiki
-  * reguła ''if A<3 then C=A+B+4''
-  * zapis w rif [[https://ai.ia.agh.edu.pl/wiki/hekatedev:xtt_minicases]]
-===== 080422 =====
-  * możliwość zapisu:
-    * złożonej konkluzji w postaci ''A^B^...^N''
-    * sterowania wnioskowania w decyzji (idtabeli+idreguły)
-    * wielowartościowych atrybutów: zbiór, lista
-  * FIXME
-===== 080429 =====
-  * freeze
-  * minicases
-  * możliwość bezpośredniego zapisu XTT w RIF
-===== 080520 =====
-    * możliwość bezpośredniego zapisu XTT w RIF ''id'' XML?
-    * w XTT tylko production rules
-    * [[hekate:xtt]]
-===== 080527 =====
-    * przemyśleć ew. trans. xttml->rif
-    * opis "zasadzek" w rif<->xtt, np any, link, etc z odn. do dok rif
-    * metadane w group
-====== Projekt ======
-Elementy przestarzałe zostały przeniesione [[pl:miw:miw08_xtt_rif:obsolate|tutaj]].
-===== Przetestowane narzędzia/podejścia =====
-//których ew. my możemy użyć//
-  * [[http://saxon.sourceforge.net/|SAXON]] translator XSLT zaimplemantowany w JAVA oraz .NET (jest wersja Open Source, która nie zawiera paru dodatkowych funkcji)
-  * [[http://www.gingerall.org/sablotron.html|Sablotron]]
-  * [[http://xml.apache.org/]]
-===== Ciekawe linki =====
-  * [[http://www.w3.org/2005/rules/wg/wiki/Arch/XML_Syntax_Issues_2]]
-====== Sprawozdanie ======
-----
-//W oparciu o dokumentację z 15.04.2008// ({{:pl:miw:miw08_xtt_rif:rif_bld_fld_freez.zip|rif_bld_fld_freez.zip}})
-----
-===== Wprowadzenie do RIF =====
-Format RIF jest ciągle w fazie rozwoju, jedyne dostępne dokumenty są to szkice specyfikacji poszczególnych modułów (Working Draft). Do rozwijanych dokumentów należą m.in. //(istotne według mnie dla projektu)//:
-  * [[http://www.w3.org/2005/rules/wg/draft/rif-fld/|RIF Framework for Logic Dialects]] (status: Editor's Draft)
-  * [[http://www.w3.org/2005/rules/wg/draft/rif-bld/|RIF Basic Logic Dialect]] (status: Editor's Draft)
-Już w obecnej fazie prac, można znaleźć projekty zainteresowane [[http://www.w3.org/2005/rules/wg/wiki/Implementation_plans|wykorzystaniem RIFa]].
-Od strony teoretycznej RIF-BLD (the Basic Logic Dialect of the Rule Interchange Format) odpowiada językowi klauzul Horna z równością oraz standardową semantyką aksjomatyczną (ang. definite Horn rules with equality and with a standard first-order semantics).
-RIF-BLD jest definiowany na dwa sposoby. Po pierwsze jako specjalizacja RIF-FLD (the RIF Framework for Logic-based Dialects) - jest to bardzo zwięzły opis, ale wymaga znajomości [[http://www.w3.org/2005/rules/wg/draft/rif-fld/|RIF-FLD]]. FLD dostarcza ogólnego frameworku - zarówno syntaktycznego i semantycznego, co umożliwia definiowanie dialektów RIFa. Drugi sposób jest to definiowanie RIF-BLD niezależnie od frameworku. Korzyścią tego podejścia jest szybsze pojęcie składni formatu, lecz mniejsza znajomość możliwości jego rozszerzania.
-===== Bezpośrednia specyfikacja składni RIF-BLD =====
-Ten normatywny rozdział, określa składnię RIF-BLD bezpośrednio, bez opierania się na RIF-FLD. Definiuje się składnię prezentacji oraz składnię XML. Składnia prezentacji **nie ma być konkretną składnią** dla RIF-BLD. Jest zdefiniowana przy pomocy języka matematycznego (ang. mathematical English) i powinna być wykorzystywana w przykładach i definicjach. Składnia ta celowo pomija szczegóły, takie jak separatory różnych komponentów syntaktycznych, symboli ucieczki (ang. escape symbols), **parenthesizing**, pierwszeństwo operatorów i podobne. Ponieważ RIF jest formatem wymiany, używa XML jako konkretnej składni.
-==== Alfabet ====
-Alfabet RIF-BLD składa się z dowolnej //(ang. countably infinite)// liczby:
-  * **stałych symboli**: ''Const''
-  * **zmiennych symboli** (rozłącznych z ''Const''): ''Var''
-  * **nazw argumentów** (rozłącznych z ''Const'' i ''Var''): ''ArgNames''
-  * **łączników**: ''And'', ''Or'', '':-''
-  * **kwantyfikatorów**: ''Exists'', ''ForAll''
-  * **symboli**: ''='', ''#'', ''##'', ''->'' oraz ''External''
-  * **symbolu grupującego**: ''Group''
-  * **pomocniczych symboli**: np. "''(''", "'')''", "''[''", "'']''" oraz "''^^''"
-Zbiór łączników, kwantyfikatorów, ''='', itp., jest rozłączny z ''Const'' oraz ''Var''.  Nazwy argumentów w ''ArgNames'' są zapisywane jako stringi w Unicode i nie mogą zaczynać się od "?". Zmienne są zapisywane jako stringi w Unicode poprzedzone przez "?".
-Stałe są zapisywane jako ''"literal"^^symspace'', gdzie ''literal'' jest sekwencją znaków Unicode, a ''symspace'' jest identyfikatorem przestrzeni symboli. Przestrzeni symboli są zdefiniowane w [[http://www.w3.org/2005/rules/wg/draft/ED-rif-fld-20080410/#sec-symbol-spaces|Rozdziale Symbol Spaces ]] [[http://www.w3.org/2005/rules/wg/draft/ED-rif-fld-20080410/|dokumentu RIF-FLD]].
-//Ostatecznie definicja Przestrzeni symboli będzie się znajdować w dokumencie [[http://www.w3.org/2005/rules/wiki/DTB|Data Types and Builtins]].//
-Symbole ''='', ''#'' oraz ''##'' są używane w formułach, które definiują równość, przynależenie do klas oraz związki pomiędzy podklasami. Symbol ''-> '' jest wykorzystywany w termach, które mają nazwane argumenty oraz w formułach ramowych (ang. frame forumula). Symbol ''External'' wskazuje, że formuła atomiczna albo term funkcji (ang. function term) jest zdefiniowany na zewnątrz (np. jest wbudowany).
-Symbol ''Group'' używa się do organizowania reguł RIF-BLD w kolekcje oraz do dodawania adnotacji w postaci meta-danych (ang. annotate them with metadata).
-Język RIF-BLD jest zbiorem formuł zbudowanych przy pomocy alfabetu i zgodnie z regułami podanymi poniżej.
-==== Przestrzenie symboli (z RIF-FLD) ====
-W tym dokumencie będziemy używać następujących prefiksów:
-   * ''xsd:'' oznaczający przestrzeń nazw schematu XML URI [[http://www.w3.org/2001/XMLSchema#]]
-   * ''rdf:'' dla [[http://www.w3.org/1999/02/22-rdf-syntax-ns#]]
-   * ''rif:'' dla URI przestrzeni nazw RIF, [[http://www.w3.org/2007/rif#]]
-Skłania typu ''xsd:string'' powinna być rozumiana jako zwarty URI ([[http://www.w3.org/2005/rules/wg/draft/ED-rif-fld-20080415/diff-since-20080414#ref-curie|CURIE]]) - makro, które jest rozwija związek ciągu znaków oznaczaną przez prefiks ''xsd'' oraz string ''string''. Notacja zwartych URI nie jest częścią składni RIF, lecz zabiegiem zaoszczędzającym miejsce w zapisie.
-Zbiór wszystkich stałych symboli w dialekcie RIF jest podzielony na podzbiory, zwane przestrzeniami symboli, wykorzystywanymi do reprezentowania typów danych w schematach XML, oraz typów danych zdefiniowanych w innych specyfikacjach W3C, jak ''rdf:XMLLiteral''. Są one również używane do odróżniania zbiorów stałych. Wszystkie stałe symbole mają składnię (czasem również semantykę), narzuconą przez przestrzeń symboli, do której należą.
-**Definicja przestrzeni symboli**\\
-Przestrzeń symboli jest nazwanym podzbiorem zbioru wszystkich stałych, ''Const''. Aspekty semantyczne przestrzeni symboli będą opisane w rozdziale [[http://www.w3.org/2005/rules/wg/draft/ED-rif-fld-20080415/diff-since-20080414#sec-fld-semantic-framework|Semantic Framework]]. Każdy symbol z ''Const'' należy do dokładnie jednej przestrzeni symboli.
-Każda przestrzeń symboli posiada związaną przestrzeń leksykalną, unikalny identyfikator oraz, prawdopodobnie, jeden lub więcej alias. Dokładniej:
-    * Przestrzeń leksykalna przestrzeni symboli, jest niepustym zbiorem ciągów znaków (string) Unicode.
-    * Identyfikator przestrzeni symboli jest sekwencją znaków Unicode, które tworzą kompletne IRI.
-    * Alias jest również sekwencją znaków Unicode, ale nie musi mieć postaci kompletnego IRI.
-    * Inne przestrzenie symboli nie mogą posiadać tych samych identyfikatorów czy aliasów.
-Identyfikatory i aliasy przestrzeni symboli nie są same w sobie symbolami stałymi w RIF.
-Aby uprościć język, będziemy często używać identyfikatorów przstrzeni symboli, by odwoływać się do konkretnych przestrzeni (np. zostanie użyte "przestrzeń nazw ''xsd:string''" zamiast "przestrzeń nazw identyfikowana przez ''xsd:string''").
-By odwołać się do stałej w określonej przestrzeni nazw RIF, używamy następującej składni prezentacji:
-<code>"literal"^^symspace</code>
-Gdzie ''literal'' to część leksykalna symbolu, a ''symspace'', jest identyfikatorem lub aliasem przestrzeni symboli. W tym wypadku ''literal'' jest sekwencją znaków Unicode, która musi być elementem z przestrzeni leksykalnej, należącej do przestrzeni symboli ''symspace''. Na przykład ''"1.2"^^xsd:decimal'' oraz ''"1"^^xsd:decimal'' są prawidłowymi symbolami, ponieważ ''1.2'' oraz ''1'' należą do przestrzeni leksykalnej typu danych ''xsd:decimal'' schematu XML. Z drugiej strony ''"a+2"^^xsd:decimal'' nie jest poprawnym symbolem, ponieważ ''a+2'' nie należy do przestrzeni leksykalnej ''xsd:decimal''.
-Zbiór wszystkich przestrzeni symboli, które dzielą ''Const'' jest uważany za część **języka logiki** RIF-FLD.
-==== Termy ====
-RIF-BLD wspiera kilka rodzajów termów: //stałych// i //zmiennych//, //termów pozycjonowanych//, //termów z nazwanymi argumentami//, //równości//, //przynależności do klasy// oraz //formuł atomicznych podklasy//, i //formuły ramowe//. Słowo "term" będzie używane zastępczo do każdego z tych określeń.
-=== Definicja ===
-Podstawową konstrukcją języka są termy. Wyróżniamy:
-  * //Stałe// i //zmienne//. Jeśli ''t'' należy do ''Const'' albo ''t'' należy do ''Var'' to ''t'' jest prostym termem (ang. simple term).
-  * //Termy pozycjonowane (ang. positional terms)//. Jeśli ''t'' należy do ''Const'' oraz ''t_1, ..., t_n'' są termami prostymi, pozycjonowanymi lub z nazwanymi argumentami, to ''t(t_1 ... t_n)'' jest termem pozycjonowanym.
-  * //Termy z nazwanymi argumentami (ang. terms with named arguments)//. Są to termy postaci ''t(s_1->v_1 ... s_n->v_n)'', gdzie ''t'' należy do ''Const'' oraz ''t_1, ..., t_n'' są termami prostymi, pozycjonowanymi lub z nazwanymi argumentami oraz ''s_1, ..., s_n'' są //pairwise//, różnymi symbolami ze zbioru ''ArgNames''.
-Term ''t'' reprezentuje predykat bądź funkcję; ''s_1, ..., s_n'' to nazwy argumentów; ''v_1 , ..., v_n''  - wartości argumentów. Termy z nazwanymi argumentami są jak zwykłe termy pozycjonowane, z tym że argumenty są nazwane a ich kolejność jest nieistotna. Warto zauważyć, że term bez argumentów, np. ''f()'', jest zarówno pozycjonowany jak i z nazwanymi argumentami.
-  * //Termy równościowe (ang. equality terms)//. Jeśli ''t'' oraz ''s'' są termami prostymi, pozycjonowanymi lub z nazwanymi argumentami, to ''t = s'' jest termem równościowym.
-  * //Termy klasyfikujące (ang. class membership terms/just membership terms)//. ''t#s'' jest termem klasyfikującym, jeśli ''t'' oraz ''s'' są termami prostymi, pozycjonowanymi lub z nazwanymi argumentami.
-  * //Termy podklas (ang. subclass terms)//. t##s jest termem podklasy jeśli ''t'' oraz ''s'' są termami prostymi, pozycjonowanymi lub z nazwanymi argumentami.
-  * //Termy ramowe (ang. frame terms)//. ''t[p_1->v_1 ... p_n->v_n]'' jest termem ramowym (ramą) jeśli ''t, p_1, ..., p_n, v_1, ..., v_n'', ''n >= 0'', są termami prostymi, pozycjonowanymi lub z nazwanymi argumentami.
-  * //Termy zdefiniowane zewnętrznie (ang. externally defined terms)//. Jeśli ''t'' jest termem, to ''External(t)'' jest termem zdefiniowanym zewnętrznie.
-Takie termy są wykorzystywane do reprezentowania wbudowanych funkcji oraz predykatów, jak również "dołączanych proceduralnie" termów czy predykatów, które mogą istnieć w różnych systemach regułowych, ale nie są określone przez RIFa.
-Termy klasyfikujące, podklas i ramowe są używane do opisu obiektów i hierarchii klas.
-=== Poprawne formułowanie Termów (Well-formedness of Terms)===
-Zbiór wyszystkich symboli, ''Const'', jest podzielony na:
-    * Pozycjonowane symbole predykatów (ang. positional predicate symbols)
-    * Symbole predykatów z nazwanymi argumentami (ang. predicate symbols with named arguments)
-    * Pozycjonowane symbole funkcji (ang. positional function symbols)
-    * Symbole funkcji z nazwanymi argumentami (ang. function symbols with named arguments)
-    * Osobniki (ang. individuals).
-Symbole w ''Const'', które są wspieranymi przez RIF typami danych są osobnikami.
-Każdy symbol predykatu i funkcji ma dokładnie jedną arność.
-    * Dla symboli pozycjonowanych, arność to nieujemna liczba całkowita (integer), mówiąca ile argumentów dany symbol przyjmuje.
-    * Dla symboli z nazwanymi argumentami, arność jest zbiorem ''{s_1 ... s_k}'' nazw argumentów (''s_i'' należy do ''ArgNames''), które  są dozwolone dla danego symbolu.
-Arność symbolu (czy predykatu, funkcji, bądźor osobnika) nie jest określona w RIF-BLD kategorycznie. Przeciwnie, jest ona wnioskowana jak następuje:
-    * Każdy stały symbol w foirmule RIF-BLD (lub zbiorze formuł) może się pojawić conajwyżej w jednym z kontekstów:
-       * jako osobnik,
-       * jako symbol funkcji o określonej arności
-       * jako symbol predykatu o określonej atności.
-    * Arność symbolu i jego typ jest określany przez jego kontekst.
-    * Jeśli symbol ze zbioru ''Const'' pojawi się więcej niż w jednym kontekście w zbiorze formuł, to zbiór nie jest poprawnie sformułowany w RIF-BLD.
-Dla termu postaci ''External(t)'' bycie dobrze sformułowanym oznacz, że ''t'' musi być instancją [[http://www.w3.org/2005/rules/wg/draft/ED-rif-fld-20080410/#def-fld-external-schema|zewnętrznego schematu (ang. external schema)]], np. schematem zewnętrznie określonego termu, jak to zostało zdefiniowane w [[http://www.w3.org/2005/rules/wg/draft/ED-rif-fld-20080410/#sec-formal-external-schema|Rozdziale Schemas for Externally Defined Terms of RIF-FLD]].
-Jeśli term postaci ''External(p(...))'' pojawi się jako formuła atomiczna, to ''p'' jest uważane za predykat.
-//Definicja zewnętrznych schematów (ang. external schemas) ostatecznie pojawi się w dokumencie [[http://www.w3.org/2005/rules/wiki/DTB|Data Types and Builtins]].//
-==== Formuły ====
-Każdy term (pozycjonowany, lub z nazwanymi argumentami) postaci ''p(...)'' (lub ''External(p(...)''), gdzie ''p'' jest symbolem predykatu, jest również formułą atomiczną. Termy równościowe, klasyfikujące, podklas oraz ramowe również są formułami atomicznymi. Formuła postaci ''External(p(...))'' też jest nazywana zewnętrznie zdefiniowaną formułą atomiczną.
-Proste termy (stałe i zmienne) nie są formułami. Nie wszystkie formuły atomiczne są dobrze sformułowane (ang. well-formed). Dobrze sformułowana formuła atomiczna, to taka, która jest również dobrze sformułowanym termem. Bardziej ogólne formuły są budowane z formuł atomicznych z pomocą łączników logicznych (ang. logical connectives).
-=== Definicja dobrze sformułowanej formuły ===
-Dobrze sformułowana formuła posiada jedną z poniższych postaci:
-   * //Atomiczną (ang. atomic)//: Jeśli ''t'' jest dobrze sformułowaną formułą atomiczną, to jest również dobrze sformułowaną formułą.
-   * //Koniunktywna (ang. conjunction)//: Jeśli ''t_1, ..., t_n'', ''n >= 0'' są dobrze sformułowanymi formułami, to również formuła koniunktywna ''And(t_1 ... t_n)'' jest dobrze sformułowana. W specjalnym przypadku, ''And()'' jest dozwolone i traktowane jako tautologia (ang. tautology), t.j. formuła, która jest zawsze prawdziwa.
-   * //Dysjunktywna (ang. disjunction)//:  Jeśli ''t_1, ..., t_n'', ''n >= 0'' są dobrze sformułowanymi formułami, to również formuła dyjunktywna ''Or(t_1 ... t_n)'' jest dobrze sformułowana. Gdy ''n=0'', dostajemy ''Or()'' jako specjalny przypadek; Jest on traktowany jako it is treated as a zaprzeczenie, t.j. formuła która jest zawsze fałszywa.
-   * //Istnienia (ang. existentials)//: Jeśli ''t'' jest dobrze sformułowaną formułą oraz ''?V_1, ..., ?V_n'' są zmiennymi, wtedy ''Exists ?V_1 ... ?V_n(t)'' jest formułą istnienia.
-Formuły zbudowane z użyciem powyższych definicji są nazywane warunkami RIF-BLD. Następujące formuły prowadzą do pojęcia reguły RIF-BLD:
-   * //Implikacja reguł (ang. rule implication)//: Jeśli ''t'' jest dobrze sformułowaną formułą atomiczną oraz ''p'' jest warunkiem RIF-BLD to ''t :- p'' jest dobrze sformułowaną formułą, nazywaną regułą wynikania (ang. rule implication), pod warunkiem, że ''t'' nie jest zdefiniowane zewnętrznie (t.j. nie ma postaci ''External(...)'').
-   * //Reguła kwantyfikująca (ang. quantified rule)//: Jeśli ''t'' jest regułą wynikania oraz ''?V_1, ..., ?V_n'' są zmiennymi, wtedy ''Forall ?V_1 ... ?V_n(t)'' jest dobrze sformułowaną formułą, nazywaną regułą kawntyfikującą. Wymaga się aby wszystkie wolne (t.j. nie kwantyfikujące) zmienne  w ''t'' pojawiły się w prefiksie ''Forall ?V_1 ... ?V_n''. Reguły kwantyfikujące będą również nazywane jako reguły RIF-BLD.
-   * //Grupa (ang. group)//: Jeśli ''t'' jest ramą oraz ''p_1, ..., p_n'' są regułami RIF-BLD lub grupami formuł (mogą byc wymieszane), to ''Group t (p_1 ... p_n)'' i ''Group (p_1 ... p_n)'' formułami grupowymi.
-Formuły grupowe mają za zadanie reprezentować zbiory reguł z przypisami w meta-danych (ang. annotated with metadata). Te meta-dane są określone przy pomocy opcjonalnego termu ramowego ''t''. Warto zauważyć, że niektóre z ''p_i'' mogą być formułami grupowymi, co oznacza, że grupy mogą być zagnieżdżane. To pozwala na przypisy meta-danych to różnych podzbiorów reguł, które mogą być wewnątrz większych zbiorów reguł, do których też można dołączyć przypisy.
-Z powyższych definicji wynika, że RIF-BLD posiada szeroki wachlarz form syntaktycznych dla termów i formuł. Zapewnia to infrastrukturę dla wymiany językowów regułowych, które wspierają bogate kolekcje form syntaktycznych. Systemy, które nie wspierają części składni bezpośrednio, mogą nadal ją wspierać poprzez transformacje syntaktyczne. Na przykład dysjunkcję w ciele reguły można wyeliminować poprzez standardową transformację, taką, jak zamiana ''p :- Or(q r)'' na parę reguł ''p :- q'', ''p :- r''. Termy z nazwanymi argumentami mogą zostać zredukowane do termów pozycjonowanych poprzez upożądkowanie argumentów po nazwach oraz włączenie ich w nazwę predykatu. Na przykład: ''p(bb->1 aa->2)'' może być przedstawiony jako ''p_aa_bb(2,1)''.
-==== Gramatyka warstwy prezentacji (EBNF) ====
-Analizując zapis RIF w tej notacji, należy pamiętać o kilku rzeczach:
-   * Składnisa logiki pierwszego rzędu (ang. first-order logic) nie jest bezkontekstowa, więc EBNF nie opisuje składni RIF-BLD dokładnie. Na przykład nie da się zapisać reguł dobrego formułowania.
-   * Składnia EBNF nie jest konkretna: nie opisuje szczegółów reprezentowania stałych i zmiennych, nie jest też dostatecznie dokładna co do separatorów. Zamiast tego spacja jest nieformalnie wykotrzystywana jako separator.
-   * Składnia EBNF nie jest normatywna.
-**Definicja języka warunkowego:**
-<code>  FORMULA        ::= 'And' '(' FORMULA* ')' |
-                     'Or' '(' FORMULA* ')' |
-                     'Exists' Var+ '(' FORMULA ')' |
-                     ATOMIC |
-                     'External' '(' ATOMIC ')'
-  ATOMIC         ::= Atom | Equal | Member | Subclass | Frame
-  Atom           ::= UNITERM
-  UNITERM        ::= Const '(' (TERM* | (Name '->' TERM)*) ')'
-  Equal          ::= TERM '=' TERM
-  Member         ::= TERM '#' TERM
-  Subclass       ::= TERM '##' TERM
-  Frame          ::= TERM '[' (TERM '->' TERM)* ']'
-  TERM           ::= Const | Var | Expr | 'External' '(' Expr ')'
-  Expr           ::= UNITERM
-  Const          ::= '"' UNICODESTRING '"^^' SYMSPACE
-  Name           ::= UNICODESTRING
-  Var            ::= '?' UNICODESTRING
-  SYMSPACE       ::= UNICODESTRING</code>
-**Definicja reguł RIF-BLD:**\\
-Składnia prezentacji dla reguł Horna, rozszerza definicje języka warunkowego o następujące produkcje:
-<code>  Group    ::= 'Group' IRIMETA? '(' (RULE | Group)* ')'
-  IRIMETA  ::= Frame
-  RULE     ::= 'Forall' Var+ '(' CLAUSE ')' | CLAUSE
-  CLAUSE   ::= Implies | ATOMIC
-  Implies  ::= ATOMIC ':-' FORMULA</code>
-Przykłady zapisu, można znaleźć [[pl:miw:miw08_xtt_rif:presentation_examples|tutaj]].
-===== Bezpośrednia specyfikacja semantyki RIF-BLD =====
-==== Wartości Prawdy (Truth Values) ====
-Zbiór ''TV'' wartości prawdy w RIF-BLD składa się z dwóch wartości: ''t'' oraz ''f''.
-==== Konstrukcje Semantyczne ====
-Kluczowym pojęciem w modelowo-teoretycznej semntyce języka logiki jest pojęcie struktury semantycznej. Definicja (poniżej) jest trochę ogólniejsza niż to potrzebne. Została tak napisana, aby lepiej można było zrozumieć związek z semantyką framewora RIF.
-**Definicja (Struktura Semantyczna)**\\
-Struktura semantyczna, ''I'', jest to tuple //(ang.)// postaci ''<TV, DTS, D, Dind, Dfunc, IC, IV, IF, Iframe, ISF, Isub, Iisa, I=, Iexternal, Itruth>''. Gdzie ''D'' jest niepustym zbiorem elementów zwanym //domeną ''I'' (ang. domain)//, natomiast ''Dind'', ''Dfunc'' są niepustymi podzbiorami ''D''. ''Ding'' jest używany do interpretowania elementów ''Const'', oznaczających osobniki. ''Dfunc'' zawiera elementy ''Const'' oznaczające symbole funkcyjne. Jak poprzednio, ''Const'' oznacza zbiór wszystkich stałych symboli, a ''Var'' - zbiór wszystkich zmiennych symboli. ''TV'' oznacza zbiór wartości prawdy, których używa struktura semantyczna, a ''DTS'' jest zbiorem prostych typów danych używanych w ''I'' (Rozdział Primitive Data Types w RIF-FLD).
-Pozostałe składowe ''I'' są odwzorowaniami zupełnymi (ang. total mappings) zdefiniowanymi następująco:
-   - ''IC'' odwzorowuje ''Const'' na ''D''. To odwzorowanie objaśnia stałe symbole. Dodatkowo:
-          * Jeśli stała ''c'' należy do ''Const'', oznacza osobnika, to jest wymagane, by ''IC(c)'' należało do ''Dind''.
-          * Jeśli stała ''c'' należy do ''Const'', oznacza symbol funkcyjny (pozycjonowany, lub z nazwanymi argumentami), to jest wymagane, by ''IC(c)'' należało do ''Dfunc''.
-   - ''IV'' odwzorowuje ''Var'' na ''Dind''. To odwzorowanie objaśnia zmienne symbole.
-   - ''IF'' odwzorowuje ''D'' na funkcje ''D*ind -> D'' (tutaj ''D*ind'' jest zbiorem wszystkich sekwencji dowolniej skończonej długości na zbiorze Dind).        To odwzorowanie objaśnia termy pozycjonowane. Dodatkowo:
-          * Jeśli ''d'' należy do ''Dfunc'', to ''IF(d)'' musi być funkcją ''D*ind -> Dind''.
-          * Oznacza to, że kiedy symbol funkcyjny jest stosowany do argumentów, które są osobnymi obiektami, to wynik jest również osobnym obiektem.
-   - ''ISF'' jest zupełnym odwzorowaniem z ''D'' na zbiór zupełny funkcji postaci ''SetOfFiniteSets(ArgNames x Dind) -> D''. To odwzorowanie określa symbole funkcyjne z nazwanymi argumentami. Dodatkowo:
-          * Jeśli ''d'' należy do ''Dfunc'', to ''ISF(d)'' musi być funkcją ''SetOfFiniteSets(ArgNames x Dind) -> Dind''.
-          * Jest to analogiczne do interpretacji termów pozycjonowanych, z dwoma różnicami:          *
-                * Każda para ''<s,v>'' należąca do ''ArgNames x Dind'' reprezentuje pary argument/wartość, zamiast reprezentować tylko wartość w wypadku termu pozycjonowanego.
-                * Argumenty termu z nazwanymi argumentami stanowią skończony zbiór par argumentów/wartości, a nie skończoną listę elementów. Więc kolejność elementów nie ma znaczenia.
-   - ''Iframe'' jest zupełnym odwzorowaniem z ''Dind'' na zupełny zbiór funkcji postaci ''SetOfFiniteBags(Dind x Dind) -> D''.
-           * To odwzorowanie przedstawia termy ramowe. Argument ''d'' należący do ''Dind'' do ''Iframe'' reprezentuje obiekt oraz skończoną rodzinę zbiorów (ang. bag) ''{<a1,v1>, ..., <ak,vk>}'' przedstawiającą rodzinę zbiorów par atrybutów-wartości dla ''d''. Niedługo zobaczymy jak ''Iframe'' jest wykorzystywany do określania oszacowania prawdy termu ramowego (ang. truth valuation of frame terms).
-           * Rodziny zbiorów (multi-zbiory) są tu użyte, ponieważ kolejność par atrybut/wartość w ramie jest nieistotna a pary mogą się powtarzać: ''o[a->b a->b]''. Takie powtórzenia powstają oczywiści kiedy pod zmienne są podstawiane stałe. Na przykład, ''o[?A->?B ?A->?B]'' staje się ''o[a->b a->b]'' jeśli pod zmienną ''?A'' zostanie podstawiony symbol ''a'', a pod ''?B'' symbol ''b''.
-   - ''Isub'' nadaje znaczenie relacji podklasom. Jest to zupełna funkcja ''Dind x Dind -> D''.
-           * Operator ''##'' jest musi być przechodni, t.j., ''c1 ## c2'' i ''c2 ## c3'' z tego musi wynikać ''c1 ## c3''. Jest to zapewnione poprzez obostrzenie w rozdziale dotyczącym interpretacji fotmuł (Interpretation of Formulas).
-   - ''Iisa'' nadaje znaczenie przynależeniu do klas. Jest to zupełna funkcja ''Dind x Dind -> D''.
-           * Przynależności ''#'' oraz ''##'' muszą posiadać własność, że wszyscy członkowie podklasy są również członkami klasy wyżej (ang. superclass), t.j. ''o # cl'' oraz ''cl ## scl'' z tego musi wynikać ''o # scl''. Jest to zapewnione prze obostrzenie w rozdziale dotyczącym interpretacji fotmuł (Interpretation of Formulas).
-  - ''I='' jest to zupełna funkcja ''Dind x Dind -> D''. Daje ona znaczenie operatorowi równości.
-  - ''Itruth'' jest zupełnym odwzorowaniem ''D -> TV''. Jest wykorzystywane do definiowania oceny prawdziwości formuł.
-  - ''Iexternal'' to odwzorowanie z koherentnego zbioru schematów (ang. schemas) dla zewnętrznie zdefiniowanych funkcji, do funkcji zupełnych ''D* -> D''. Dla każdego zewnętrznego schematu ''s = (?X1 ... ?Xn; t)''  w koherentnym zbiorze takich schematów związanych z językiem, ''Iexternal(s)'' jest funkcją postaci ''Dn -> D''.
-          * Dla każdego zewnętrznego schematu ''s'', związanego z językiem, zakłada się, że ''Iexternal(s)'' jest określone w jakimś zewnętrznym dokumencie (stąd nazwa zewnętrzny schemat). W szczególności, jeśli s jest schematem wbudowanego predykatu lub funkcji RIFa, ''Iexternal(s)'' jest określone w dokumencie Data Types and Builtins, po to aby:
-               * Jeśli ''s'' jest schematem wbudowanej funkcji, to ''Iexternal(s)'' musi być funkcją zdefiniowaną we wspomnianym dokumencie.
-               * Jeśli ''s'' jest schematem wbudowanego predykatu, to ''Itruth ο (Iexternal(s))'' (złożenie ''Itruth'' i ''Iexternal(s)'', funkcja prawdziwa) musi być określona w Data Types and Builtins.
-Dla wygody zostały również zdefiniowane odwzorowania ''I'' z termów na ''D'':
-    * ''I(k) = IC(k)'', jeśli ''k'' jest symbolem ze zbioru ''Const''
-    * ''I(?v) = IV(?v)'', jeśli ''?v'' jest symbolem ze zbioru ''Var''
-    * ''I(f(t1 ... tn)) = IF(I(f))(I(t1),...,I(tn))''
-    * ''I(f(s1->v1 ... sn->vn)) = ISF(I(f))({<s1,I(v1)>,...,<sn,I(vn)>})'' - Tutaj używamy ''{...}'' aby oznaczyć zbiór par argumentów/wartości.
-    * ''I(o[a1->v1 ... ak->vk]) = Iframe(I(o))({<I(a1),I(v1)>, ..., <I(an),I(vn)>})'' - Tutaj używamy ''{...}'' aby oznaczyć worek par atrybutów/wartości.
-    * ''I(c1##c2) = Isub(I(c1), I(c2))''
-    * ''I(o#c) = Iisa(I(o), I(c))''
-    * ''I(x=y) = I=(I(x), I(y))''
-    * ''I(External(t)) = Iexternsl(σ)(I(s1), ..., I(sn))'', jeśli ''t'' jest instancją zewnętrznego schematu ''s = (?X1 ... ?Xn; t)'' przez podstawienie ''?X1/s1 ... ?Xn/s1''.
-Warto zauważyć, że z definicji, ''External(t)'' jest dobrze sformułowany tylko, jeśli ''t'' jest instancją zewnętrznego schematu. Ponadto, z definicji koherentnych zbiorów zewnętrznych schematów, wynika, że ''t'' może być instancją co najwyżej jednego schematu, aby ''I(External(t))'' było dobrze sformułowane.
-**Wynik typów danych (ang. The effect of data types)**. Typy danych w **DTS** nakładają bastępujące ograniczenia. Jeśli ''dt'' jest identyfikatorem przestrzeni symboli typów danych, niech ''LSdt'' oznacza leksykalną przstrzeń ''dt'', ''VSdt'' oznacza przestrzeń wartości oraz ''Ldt'': ''LSdt -> VSdt'' odwzorowanie przstrzeni leksykalnej w przestrzeń wartości (definicje tych pojęć są w rozdziale [[http://www.w3.org/2005/rules/wg/draft/ED-rif-fld-20080410/#sec-data-types|Primitive Data Types]], RIF-FLD). To musi być zachowane:
-    * ''VSdt'' jest podzbiorem lub równa się  ''Dind''; oraz
-    * Dla każdej stałej ''"lit"^^dt'' należy do ''LSdt'', ''IC("lit"^^dt) = Ldt(lit)''.
-To znaczy, że ''IC'' musi odwzorowywać stałe typów danych zgodnie z ''Ldt''.
-RIF-BLD nie nakłada ograniczeń na ''IC'' dla stałych w przestrzni leksykalnej, które nie odpowiadają podstawowym typom danych w ''DTS''.
-==== Interpretacja Formuł ====
-**Definicja oszacowania prawdy (ang. Truth valuation)**\\
-Oszacowanie prawdy dla dobrze sformułowanej formuły w RIF-BLD jest wyznaczane przy pomocy następującej funkcji, oznaczanej jako ''TValI'':
-   - Pozycjonowane formuły atomiczne: ''TValI(r(t1 ... tn)) = Itruth(I(r(t1 ... tn)))''.
-   - Formuły atomiczne z nazwanymi argumentami: ''TValI(p(s1->v1 ... sk->vk)) = Itruth(I(p(s1->v1 ... sk->vk)))''.
-   - Równość: ''TValI(x = y) = Itruth(I(x = y))''.
-          * Aby zapewnić, że równość ma spodziewne własności, wymagane jest by:
-               * ''Itruth(I(x = y)) = t'' wtedy i tylko wtedy, gdy ''I(x) = I(y)'' oraz, że ''Itruth(I(x = y)) = f'' w przeciwnym razie.
-          * Jest to równoważne powiedzeniu, że ''TValI(x = y) = t if I(x) = I(y)''.
-   - Podklasa: ''TValI(sc ## cl) = Itruth(I(sc ## cl))''.
-          * Aby zapewnić, żeby operator ''##''był przechodni, musi być spelnione:
-               * Dla wszystkich ''c1, c2, c3'' należących do ''D'', jeśli ''TValI(c1 ## c2) = TValI(c2 ## c3) = t'' to ''TValI(c1 ## c3) = t''.
-   - Przynależność: ''TValI(o # cl) = Itruth(I(o # cl))''.
-          * Aby zapenić, że wszyscy członkowie podklas, są też członkami klasy głównej, wymagane jest:
-               * Dla wszystkich ''o, cl, scl'' należących do ''D'', jeśli ''TValI(o # cl) = TValI(cl ## scl) = t'' to ''TValI(o # scl) = t''.
-   - Rama: ''TValI(o[a1->v1 ... ak->vk]) = Itruth(I(o[a1->v1 ... ak->vk]))''.
-          * Ponieważ rózne pary atrybut/wartość powinny być rozumiane jako kombinacje, wymaga się by:
-               * ''TValI(o[a1->v1 ... ak->vk]) = t'' wtedy i tylko wtedy, gdy ''TValI(o[a1->v1]) = ... = TValI(o[ak->vk]) = t''.
-   - Zewnętrznie zdefiniowana formuła atomiczna: ''TValI(External(t)) = Itruth(Iexternal(s)(I(s1), ..., I(sn)))'', jeśli ''t'' jest formułą atomiczną, która jest instancją zewnętrznego schematu ''s = (?X1 ... ?Xn; t)'' poprzez podstawienie ''?X1/s1 ... ?Xn/s1''.
-          * Warto zauważyć, że zgodnie z definicją, ''External(t)'' jest dobrze sformułowany, jeśli ''t'' jest instancją zewnętrznego schematu. Ponadto, z definicji koherentnych zbiorów zewnętrznych schematów, ''t'' może być instancją co najwyżej jednego schemtu, aby ''I(External(t))'' było dobrze sformułowane.
-  - Koniunkcja: ''TValI(And(c1 ... cn)) = t'' wtedy i tylko wtedy, gdy ''TValI(ci) = t'', dla wszystkich ''i = 1, ..., n''. W innym wypadku, ''TValI(And(c1 ... cn)) = f''.
-          * Pusta koniunkcja jest traktowana jako tautologia, więc ''TValI(And()) = t''.
-   - Alternatywa (Dysjunkcja): ''TValI(Or(c1 ... cn)) = f'' wtedy i tylko wtedy, gdy ''TValI(ci) = f'', dla wszystkich ''i = 1, ..., n''. W innym wypadku, ''TValI(And(c1 ... cn)) = t''.
-  - Kwantyfikacja:
-          * ''TValI(Exists ?v1 ... ?vn (s)) = t'' wtedy i tylko wtedy, gdy dla pewnego ''I*'', opisanego poniżej, ''TValI*(s) = t''.
-          * ''TValI(Forall ?v1 ... ?vn (s)) = t'' wtedy i tylko wtedy, gdy dla każego ''I*'', opisanego poniżej, ''TValI*(s) = t''.
-          * ''I*'' jest to struktura semantyczna postaci ''<TV, DTS, D, Dind, Dfunc, IC, I*V, IF, Iframe, ISF, Isub, Iisa, I=, Iexternsl, Itruth>'',  która jest identyczna z ''I'', poza tym, że odwzorowanie ''I*V'', jest uzywane zamiast ''IV''. ''I*V'' jest zdefiniowane  tak, by pokrywać się z ''IV'' na wszystkich zmienny poza //, possibly, on ''?v1,...,?vn''//.
-  - Implikacja reguł:
-          * ''TValI(conclusion :- condition) = t'', jeśli ''TValI(conclusion)=t'' lub ''TValI(condition)=f''.
-          * ''TValI(conclusion :- condition) = f'' w innym wypadku.
-  - Grupy reguł:
-          * Jeśli ''P'' jest grupową formułą postaci ''Group t (s1 ... sn)'' lub ''Group (s1 ... sn)'' to:
-              * ''TValI(P) = t'' wtedy i tylko wtedy, gdy ''TValI(s1) = t, ..., TValI(sn) = t''.
-              * ''TValI(P) = f'' w innym wypadku.
-          * Oznacza to, że grupa reguł jest traktowana jako kombinacja. Meta-dane są ignorowane na potrzeby semantyki RIF-BLD.
-**Model** grupy reguł, ''P'', jest strukturą semantyczną ''I'' taką, że ''TValI(P) = t''. W takim wypadku piszemy ''I |= P''.
-==== Logical Entailment ====
-Pomimo, że meta-dane, związane z formułami RIF-BLD są ignorowane przez semantykę, mogą być wydobyte poprzez narzędzia XML'a. Ponieważ meta-dane są przedstawiane za pomocą termów ramowych, mogą być uzasadnione regułami RIF-BLD.
-===== Serializacja XML RIFa =====
-Wszystkie tagi XML są podzielone na:
-   * deskryptory klas (ang. class descriptors), zwane tagami typów (type tags),
-   * deskryptory właściwości (ang. property descriptors), zwane tagami ról (role tags).
-Będziemy używać nazw napisanych dużymi literami dla tagów typów, oraz małymi literami dla tagów ról.
-==== Zapis w XML języka warunkowego ====
-Wykorzystujemy następujące tagi:
-<code>- And       (conjunction)
-- Or        (disjunction)
-- Exists    (quantified formula for 'Exists', containing declare and formula roles)
-- declare   (declare role, containing a Var)
-- formula   (formula role, containing a FORMULA)
-- Atom      (atom formula, positional or with named arguments)
-- External  (external call, containing a content role)
-- content   (content role, containing an Atom, for predicates, or Expr, for functions)
-- Member    (member formula)
-- Subclass  (subclass formula)
-- Frame     (Frame formula)
-- object    (Member/Frame role, containing a TERM or an object description)
-- op        (Atom/Expr role for predicates/functions as operations)
-- arg       (positional argument role)
-- upper     (Member/Subclass upper class role)
-- lower     (Member/Subclass lower instance/class role)
-- slot      (Atom/Expr/Frame slot role, containing a Prop)
-- Prop      (Property, prefix version of slot infix '->')
-- key       (Prop key role, containing a Const)
-- val       (Prop val role, containing a TERM)
-- Equal     (prefix version of term equation '=')
-- Expr      (expression formula, positional or with named arguments)
-- side      (Equal left-hand side and right-hand side role)
-- Const     (individual, function, or predicate symbol, with optional 'type' attribute)
-- Name      (name of named argument)
-- Var       (logic variable)</code>
-Składnie XML dla przestrzeni symboli wykorzystuje atrybut typu, związany z elementami termów, jak ''Const''. Na przykład ''<Const type="xsd:dateTime">2007-11-23T03:55:44-02:30</Const>''.
-**//[[pl:miw:miw08_xtt_rif:przyklad3|Przykład 3a]]//**\\
-Przykład ten obrazuje serializację XML dla warunkór RIFa.
-**//[[pl:miw:miw08_xtt_rif:przyklad3b|Przykład 3b]]//**\\
-Opisuje serializację warunku RIF, zawierającego termy z nazwanymi argumentami.
-==== Zapis w XML języka reguł ====
-Jest to rozszerzenie języka warunkowego, o:
-<code>- Group    (nested collection of sentences annotated with metadata)
-- meta     (meta role, containing metadata, which is represented as a Frame)
-- sentence (sentence role, containing RULE or Group)
-- Forall   (quantified formula for 'Forall', containing declare and formula roles)
-- Implies  (implication, containing if and then roles)
-- if       (antecedent role, containing FORMULA)
-- then     (consequent role, containing ATOMIC)</code>
-**//[[pl:miw:miw08_xtt_rif:przyklad|Przykład]]//**\\
-Przykład prezentuje serializację reguły z [[pl:miw:miw08_xtt_rif:presentation_examples|przykładu 3]], dotyczącego warstwy prezentacji.
-==== Translacja pomiędzy składnią prezentacji a zapisem XML ====
-Bardzo przejrzysty opis translacji pomiedzy tymi dwoma rodzajami zapisu jest umieszczony w [[http://www.w3.org/2005/rules/wg/draft/rif-bld/#Translation_Between_the_RIF-BLD_Presentation_and_XML_Syntaxes|dokumentacji do RIF-BLD]]. Jest on na tyle przejrzysty, że nie wymaga tłumaczenia na język polski.
-===== Thermostat w RIF =====
-Przykład reguł [[hekate:hekate_case_thermostat|termostatu]], zapisany za pomocą składni XML formatu RIF, znajduje się [[pl:miw:miw08_xtt_rif:thermostat|tutaj]]. Plik XML z thrermostatem: {{:pl:miw:miw08_xtt_rif:thermostat_v2.xml|thermostat_v2.xml}}.
-===== Próba werbalizacji RIF'a na przykładzie thermostatu  =====
-Opierając się o zapisane reguły thermostatu w RIF, udało mi się za pomocą XSLT wykonać prostą werbalizację:
-<file>
-If dayofweek is Monday or dayofweek is Tuesday or dayofweek is Wednesday or dayofweek is Thursday or dayofweek is Friday
-then thrm:is-workday( var dayofweek).
-If dayofweek is Saturday or dayofweek is Sunday
-then thrm:is-weekend( var dayofweek).
-If thrm:is-weekend(External fn:get-dayOfWeek-from-DateTime(var today)) is true
-And External op:numeric-between(External fn:hours-from-dateTime(var today), 9am, 5pm) is true
-then thrm:is-during-business-hours( var today).
-If thrm:is-workday(External fn:get-dayOfWeek-from-DateTime(var today)) is true
-And External op:numeric-less-than(External fn:hours-from-dateTime(var today), 9am) is true
-then thrm:is-not-during-business-hours(var today).
-If thrm:is-workday(External fn:get-dayOfWeek-from-DateTime(var today)) is true
-And External op:numeric-greater-than(External fn:hours-from-dateTime(var today), 5pm) is true
-then thrm:is-not-during-business-hours( var today).
-If thrm:is-weekend(External fn:get-dayOfWeek-from-DateTime(var today)) is true
-then thrm:is-not-during-business-hours(var today).
-If month is January or month is February or month is December then thrm:is-summer(var month).
-If month is March or month is April or month is May then thrm:is-atumn(var month).
-If month is June or month is July or month is August then thrm:is-winter(var month).
-If month is September or month is October or month is November then thrm:is-spring(var month).
-If thrm:is-spring(External fn:month-from-dateTime(var date)) is true
-And thrm:is-during-buisness-hours(var date) is true then thrm:thermostat-setting(20).
-If thrm:is-spring(External fn:month-from-dateTime(var date)) is true
-And thrm:is-not-during-buisness-hours(var date) is true then thrm:thermostat-setting(15).
-If thrm:is-summer(External fn:month-from-dateTime(var date)) is true
-And thrm:is-during-buisness-hours(var date) is true then thrm:thermostat-setting(24).
-If thrm:is-summer(External fn:month-from-dateTime(var date)) is true
-And thrm:is-not-during-buisness-hours(var date) is true then thrm:thermostat-setting(27).
-If thrm:is-atumn(External fn:month-from-dateTime(var date)) is true
-And thrm:is-during-buisness-hours(var date) is true then thrm:thermostat-setting(20).
-If thrm:is-atumn(External fn:month-from-dateTime(var date)) is true
-And thrm:is-not-during-buisness-hours(var date) is true then thrm:thermostat-setting(16).
-If thrm:is-winter(External fn:month-from-dateTime(var date)) is true
-And thrm:is-during-buisness-hours(var date) is true
-then thrm:thermostat-setting(18).
-If thrm:is-winter(External fn:month-from-dateTime(var date)) is true
-And thrm:is-not-during-buisness-hours(var date) is true then thrm:thermostat-setting(14).</file>
-Treść arkusza XSLT znajduje się [[pl:miw:miw08_xtt_rif:verb|tutaj]]. Plik do pobrania: {{:pl:miw:miw08_xtt_rif:rifverb.xml|RIFverb.xml}}
-===== Próba wizualizacji reguł RIF'a na przykładzie thermostatu  =====
-Kolejną podjętą przeze mnie próbą było wizualizowanie reguł.\\
-{{:pl:miw:miw08_xtt_rif:rifvis.png|:pl:miw:miw08_xtt_rif:rifvis.png}}\\
-Arkusz XSLT służący do wizualizacji znajduje się [[pl:miw:miw08_xtt_rif:visual|tutaj]]. Plik do pobrania: {{:pl:miw:miw08_xtt_rif:rifvis.xml|RIFvis.xml}}
-===== XTT Minicases =====
-[[pl:miw:miw08_xtt_rif:rif_minicases|Analiza i próba zapisu za pomocą RIFa.]]
-**Wnioski:**
-   * Aby konkluzja mogła składać się z więcej niż jednego predykatu/zmiennej, trzeba stworzyć predykat, który to umożliwi.
-   * Do sterowanie wnioskami można wykorzystać właściwość języka XML - nadawać elementom ''Group'' oraz ''sentence'' identyfikatory za pomocą ''id'' i odwoływać się do nich w jakimś predykacie (nie znalazłem informacji, żeby nie można było użyć ''id'').
-   * Do zapisu wielowartościowych atrybutów proponuję:
-      * **termy z nazwanymi argumentami** dla zbiorów wartości.
-      * **termy pozycjonowane** dla list wartości.
-===== RIF a XTTML =====
-Wstępne przmyślenia:
-   * Do nadania identyfikatorów posłuży element spoza RIF, należący do języka XML - ''id''.
-==== Proponowany zapis ====
-<code xml>
-<Group id="xtt_table1"> <!-- definicja tabeli xtt -->
- <sentence id="xtt_table_row1"> <!-- definicja wiersza tabeli -->
-  <Implies>
-   <if>
-    <!-- warunki łączone za pomocą 'and' bądź 'or' -->
-   </if>
-   <then>
-    <Atom> <!-- specjalny predykat, sugerujący następną regułę/tablicę i wywołujący inne predykaty -->
-     <op><Const type="rif:iri">xtt:concl</Const></op>
-     <arg>
-      <Atom> <!-- predykat podajacy wartosci 'id' nastepnej tablicy/wiersza -->
-       <op><Const type="rif:iri">xtt:next_table_rule</Const></op>
-       <arg><Const type="xsd:string">xtt_table1</Const></arg>
-       <arg><Const type="xsd:string">xtt_table_row1</Const></arg>
-      </Atom>
-     </arg>
-     <arg>
-      <!-- albo predykat do wywołania, albo predykat xtt:run_many wywołujący więcej niż jeden predykat -->
-     </arg>
-    </Atom>
-   </then>
-  </Implies>
- </sentence>
- <sentence id="xtt_table_row2">
-  ...
- </sentence>
- ...
-</Group></code>
-=== Niuanse zapisu XTT w RIF ===
-Jeśli któryś z wierszy ma być zawsze wykonywany (dla dowolnej wartości zmiennej na wejściu), to część warunkowa powinna wyglądać następująco:
-<code xml>
-<if>
- <And></And>
-</if></code>
-Pusty ''And'' zwraca zawszę prawdę. ([[pl:miw:miw08_xtt_rif#formuly|Patrz rozdział Formuły: Dobrze sformułowane formuły]])
-Parametry ''id'' zostały dodane do tag'ów ''Group'' oraz ''sentence''. Ich zadaniem jest oznaczenie poszczególnych tablic i wierszy, aby można było sterować wnioskowaniem (XTT link). Do sterowania wnioskowaniem w części wynikowej reguły używany jest predykat ''xtt:concl/2'' pierwszy argument to ''xtt:next_table_rule/2'' lub ''xtt:next_table/1''. Drugim argumentem jest wywołanie dowolnego predykatu. Aby wywołać więcej niż jeden, można użyć ''xtt:run_many''.
-**Uwagi**\\
-  * Każda tablica (element ''Group'') musi być w osobnym pliku (zgodność z plikami xsd).
-=== Przykład 1: calculations (factorial) ===
-<code>
-|----------------------------------------------------|
-|                                                    |
-|   x s  || s                                        |
-|->------------             x   y   s   ||  y        |
-      NA ||=x   --+------> -------------------       |
-      >0 ||=s-1 --|                     ||           |
-                            >0     >0   || =y*s -----|
-                            =0          ||  =1  -----------|
-                            >0     =1   ||      -----------+------>
-</code>
-<code xml>
-<Group id="xtt_table1">
- <sentence id="xtt_table1_row1">
-  <Implies>
-   <if>
-    <External>
-     <content>
-      <Atom>
-       <op><Const type="rif:iri">fn:is_empty</Const></op>
-       <arg><Var>x</Var></arg>
-      </Atom>
-     </content>
-    </External>
-   </if>
-   <then>
-    <Atom>
-     <op><Const type="rif:iri">xtt:concl</Const></op>
-     <arg>
-      <External>
-       <content>
-        <Expr>
-         <op><Const type="rif:iri">xtt:next_table</Const></op>
-         <arg><Const type="xsd:string">xtt_table2</Const></arg>
-        </Expr>
-       </content>
-      </External>
-     </arg>
-     <arg>
-      <External>
-       <content>
-        <Expr>
-         <op><Const type="rif:iri">op:assign</Const></op>
-         <arg><Var>s</Var></arg>
-         <arg><Var>x</Var></arg>
-        </Expr>
-       </content>
-      </External>
-     </arg>
-    </Atom>
-   </then>
-  </Implies>
- </sentence>
- <sentence id="xtt_table1_row2">
-  <Implies>
-   <if>
-    <External>
-     <content>
-      <Atom>
-       <op><Const type="rif:iri">op:numeric-greater-than</Const></op>
-       <arg><Var>s</Var></arg>
-       <arg><Const type="xsd:decimal">0</Const></arg>
-      </Atom>
-     </content>
-    </External>
-   </if>
-   <then>
-    <Atom>
-     <op><Const type="rif:iri">xtt:concl</Const></op>
-     <arg>
-      <External>
-       <content>
-        <Expr>
-         <op><Const type="rif:iri">xtt:next_table</Const></op>
-         <arg><Const type="xsd:string">xtt_table2</Const></arg>
-        </Expr>
-       </content>
-      </External>
-     </arg>
-     <arg>
-      <External>
-       <content>
-        <Expr>
-         <op><Const type="rif:iri">op:assign</Const></op>
-         <arg><Var>s</Var></arg>
-         <arg>
-          <External>
-           <content>
-            <Expr>
-             <op><Const type="rif:iri">op:numeric-substract</Const></op>
-             <arg><Var>s</Var></arg>
-             <arg><Const type="xsd:decimal">1</Const></arg>
-            </Expr>
-           </content>
-          </External>
-         </arg>
-        </Expr>
-       </content>
-      </External>
-     </arg>
-    </Atom>
-   </then>
-  </Implies>
- </sentence>
-</Group>
-<Group id="xtt_table2">
- <sentence id="xtt_table2_row1">
-  <Implies>
-   <if>
-    <And>
-     <formula>
-      <External>
-       <content>
-        <Atom>
-         <op><Const type="rif:iri">op:numeric-greater-than</Const></op>
-         <arg><Var>x</Var></arg>
-         <arg><Const type="xsd:decimal">0</Const></arg>
-        </Atom>
-       </content>
-      </External>
-     </formula>
-     <formula>
-      <External>
-       <content>
-        <Atom>
-         <op><Const type="rif:iri">op:numeric-greater-than</Const></op>
-         <arg><Var>s</Var></arg>
-         <arg><Const type="xsd:decimal">0</Const></arg>
-        </Atom>
-       </content>
-      </External>
-     </formula>
-    </And>
-   </if>
-   <then>
-    <Atom>
-     <op><Const type="rif:iri">xtt:concl</Const></op>
-     <arg>
-      <External>
-       <content>
-        <Expr>
-         <op><Const type="rif:iri">xtt:next_table</Const></op>
-         <arg><Const type="xsd:string">xtt_table1</Const></arg>
-        </Expr>
-       </content>
-      </External>
-     </arg>
-     <arg>
-      <External>
-       <content>
-        <Expr>
-         <op><Const type="rif:iri">op:assign</Const></op>
-         <arg><Var>y</Var></arg>
-         <arg>
-          <External>
-           <content>
-            <Expr>
-             <op><Const type="rif:iri">op:numeric-multiply</Const></op>
-             <arg><Var>y</Var></arg>
-             <arg><Var>s</Var></arg>
-            </Expr>
-           </content>
-          </External>
-         </arg>
-        </Expr>
-       </content>
-      </External>
-     </arg>
-    </Atom>
-   </then>
-  </Implies>
- </sentence>
- <sentence id="xtt_table1_row2">
-  <Implies>
-   <if>
-    <Equal>
-     <side><Var>x</Var></side>
-     <side><Const type="xsd:decimal">0</Const></side>
-    </Equal>
-   </if>
-   <then>
-    <Atom>
-     <op><Const type="rif:iri">xtt:run_many</Const></op>
-     <arg>
-      <External>
-       <content>
-        <Expr>
-         <op><Const type="rif:iri">op:assign</Const></op>
-         <arg><Var>y</Var></arg>
-         <arg><Const type="xsd:decimal">1</Const></arg>
-        </Expr>
-       </content>
-      </External>
-     </arg>
-     <arg>
-      <External>
-       <content>
-        <Expr>
-         <op><Const type="rif:iri">xtt:return</Const></op>
-         <arg><Var>s</Var></arg>
-         <arg><Var>x</Var></arg>
-         <arg><Var>y</Var></arg>
-        </Expr>
-       </content>
-      </External>
-     </arg>
-    </Atom>
-   </then>
-  </Implies>
- </sentence>
- <sentence id="xtt_table2_row3">
-  <Implies>
-   <if>
-    <And>
-     <formula>
-      <External>
-       <content>
-        <Atom>
-         <op><Const type="rif:iri">op:numeric-greater-than</Const></op>
-         <arg><Var>x</Var></arg>
-         <arg><Const type="xsd:decimal">0</Const></arg>
-        </Atom>
-       </content>
-      </External>
-     </formula>
-     <formula>
-      <Equal>
-       <side><Var>s</Var></side>
-       <side><Const type="xsd:decimal">1</Const></side>
-      </Equal>
-     </formula>
-    </And>
-   </if>
-   <then>
-    <Atom>
-     <op><Const type="rif:iri">xtt:return</Const></op>
-     <arg><Var>s</Var></arg>
-     <arg><Var>x</Var></arg>
-     <arg><Var>y</Var></arg>
-    </Atom>
-   </then>
-  </Implies>
- </sentence>
-</Group>
-</code>
-Obie tablice w formacie xml: {{:pl:miw:miw08_xtt_rif:factorial.xml|factorial.xml}}, {{:pl:miw:miw08_xtt_rif:factorial1.xml|factorial1.xml}}
-----
-Powyższy przykład został zwalidowany za pomocą dostępnych arkuszy XSD. Jedyny element, który zgłasza błędy jest to parametr ''id'', aczkolwiek ze względu na brak walidacji niektórych przykładów obecnych w dokumentacji, nie należy się tym przejmować. Nigdzie w dokumentacji nie ma wyraźnego zakazu wykorzystywania elementów standardu XML.
-==== Translacja XTTML => RIF ====
-Po zaproponowaniu wstępnej postaci zapisu XTT w RIF, nadszedł czas na stowrzenie translatora [[hekate:hekate_markup_language#xttml|XTTML]] => RIF.
-Translator można pobrać tutaj: {{:pl:miw:miw08_xtt_rif:xtttorif.xml|XTTtoRIF.xml}}.
-Sposób zapisu w RIFie mniejwiecej zgadza się z przedstawionym powyżej. Dokonałem jedynie pewnych uproszczeń, ułatwiających translacje. Za pomocą powyższego arkusza XSLT dokonałem translacji [[hekate:hekate_markup_language#xttml|przykładu]], która znajduje się [[pl:miw:miw08_xtt_rif:xtt2rif|tutaj]]. Z powodu składni RIFa stosunkowo prosty i czytelny przykład rozrósł się dość znacznie.
-====== Materiały ======
-XSLT:
-   * [[http://www.w3schools.com/xsl/default.asp|W3 Shools]]
-RIF:
-   * [[http://www.w3.org/2005/rules/wiki/RIF_Working_Group|RIF Working Group]]
-   * [[http://oxygen.informatik.tu-cottbus.de/rewerse-i1/?q=RIF|Oxygen Informatik]]

pl/miw/miw08_xtt_rif.txt · ostatnio zmienione: 2019/06/27 15:50 (edycja zewnętrzna)

Pokaż stronę Poprzednie wersje

Menadżer multimediów Do góry

AIwiki

Menu

Dla Studentów

Old specialized AI courses

SMaDA/SMaIDA/AIDA

Informatyka (EAIiIB)

Studia Dr

Inne materialy dydaktyczne

Archiwum

Dyplomanci

Geist Season of Code

HeKatE

Public

Różnice