Różnice

Różnice między wybraną wersją a wersją aktualną.

Odnośnik do tego porównania

Both sides previous revision Poprzednia wersja
Nowa wersja
Poprzednia wersja
pl:miw:miw08_xtt_rif [2008/05/28 11:36]
miw
pl:miw:miw08_xtt_rif [2019/06/27 15:50] (aktualna)
Linia 1: Linia 1:
 ====== Opis ====== ====== Opis ======
 +__**Projekt zakończony**__
 +
 Mateusz Mazur, <​m-a-t-i@o2.pl>​ Mateusz Mazur, <​m-a-t-i@o2.pl>​
  
Linia 8: Linia 10:
   * Elementy przestarzałe zostały przeniesione [[pl:​miw:​miw08_xtt_rif:​obsolate|tutaj]].   * Elementy przestarzałe zostały przeniesione [[pl:​miw:​miw08_xtt_rif:​obsolate|tutaj]].
   * :​!:​**[[pl:​miw:​miw08_xtt_rif:​spotkania|Spotkania]]**.   * :​!:​**[[pl:​miw:​miw08_xtt_rif:​spotkania|Spotkania]]**.
-  * [[http://​saxon.sourceforge.net/​|SAXON]] translator XSLT zaimplemantowany ​w JAVA oraz .NET (jest wersja Open Source, która nie zawiera paru dodatkowych funkcji)+  * [[http://​saxon.sourceforge.net/​|SAXON]] translator XSLT zaimplementowany ​w JAVA oraz .NET (jest wersja Open Source, która nie zawiera paru dodatkowych funkcji)
   * [[http://​www.gingerall.org/​sablotron.html|Sablotron]]   * [[http://​www.gingerall.org/​sablotron.html|Sablotron]]
   * [[http://​xml.apache.org/​]]   * [[http://​xml.apache.org/​]]
   * :​!:​**[[http://​www.w3.org/​2005/​rules/​wg/​wiki/​Arch/​XML_Syntax_Issues_2]]**   * :​!:​**[[http://​www.w3.org/​2005/​rules/​wg/​wiki/​Arch/​XML_Syntax_Issues_2]]**
 +
  
 ====== Sprawozdanie ====== ====== Sprawozdanie ======
Linia 17: Linia 20:
 //W oparciu o dokumentację z 15.04.2008//​ ({{:​pl:​miw:​miw08_xtt_rif:​rif_bld_fld_freez.zip|rif_bld_fld_freez.zip}}) //W oparciu o dokumentację z 15.04.2008//​ ({{:​pl:​miw:​miw08_xtt_rif:​rif_bld_fld_freez.zip|rif_bld_fld_freez.zip}})
 ---- ----
 +  * 08.05.18 - nowy szkic specyfikacji. Nowości:
 +    * Dokument: [[http://​www.w3.org/​2005/​rules/​wg/​draft/​ED-rif-dtb-20080518/​|RIF Data Types and Built-Ins]]
 +    * Dokument: [[http://​www.w3.org/​2005/​rules/​wg/​draft/​ED-rif-ucr-20080518/​|RIF Use Cases and Requirements]] ​
 +    * Rozdział w RIF-BLD: [[http://​www.w3.org/​2005/​rules/​wg/​draft/​ED-rif-bld-20080518/​diff-since-20080415#​Interpretation_of_Documents|Interpretation of Documents]]
 +    * BLD: zmiany w opisie termów
 +    * BLD: zmiany w opisie dobrze sformułowanych formuł
 +    * BLD: zmiany w gramatyce
  
 ===== Wprowadzenie do RIF ===== ===== Wprowadzenie do RIF =====
Linia 89: Linia 99:
  
  
-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''"​). ​+Aby uprościć język, będziemy często używać identyfikatorów ​przestrzeni ​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:​ By odwołać się do stałej w określonej przestrzeni nazw RIF, używamy następującej składni prezentacji:​
Linia 123: Linia 133:
  
 === Poprawne formułowanie Termów === === Poprawne formułowanie Termów ===
-[[http://​www.w3.org/​2005/​rules/​wg/​draft/​rif-bld/#​Well-formedness_of_Terms|Well-formedness of Terms]]//\\+//[[http://​www.w3.org/​2005/​rules/​wg/​draft/​rif-bld/#​Well-formedness_of_Terms|Well-formedness of Terms]]//\\
  
-Zbiór ​wyszystkich ​symboli, ''​Const'',​ jest podzielony na:+Zbiór ​wszystkich ​symboli, ''​Const'',​ jest podzielony na:
     * Pozycjonowane symbole predykatów (ang. positional predicate symbols)     * Pozycjonowane symbole predykatów (ang. positional predicate symbols)
     * Symbole predykatów z nazwanymi argumentami (ang. predicate symbols with named arguments)     * Symbole predykatów z nazwanymi argumentami (ang. predicate symbols with named arguments)
Linia 138: Linia 148:
     * 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.     * 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:​ +Arność symbolu (czy predykatu, funkcji, bądź 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:​+    * Każdy stały symbol w formule ​RIF-BLD (lub zbiorze formuł) może się pojawić ​co najwyżej w jednym z kontekstów:​
        * jako osobnik,        * jako osobnik,
        * jako symbol funkcji o określonej arności        * jako symbol funkcji o określonej arności
-       * jako symbol predykatu o określonej ​atności.+       * jako symbol predykatu o określonej ​arności.
     * Arność symbolu i jego typ jest określany przez jego kontekst.     * 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.     * 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.
Linia 155: Linia 165:
  
 ==== Formuły ==== ==== Formuły ====
 +//​[[http://​www.w3.org/​2005/​rules/​wg/​draft/​rif-bld/#​Formulas|Formulas]]//​\\
 +
 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ą. 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ą.
  
Linia 163: Linia 175:
    * //​Atomiczną (ang. atomic)//: Jeśli ''​t''​ jest dobrze sformułowaną formułą atomiczną, to jest również dobrze sformułowaną formułą.    * //​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.    * //​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.+   * //​Dysjunktywna (ang. disjunction)//: ​ Jeśli ''​t_1,​ ..., t_n'',​ ''​n >= 0''​ są dobrze sformułowanymi formułami, to również formuła ​dysjunktywna ​''​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.    * //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: 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(...)''​).    * //​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. +   * //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łą ​kwantyfikują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.+   * //Grupa (ang. group)//: Jeśli ''​t''​ jest ramą oraz ''​p_1,​ ..., p_n''​ są regułami RIF-BLD lub grupami formuł (mogą ​być 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.+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żone. 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)''​.+Z powyższych definicji wynika, że RIF-BLD posiada szeroki wachlarz form syntaktycznych dla termów i formuł. Zapewnia to infrastrukturę dla wymiany językó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 ​uporzą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)''​.
  
  
Linia 181: Linia 193:
  
 ==== Gramatyka warstwy prezentacji (EBNF) ==== ==== Gramatyka warstwy prezentacji (EBNF) ====
 +//​[[http://​www.w3.org/​2005/​rules/​wg/​draft/​rif-bld/#​EBNF_Grammar_for_the_Presentation_Syntax_of_RIF-BLD|EBNF Grammar for the Presentation Syntax of RIF-BLD]]//​\\
 +
 Analizując zapis RIF w tej notacji, należy pamiętać o kilku rzeczach: 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ładnisa logiki pierwszego rzędu (ang. first-order logic) nie jest bez kontekstowa, 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 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 ​wykorzystywana ​jako separator.
    * Składnia EBNF nie jest normatywna.    * Składnia EBNF nie jest normatywna.
  
Linia 216: Linia 230:
  
 ===== Bezpośrednia specyfikacja semantyki RIF-BLD ===== ===== Bezpośrednia specyfikacja semantyki RIF-BLD =====
-==== Wartości Prawdy ​(Truth Values) ​====+==== Wartości Prawdy ==== 
 +//​[[http://​www.w3.org/​2005/​rules/​wg/​draft/​rif-bld/#​Truth_Values|Truth Values]]//​\\ 
 Zbiór ''​TV''​ wartości prawdy w RIF-BLD składa się z dwóch wartości: ''​t''​ oraz ''​f''​. Zbiór ''​TV''​ wartości prawdy w RIF-BLD składa się z dwóch wartości: ''​t''​ oraz ''​f''​.
 +
  
  
Linia 224: Linia 241:
  
 ==== Konstrukcje Semantyczne ==== ==== Konstrukcje Semantyczne ====
 +//​[[http://​www.w3.org/​2005/​rules/​wg/​draft/​rif-bld/#​Semantic_Structures|Semantic Structures]]//​\\
 +
 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. 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)**\\ **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).+Struktura semantyczna,​ ''​I'',​ jest to entka //​(ang. ​tuple)// 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:​ Pozostałe składowe ''​I''​ są odwzorowaniami zupełnymi (ang. total mappings) zdefiniowanymi następująco:​
Linia 278: Linia 297:
  
  
 +==== Interpretacja Formuł ====
 +//​[[http://​www.w3.org/​2005/​rules/​wg/​draft/​rif-bld/#​Interpretation_of_Formulas|Interpretation of Formulas]]//​\\
  
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
-==== Interpretacja Formuł ==== 
 **Definicja oszacowania prawdy (ang. Truth valuation)**\\ **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'':​ Oszacowanie prawdy dla dobrze sformułowanej formuły w RIF-BLD jest wyznaczane przy pomocy następującej funkcji, oznaczanej jako ''​TValI'':​
Linia 334: Linia 338:
  
 ==== Logical Entailment ==== ==== Logical Entailment ====
 +//​[[http://​www.w3.org/​2005/​rules/​wg/​draft/​rif-bld/#​Logical_Entailment|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. 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.
Linia 348: Linia 353:
  
 ==== Zapis w XML języka warunkowego ==== ==== Zapis w XML języka warunkowego ====
 +//​[[http://​www.w3.org/​2005/​rules/​wg/​draft/​rif-bld/#​XML_for_the_RIF-BLD_Condition_Language|XML for the RIF-BLD Condition Language]]//​\\
 +
 Wykorzystujemy następujące tagi: Wykorzystujemy następujące tagi:
 <​code>​- And       ​(conjunction) <​code>​- And       ​(conjunction)
Linia 387: Linia 394:
  
 ==== Zapis w XML języka reguł ==== ==== Zapis w XML języka reguł ====
 +//​[[http://​www.w3.org/​2005/​rules/​wg/​draft/​rif-bld/#​XML_for_the_RIF-BLD_Rule_Language|XML for RIF-BLD Rule Language]]//​\\
 +
 Jest to rozszerzenie języka warunkowego,​ o: Jest to rozszerzenie języka warunkowego,​ o:
 <​code>​- Group    (nested collection of sentences annotated with metadata) <​code>​- Group    (nested collection of sentences annotated with metadata)
Linia 497: Linia 506:
 Wstępne przmyślenia:​ Wstępne przmyślenia:​
    * Do nadania identyfikatorów posłuży element spoza RIF, należący do języka XML - ''​id''​.    * Do nadania identyfikatorów posłuży element spoza RIF, należący do języka XML - ''​id''​.
 +
 +
 +
 +
 +
 +
 +
 +
 +
 +
 +
 +
 +
  
  
Linia 531: Linia 553:
    <​then>​    <​then>​
     <​Atom>​ <!-- specjalny predykat, sugerujący następną regułę/​tablicę i wywołujący inne predykaty -->     <​Atom>​ <!-- specjalny predykat, sugerujący następną regułę/​tablicę i wywołujący inne predykaty -->
-     <​op><​Const type="​rif:​iri">​xtt:​concl</​Const></​op>​ +     <​op><​Const type="​rif:​iri">​xtt:​next_table_rule</​Const></​op>​ 
-     <​arg>​ +     <​arg><​Const type="​xsd:​string">​xtt_table1</​Const></​arg>​ 
-      <​Atom>​ <!-- predykat podajacy wartosci '​id'​ nastepnej tablicy/​wiersza --> +     ​<​arg><​Const type="​xsd:​string">​xtt_table_row1</​Const></​arg>​
-       <​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>​      <​arg>​
       <!-- albo predykat do wywołania, albo predykat xtt:​run_many wywołujący więcej niż jeden predykat -->       <!-- albo predykat do wywołania, albo predykat xtt:​run_many wywołujący więcej niż jeden predykat -->
Linia 564: Linia 581:
 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''​. 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''​.
  
-Aby zapisać warunek gdzie zmienna ​należdo np. ''​{1,5}u8''​ w RIF posłużono się następującą konstrukcją:​+Jako, że XTT posługuje się również parametrami będącymi zbiorami (zapisywane przez ''​{V}''​), ​należało stworzyć konstrukcję o podobnym działaniu w RIF. Moja propozycja jest taka, aby taki parametr identyfikować predykatem ''​xtt:​set/​2''​ definiujący zbiór od liczby ''​a'' ​do ''​b''​Aby zapisać znienną ​''​{a,b}uC''​, gdzie C jest pojedyńczym elementem, bądź innym przedziałem, ​w RIF posłużono się następującą konstrukcją:​
 <code xml><​Atom>​ <code xml><​Atom>​
- <​op><​Const type="​rif:​iri">​in</​Const></​op> <!-- przynależność do zbioru --+ <​op><​Const type="​rif:​iri">​xtt:​complex_set</​Const></​op>​ 
- <​arg><​Var>​att_0</​Var></​arg>​  + <​arg>​
- <​arg>​ <!-- {1,5} -->+
   <​External>​   <​External>​
    <​content>​    <​content>​
     <​Expr>​     <​Expr>​
      <​op><​Const type="​rif:​iri">​xtt:​set</​Const></​op>​      <​op><​Const type="​rif:​iri">​xtt:​set</​Const></​op>​
-     <​arg><​Const type="​xsd:​decimal">​1</​Const></​arg>​ +     <​arg><​Const type="​xsd:​decimal">​a</​Const></​arg>​ 
-     <​arg><​Const type="​xsd:​decimal">​5</​Const></​arg>​+     <​arg><​Const type="​xsd:​decimal">​b</​Const></​arg>​
     </​Expr>​     </​Expr>​
    </​content>​    </​content>​
   </​External>​   </​External>​
  </​arg>​  </​arg>​
- <​arg><​Const type="​xsd:​decimal">​8</​Const></​arg> <!-- u8 -->+ <​arg>​ 
 +  ​<Const type="​xsd:​decimal">​C</​Const>​ 
 + </​arg>​
 </​Atom></​code>​ </​Atom></​code>​
  
-**Uwagi**\\ +Zapis przyrównania zmiennej do zbioru ​(''​X = {1,2,4}''​) ​będzie realizowany za pomocą tagu ''​Equal'':​ 
-  * Każda tablica ​(element ​''​Group''​) ​musi być w osobnym pliku (zgodność z plikami ​xsd).+<code xml><​Equal>​ 
 + <​side><​Var>​X</​Var></​side>​ 
 + <​side>​ 
 +  <​External>​ 
 +   <​content>​ 
 +    <​Expr>​ 
 +     <​op><​Const type="​rif:​iri">​xtt:​complex_set</​Const></​op>​ 
 +     <​arg><​Const type="xsd:​decimal">​1</​Const></​arg>​ 
 +     <​arg><​Const type="​xsd:​decimal">​2</​Const></​arg>​ 
 +     <​arg><​Const type="​xsd:​decimal">​4</​Const></​arg>​ 
 +    </​Expr>​ 
 +   </​content>​ 
 +  </​External>​ 
 + </​side>​ 
 +</​Equal></​code>​ 
 +//ten zapis nie został zaimplementowany w translatorze,​ ze względu na brak informacji co do zapisu po stronie XTTMLa.//
  
-=== Przykład 1: calculations (factorial) ​=== +=== Wykorzystywane predykaty ​=== 
-<​code>​ +W najnowszej wersji dokumentacji RIFa pojawił się dokument definiujący zarówno [[http://www.w3.org/2005/rules/wg/draft/ED-rif-dtb-20080518/#​List_of_Supported_Built-in_Predicates_and_Functions|predykaty wbudowane]],​ jaki i [[http://www.w3.org/2005/rules/wg/draft/rif-dtb/#Appendix:_Schemas_for_Externally_Defined_Terms|definiowanie zewnętrznych]].
-|----------------------------------------------------| +
-|                                                    | +
-|   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">​ +^Predykat ​ ^External ​schema ​                          ​^Opis ​                                                                   ^ 
-  <​Implies>​ +| xtt:set  |''​(?​arg1 ?arg2; pred:set(?arg1, ?​arg2))''​ |Predykat definiuje zbiór liczb z zakresu. Odpowiednik ''​{arg1,​ arg2}''​. | 
-   <​if>​ +| xtt:complex_set |''​(?​arg1 ?arg2 [...]; pred:complex_set(?​arg1,​ ?arg2, [...]))''​ |Predykat definiuje złożony zbiór. Za argumenty może przyjmować nie tylko liczby całkowite, ale również predykaty ''​xtt:set''​. | 
-    <External> +xtt:next_table_rule |''​(?​arg1 ?arg2 ?arg3; pred:next_table_rule(?​arg1,​ ?arg2, ?​arg3))''​ |Predykat sterujący wnioskowaniem. Pierwszy argument to ''​id''​ tabeli, która powinna być wywołana jako następna (''​id''​ taga ''​Group''​). Drugi - ''​id''​ konkretnego wiersza owej tabeli (''​id''​ taga ''​sentence''​). Ostatni parametr to operacja, jaką należy wykonać przy wykonaniu reguły. | 
-     <​content>​ +| xtt:next_table |''​(?​arg1 ?arg2; pred:next_table(?​arg1,​ ?​arg2))''​ |Predykat sterujący wnioskowaniem. Pierwszy argument to ''​id''​ tabeli, która powinna być wywołana jako następna (''​id''​ taga ''​Group''​). Drugi parametr to operacja, jaką należy wykonać przy wykonaniu reguły. | 
-      <​Atom>​ +| xtt:run_many |''​(?​arg1 ?arg2 [...]; pred:run_many(?​arg1,​ ?arg2, [...]))''​ |Predykat wykorzystywany w konkluzji, ​służący do wywoływania więcej niż jednej operacji. |
-       <​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">​ +Dodatkowo wszystkie operatory ''​logop'' ​są traktowane jako zdefiniowane operatory i występują jako predykaty z przedrostkiem ''​xtt:''​. Na przykład ''​\in''​ będzie to ''​<​op><​Const type="​rif:​iri">​xtt:​in</​Const></​op>​''​. 
- <​sentence id="​xtt_table2_row1">​ + 
-  <​Implies>​ +**Uwagi**\\ 
-   <​if>​ +  ​* Każda tablica (element ''​Group''​) musi być osobnym pliku (zgodność z plikami xsd).
-    <​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 ​dokumentacji,​ nie należy się tym przejmować. Nigdzie w dokumentacji nie ma wyraźnego zakazu wykorzystywania elementów standardu XML.+
  
  
 +==== Sugestie/​Braki w RIF ====
 +  * Możliwość umieszczania kilku elementów ''​Group''​ w jednym pliku
 +  * Identyfikowanie poszczególnych ''​Group'',​ ''​sentence'',​ np. poprzez parametr ''​id''​
 +  * Uproszczenie zapisu w xml ''​External schema'',​ bo w tej chwili zapis powoduje spory rozrost pliku i zmniejsza czytelność
 +  * "​Wywoływanie"​ większej ilości predykatów w konkluzji
  
 FIXME FIXME
-  * runmany, etc +  * ^_^runmany, etc 
-  * zestawienie wprowadzonych predykatów iri:xtt_... -> odn. do ew. impl. +  * ^_^zestawienie wprowadzonych predykatów iri:xtt_... -> odn. do ew. impl. 
-  * ew. lista sugestii/​ograniczeń w rif (id reguł)+  * ^_^ew. lista sugestii/​ograniczeń w rif (id reguł)
  
 ==== Translacja XTTML => RIF ==== ==== Translacja XTTML => RIF ====
pl/miw/miw08_xtt_rif.1211967419.txt.gz · ostatnio zmienione: 2019/06/27 15:58 (edycja zewnętrzna)
www.chimeric.de Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0