Both sides previous revision
Poprzednia wersja
Nowa wersja
|
Poprzednia wersja
|
pl:miw:miw08_xtt_rif [2008/05/21 20:34] miw translator |
pl:miw:miw08_xtt_rif [2019/06/27 15:50] (aktualna) |
====== 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 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://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]] | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
//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 ===== |
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'' |
| |
| |
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: |
| |
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 === |
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) |
* 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. |
| |
==== 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ą. |
| |
* //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)''. |
| |
| |
| |
==== 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. |
| |
| |
===== 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''. |
| |
| |
| |
| |
==== 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: |
| |
| |
| ==== 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'': |
| |
==== 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. |
| |
==== 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) |
| |
==== 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) |
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''. |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
<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 --> |
| |
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''. |
| |
| 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> |
| <op><Const type="rif:iri">xtt:complex_set</Const></op> |
| <arg> |
| <External> |
| <content> |
| <Expr> |
| <op><Const type="rif:iri">xtt:set</Const></op> |
| <arg><Const type="xsd:decimal">a</Const></arg> |
| <arg><Const type="xsd:decimal">b</Const></arg> |
| </Expr> |
| </content> |
| </External> |
| </arg> |
| <arg> |
| <Const type="xsd:decimal">C</Const> |
| </arg> |
| </Atom></code> |
| |
| Zapis przyrównania zmiennej do zbioru (''X = {1,2,4}'') będzie realizowany za pomocą tagu ''Equal'': |
| <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.// |
| |
| === Wykorzystywane predykaty === |
| 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]]. |
| |
| ^Predykat ^External schema ^Opis ^ |
| | xtt:set |''(?arg1 ?arg2; pred:set(?arg1, ?arg2))'' |Predykat definiuje zbiór liczb z zakresu. Odpowiednik ''{arg1, arg2}''. | |
| | 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''. | |
| | 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. | |
| | 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. | |
| | 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. | |
| |
| 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>''. |
| |
**Uwagi**\\ | **Uwagi**\\ |
* Każda tablica (element ''Group'') musi być w osobnym pliku (zgodność z plikami xsd). | * 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"> | ==== Sugestie/Braki w RIF ==== |
<sentence id="xtt_table2_row1"> | * Możliwość umieszczania kilku elementów ''Group'' w jednym pliku |
<Implies> | * Identyfikowanie poszczególnych ''Group'', ''sentence'', np. poprzez parametr ''id'' |
<if> | * Uproszczenie zapisu w xml ''External schema'', bo w tej chwili zapis powoduje spory rozrost pliku i zmniejsza czytelność |
<And> | * "Wywoływanie" większej ilości predykatów w konkluzji |
<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. | |
| |
| 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 ==== |
Po zaproponowaniu wstępnej postaci zapisu XTT w RIF, nadszedł czas na stowrzenie translatora [[hekate:hekate_markup_language#xttml|XTTML]] => RIF. | Po zaproponowaniu wstępnej postaci zapisu XTT w RIF, nadszedł czas na stowrzenie translatora [[hekate:hekate_markup_language#xttml|XTTML]] => RIF. |
Translator można pobrać tutaj: {{:pl:miw:miw08_xtt_rif:xtttorif.xml|XTTtoRIF.xml}}. | Translator można pobrać tutaj: {{:pl:miw:miw08_xtt_rif:xtttorif.xml|XTTtoRIF.xml}}. |
| |
| Sposób zapisu w RIFie mniejwiecej zgadza się z przedstawionym powyżej. Dokonałem jedynie pewnych uproszczeń, ułatwiających translacje. Za pomocą powyższego arkusza XSLT dokonałem translacji [[hekate:hekate_markup_language#xttml|przykładu]], która znajduje się [[pl:miw:miw08_xtt_rif:xtt2rif|tutaj]]. Z powodu składni RIFa stosunkowo prosty i czytelny przykład rozrósł się dość znacznie. |
| |
====== Materiały ====== | ====== Materiały ====== |