ГОСТ Р И С 018629-11 — 2010
щий функцию (function-forming term), состоит из буквы лямбда, списка переменных и термина. Нет необходимости в
использовании каппы и лямбды — обе эти буквы греческого алфавита могут быть определены в терминах setof; их
включают в KIFдля удобства.
Следующие формы Бэкуса-Наура определяют множество формальных предложений в KIF. Имеется шесть
типов предложений.
<sentence> ::= <logconst> | <equation> | <inequality> | <relsent> | <logsent> | <quantsent>
<equation> ::= (= <term> <term>)
<inequality> ::= (/= <term> <term>)
<retsent> ::= (<relconst> <term>* [<seqvar>]) | (<funconst> <term>* <tenn>)
<logsent> ::= (not <sentence>) |
(and <sentence>’) |
(or <sentence>*) |
(implies <sentence>* <sentence>) |
(<= <sentence> <sentence>*) |
(iff <sentence> <sentence>)
<quantsent> ::= (forall <indvax> <sentence>) |
(forall (<indvar>*) <sentence>) |
(exists <indvar> <sentence>) |
(exists (<indvar>*) <sentence>)
Равенство (equation) состоит из оператора «=» и двух терминов.
Неравенство (inequality) состоит из оператора «/=» и двух терминов.
Связанное предложение состоит из константы отношений и произвольного числа терминов аргументов,
завершенных необязательной переменной последовательности. Так же как с функциональными терминами, в
предложении отношений нет синтаксического ограничения к числу терминов аргументов — одна и та же констан та
отношений может быть применена к любому числу аргументов.
Синтаксис логических предложений logical sentences зависит от используемого логического оператора.
Предложение, использующее оператор not. называют отрицанием (negation). Предложение, использующее опе
ратор and. называют конъюнкцией (conjunction), а аргументы — конъюнктами (conjuncts). Предложение, ис
пользующее оператор or. называют дизъюнкцией (disjunction), а аргументы — дизъюнктами (disjuncts). Предло
жение, использующее оператор implies, называют импликацией (implication); вое его аргументы, за исключением
последнего, называют antecedents; а последний аргумент — consequent. Предложение, использующее оператор
«<=». называют обратной импликацией; ее первый аргумент называют consequent, а остальные аргументы —
(antecedents). Предложение, использующее оператор iff. называют эквивалентностью (equivalence).
Имеются два типа предложений под знаком квантора (quantified sentences) — универсально квантифици
руемое предложение (universally quantified) задают с помощью сигнала путем использования оператора forall и
экзистенционально квантифицируемое предложение (existentially quantified sentence) задают с помощью сигна
ла путем использования оператора exists.
В.ЗСемантика
Интерпретацией языка KIF первого порядка является кортеж I = (О, ext а. т^. задаваемый следующим
образом.
В.3.1 Функция расширения
В соответствии с интерпретацией «I» функция расширения ext имеет следующие свойства:
• =£ uft.
• =Е nR =<Z>:
• = If s е £. then ext (s) =0;
• = If s e R. then ext (s) c O’.
B.3.2 Функция семантического значения для терминов
В соответствии с интерпретацией «I» функция семантического значения а должна иметь свойства, указан
ные вследующих пунктах.
В.3.2.1 Семантическое значение переменных объекта (Object Variables)
Семантическим значением переменой объекта v является объект, назначаемый этой переменой в интер
претации «I»:
o(v)e О
В.3.2.2 Семантическое значение постоянных величин (Constants)
Семантическим значением константы s является объект, назначаемый этой постоянной величине в интер
претации «I»:
o(s)e О.
16