Формулы первого порядка

Формулы строятся из лексем: переменных, функциональных и предикатных символов, при помощи пропозициональных связок, кванторов и скобок. Также разрешается использовать точку Черча для группирования подформул. Используются следующие обозначения (в скобках приводится альтернативный вариант):

Каждая лексема есть последовательность латинских букв, цифр и подчерков. Регистр учитывается. Переменные, не связанные квантором явно, трактуются как константы.

Примеры правильно построенных формул:

forall x . Nat(x) > (x = zero | exists y less(y,x))

@ x, y (sym_rel(x,y) iff sym_rel(y,x))


Тексты первого порядка

Тексты в языке первого порядка, обрабатываемые системой САД, представляют собой последовательности формул, завершаемых точкой. Заметьте, что этот же символ используется для обозначения точки Черча, однако в правильно построенных формулах неоднозначности не возникает.

Формулы, предваренные двоеточием, рассматриваются как цели, и верификатор пытается вывести их из предшествующих формул. Если верификация завершилась успешно, цель становится посылкой для последующих целей. В противном случае, система прекращает работу. Если текст завершается двоеточием, в качестве заключительной цели принимается константа 'ложь'. Такая запись применяется для поиска опровержения множества формул. Одноцелевые секвенции первого порядка, в частности, являются корректными текстами. Так, секвенция  P1, P2, P3 -> G  представляется текстом  P1. P2. P3. : G. 

Разрешаются однострочные комментарии, начинающиеся символом '#'. Пример правильно построенного текста:

# Funny lemma from the group theory
forall x,y exists z P(x, y, z).
forall x,y,z,u,v,w . P(x, y, u) & P(y, z, v) & P(u, z, w) > P(x, v, w).
forall x,y,z,u,v,w . P(x, y, u) & P(y, z, v) & P(x, v, w) > P(u, z, w).
forall x . P(x, e, x) & P(e, x, x).
forall x . P(x, i(x), e) & P(i(x), x, e).
forall x P(x, x, e).
:   forall x,y,z . P(x, y, z) > P(y, x, z).
P(a, b, c).   :   P(b, a, c). # having the precedent goal proved
# the last goal is obvoiusly entailed by the last premise


ForTheL-тексты

ForTheL-текст представляет собой последовательность разделов, фраз и служебных конструктов, таких как описания шаблонов. Фразы являются либо предположениями (в этом случае они начинаются словами "let" или "assume"), либо утверждениями. Разделы могут состоять из разделов нижнего уровня и фраз. Разделами верхнего уровня являются аксиомы, определения и теоремы. Каждый раздел верхнего уровня есть последовательность предположений, завершаемая утверждением. В теоремах и аксиомах утверждение может быть произвольным утверждением ForTheL, тогда как утверждение в определении должно иметь специальный вид, в зависимости от типа определяемого объекта. Разделами нижнего уровня являются доказательства, блоки и случаи в доказательстве. Каждый раздел нижнего уровня есть последовательность предположений, утверждений и разделов нижнего уровня, завершаемая утверждением.

Грамматика ForTheL-фразы имитуирует грамматику английского предложения. Фраз строятся из существительных, обозначающих понятия (классы) и функции, из прилагательных и глаголов, обозначающих предикаты, из предлогов, союзов и служебных слов, определяющих логическую структуру сложного предложения. Пример простого утверждения: "Every closed subset of every compact set is compact."

Более подробные сведения о языке ForTheL вы можете получить из Руководства по языку ForTheL (на английском языке, gzipped PS или PDF), а также из примеров теорем и текстов. Один из этих текстов приводится ниже (запустить пример).

Простой текст из теории множеств

[set/-s] [element/-s] [belong/-s] [subset/-s]

Signature SetSort. A set is a notion.
Let S,T denote sets.

Signature ElmSort. An element of S is a notion.
Let x belongs to X stand for x is an element of X.

Definition DefSubset. A subset of S is a set T
  such that every element of T belongs to S.

Definition DefEmpty. S is empty iff S has no elements.

Axiom ExEmpty. There exists an empty set.

Proposition.
  S is a subset of every set iff S is empty.
Proof.
  Case S is empty. Obvious.

  Case S is a subset of every set.
    Take an empty set E.
    Let z be an element of S.
    Then z is an element of E.
    We have a contradiction.
  end.
qed.