Różnice między wybraną wersją a wersją aktualną.
|
pl:miw:miw08_xtt_rif:signatures [2019/06/27 15:50] |
pl:miw:miw08_xtt_rif:signatures [2019/06/27 15:50] (aktualna) |
||
|---|---|---|---|
| Linia 1: | Linia 1: | ||
| + | ====== Reguły wykorzystania podpisów w RIFie ====== | ||
| + | Zostanie tutaj opisana koncepcja podpisów (ang. signatures), które są kluczowym mechanizmem umożliwiającym kontrolowanie kontekstu, w którym dane symbole mogą się pojawić. **Należy pamiętać, że podpisy nie są częścią języka logiki w RIF, ponieważ nie pojawiają się w formułach.** | ||
| + | * Wyróżniamy następujące podpisy: | ||
| + | - term{ } - przedstawia kontekst w jakim występują pojedyncze obiekty (ale nie formuły atomiczne) | ||
| + | - atomic{ } | ||
| + | - bi_atomic{ } - przedstawia formuły atomiczne dla wbudowanych predykatów | ||
| + | Ponieważ bi_atomic < atomic, wbudowane formuły atomiczne są również zwykłymi formułami atomicznymi. Zazwyczaj większość formuł atomicznych jest zdefiniowana przez użytkownika i będą one miały podpis atomic, a nie bi_atomic. | ||
| + | * Wszelkie symbole funkcyjne o arności //n// zapisujemy następująco | ||
| + | <code>f_n{(term ... term) => term}, p_n{(term ... term) => atomic}, and bi_n{(term ... term) => bi_atomic}</code> | ||
| + | * Dla każdego zestawu symboli s_1,...,s_k zawartych w SigNames, istnieją podpisy | ||
| + | <code>f_s1...sk{(s1->term ... sk->term) => term} oraz p_s1...sk{(s1->term ... sk->term) => atomic}</code> | ||
| + | są to podpisy dla termów z nazwanymi argumentami oraz predykatów z nazwanymi argumentami. | ||
| + | * Symbol ze zbioru //Const// może mieć tylko jeden zpodpisów: term, f_n, p_n, albo bi_n, gdzie n>=0, lub f_s1...sk{(s1->term ... sk->term) => term}, p_s1...sk{(s1->term ... sk->term) => atomic}, dla pewnych s1,...,sk należących do SigNames. Symbol ten **nie może** mieć podpisu atomic, bi_atomic, ponieważ tylko złożone termy mogą mieć taki podpis. A zatem, w RIF-BLD każdy stały symbol może być: | ||
| + | - indywidualnym | ||
| + | - predykatem o określonej arności, bądź określonymi nazwami argumentów | ||
| + | - wbudowanym o określonej arności | ||
| + | - funkcją o określonej arności | ||
| + | - **Niedopuszczalne jest, aby jeden symbol odgrywał więcej niż jedną rolę** | ||
| + | * Stałe symbole, które odpowiadają typom ze Schematów XML mają zawsze podpis term w RIF-BLD. Symbole typu rif:iri, rif:local, mogą mieć następujące podpisy: term, f_n, p_n, lub bi_n, for n = 0,1,....; albo f_s1...sk, p_s1...sk, dla pewnych nazw argumentów s1,...,sk należących do SigNames. | ||
| + | * Wszystkie zmienne mają podpis term{ }. | ||
| + | * Podpis równości ={(term term) => atomic, (term term) => term}. Oznacza to, że równość może porównywać tylko te termy, których podpisem jest term, nie może porównywać nazw predykatów, czy symboli funkcji. | ||
| + | * Podpis frame, ->, to ->{(term term term) => atomic, (term term term) => term}. | ||
| + | * Podpis membership, #, to #{(term term) => atomic, (term term) => term}. | ||
| + | * Podpis podklasy relationship to ##{(term term) => atomic, (term term) => term}. | ||
| + | [[pl:miw:miw08_xtt_rif|Powrót do dokumentu]] | ||
