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/20 10:49]
gjn
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_two wywołujący więcej niż jeden predykat (można je zagnieżdżać) --> 
-     </​arg>​ 
-    </​Atom>​ 
-   </​then>​ 
-  </​Implies>​ 
- </​sentence>​ 
- 
- <​sentence id="​xtt_table_row2">​ 
-  ... 
- </​sentence>​ 
- 
- ... 
- 
-</​Group></​code>​ 
-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ę. 
- 
-**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_two</​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. 
- 
-====== 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)
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