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/21 20:47]
miw set
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>​
  
 translacja XTTML -> RIF 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 ====== ====== Projekt ======
-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]]**
- +  * [[http://​saxon.sourceforge.net/​|SAXON]] translator XSLT zaimplementowany ​w JAVA oraz .NET (jest wersja Open Source, która nie zawiera paru dodatkowych funkcji)
-===== Przetestowane narzędzia/​podejścia ===== +
-//których ewmy 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://​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]]**
-===== Ciekawe linki ===== +
-  ​* [[http://​www.w3.org/​2005/​rules/​wg/​wiki/​Arch/​XML_Syntax_Issues_2]] +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
- +
  
  
Linia 122: 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 131: Linia 36:
 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). 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. 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 ===== ===== Bezpośrednia specyfikacja składni RIF-BLD =====
 +//​[[http://​www.w3.org/​2005/​rules/​wg/​draft/​rif-bld/#​Direct_Specification_of_RIF-BLD_Syntax|Direct Specification of RIF-BLD Syntax]]//
 +
 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. 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 ==== 
 +//​[[http://​www.w3.org/​2005/​rules/​wg/​draft/​rif-bld/#​Alphabet_of_RIF-BLD|Alphabet of RIF-BLD]]//​\\ 
 Alfabet RIF-BLD składa się z dowolnej //(ang. countably infinite)// liczby: Alfabet RIF-BLD składa się z dowolnej //(ang. countably infinite)// liczby:
   * **stałych symboli**: ''​Const''​   * **stałych symboli**: ''​Const''​
Linia 185: 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 192: Linia 106:
    
 Zbiór wszystkich przestrzeni symboli, które dzielą ''​Const''​ jest uważany za część **języka logiki** RIF-FLD. Zbiór wszystkich przestrzeni symboli, które dzielą ''​Const''​ jest uważany za część **języka logiki** RIF-FLD.
 +
 +
  
 ==== Termy ==== ==== Termy ====
 +//​[[http://​www.w3.org/​2005/​rules/​wg/​draft/​rif-bld/#​Terms|Terms]]//​\\
 +
 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ń. 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 === === Definicja ===
Linia 214: Linia 132:
 Termy klasyfikujące,​ podklas i ramowe są używane do opisu obiektów i hierarchii klas. 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)=== +=== Poprawne formułowanie Termów ​=== 
-Zbiór ​wyszystkich ​symboli, ''​Const'',​ jest podzielony na:+//​[[http://​www.w3.org/​2005/​rules/​wg/​draft/​rif-bld/#​Well-formedness_of_Terms|Well-formedness of Terms]]//\\ 
 + 
 +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 228: 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 245: 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 253: 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 271: 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 306: 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 314: 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 368: 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 424: 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 438: 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 477: 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 587: 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 618: 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 651: 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
 +  * ^_^runmany, etc
 +  * ^_^zestawienie wprowadzonych predykatów iri:xtt_... -> odn. do ew. impl.
 +  * ^_^ew. lista sugestii/​ograniczeń w rif (id reguł)
  
 ==== Translacja XTTML => RIF ==== ==== Translacja XTTML => RIF ====
pl/miw/miw08_xtt_rif.1211395659.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