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:
    1. term{ } - przedstawia kontekst w jakim występują pojedyncze obiekty (ale nie formuły atomiczne)
    2. atomic{ }
    3. 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
f_n{(term ... term) => term}, p_n{(term ... term) => atomic}, and bi_n{(term ... term) => bi_atomic}
  • Dla każdego zestawu symboli s_1,…,s_k zawartych w SigNames, istnieją podpisy
f_s1...sk{(s1->term ... sk->term) => term} oraz p_s1...sk{(s1->term ... sk->term) => atomic}

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ć:
    1. indywidualnym
    2. predykatem o określonej arności, bądź określonymi nazwami argumentów
    3. wbudowanym o określonej arności
    4. funkcją o określonej arności
    5. 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}.

Powrót do dokumentu

pl/miw/miw08_xtt_rif/signatures.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