Система Автоматизации Дедукции принимает на вход одноцелевые секвенции первого порядка в виде последовательности формул, завершаемых точкой, где цель секвенции отделена от посылок двоеточием. Таким образом, секвенция  P1, P2, P3 -> G  записывается как  P1. P2. P3. : G.  Допускаются секвенции с пустой целью, в виде  P1. P2. P3. :  

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

Введите в окне внизу входную секвенцию первого порядка. Команда [Prove with Moses] запускает прувер системы САД, Moses. Команда [Prove with] запускает внешний прувер.

1. Простая лемма из теории групп. [Запустить пример]