リプライを特定の形式で送ると反応します。反応する形式は以下の通り。

from n
(nは自然数) 命題nから導かれる命題番号の一覧を返します。
to n
(nは自然数) 命題nを導かれる命題番号の一覧を返します。
from m to n
(m, nは自然数) 命題mから命題nが導かれるかどうかを返します。
prop X
(Xは命題番号) 命題Xの主張を返します。
model X
(Xはモデル番号) モデルXを返します。
model m n
(m, nは自然数) 命題mが真となり命題nが偽となるようなモデル一覧を返します。
reference nameA nameB … nameZ year
nameA, nameB, …, nameZが著者のyear年の参考文献を返します。(複数ある場合はyearの後ろにa, b, c, …が付きます。)
reference name
nameが著者の参考文献の、年一覧を返します。
search wordA wordB … wordZ
wordA, wordB, …, wordZ で部分一致検索(AND検索)を行います。
from n search wordA wordB … wordZ
to n search wordA wordB … wordZ
from nやto n の結果に対して部分一致検索(AND検索)を行います。
why
from m to nの返答(証明可能/不可能)に対してリプライすると、証明可能/不可能の理由を返します。
model
from m to nの返答(証明不可能)に対してリプライすると、証明不可能であることを示すモデルを返します。
random
ランダムに何かを表示します。