リプライを特定の形式で送ると反応します。反応する形式は以下の通り。
- 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
- ランダムに何かを表示します。