FLOTTER - クラウドでオンライン

プログラム：

NAME

SPASS - 等価性を伴う完全な一次論理のための自動化された定理証明器

SYNOPSIS

スパス [オプション] [入力ファイル]

DESCRIPTION

SPASS は、等価性を備えた完全にソートされた XNUMX 次ロジックの自動定理証明器です。
ソートによる重ね合わせとケース分析のための分割ルールを拡張します。 SPASSも可能です
様相論理および記述論理の定理証明者として使用されます。

OPTIONS

SPASS のコマンド ライン オプションは、GNU コマンド ラインを変更することで実装されます。
C 用のオプション パッケージ。オプションを指定するだけでその値が 1 に設定され、
オプション。 オプションを無効にするには、 - を宣言して値を 0 に設定する必要があります。オプション= 0。
現在、SPASS では次のオプションがサポートされています。

-自動
SPASS が自動的に設定する自動モードを有効または無効にします。 の
推論/削減ルール、ソート技術、順序付けと優先順位、
分割と選択の戦略が設定されます。 オートモードではSPASSが完了します。 混合
ユーザー定義オプションを使用した自動モードでは、完全性が損なわれる可能性があります。 デフォルトは 1 です。

-標準入力
標準入力を介した SPASS への入力を有効/無効にします。 ファイル引数は無視されます。 デフォルトは 0 です。

-相互の作用
インタラクティブモードを有効/無効にします。 まず、SPASS に一連の公理が与えられ、次に
証明者は後続の証明タスクを受け入れます。 デフォルトは 0 です。

-フッター
SPASS の CNF 変換モードを有効または無効にします。 オプションが設定されている場合、SPASS のみ
文節の標準形式の変換を実行します。 出力ファイル引数が指定されていない場合 SPASS
CNF を標準出力に出力します。 デフォルトは 0 です。

-SOS
一連のサポート戦略を有効または無効にします。 デフォルトは 0 です。

-分割=n
可能な分割アプリケーションの数を設定します。 n。 場合 n=-1 の場合、次の数
分割には制限がありません。 デフォルトは 0 です。

-メモリ=n
SPASS がプルーフ検索に使用できるメモリの量を次のように設定します。 n バイト。 NS
SPASS の起動に必要なメモリを制限することはできません。 デフォルトは -1 で、これは次のことを意味します
メモリ割り当ては、利用可能なメモリによってのみ制限されます。

-制限時間=n
証拠検索の時間制限を次のように設定します。 n 秒。 デフォルトは -1 で、SPASS を意味します。
永遠に走り続けるかもしれない。 制限時間は、SPASS が新しい条項を選択するときにポーリングされます。
推論。 単一の推論ステップによって生成される数が爆発的に増加する場合、
したがって、所定の期限を大幅に超過する場合があります。

-DocSST
静的ソフトタイピングのドキュメント出力を有効または無効にします。 ソート理論は次のように使用されます。
ソート制約に対する (失敗した) 証明の試行も出力されます。 デフォルトは 0 です。

-ドックプルーフ
証明文書を有効または無効にします。 SPASS が校正刷りを見つけると、最終的に印刷されます。
SPASS が飽和を検出した場合、飽和した文節のセットが最終的に出力されます。
証明文書を有効にすると、SPASS のパフォーマンスが大幅に低下する可能性があります。
証明者は、そうでなければ破棄できる条項を保管する必要があります。 デフォルトは 0 です。

-DocSplit
分割バックトラックステップのドキュメントを設定します。 1 に設定すると、現在の
バックトラッキングレベルが出力されます。 2 に設定すると、分割の場合にも印刷されます。
後戻りした句を後戻りします。 デフォルトは 0 です。

-ループ
SPASS のメインループ反復の最大数を設定します。 デフォルトは -1 です。

-Pサブ
包含された句の印刷を有効または無効にします。 デフォルトは 0 です。

-PRew
単純な書き換えアプリケーションの印刷を有効または無効にします。 デフォルトは 0 です。

-PCon
結露アプリケーションの印刷を有効または無効にします。 デフォルトは 0 です。

-PTaut
トートロジー削除アプリケーションの印刷を有効または無効にします。 デフォルトは 0 です。

-PObv
明らかな縮小アプリケーションの印刷を有効または無効にします。 デフォルトは 0 です。

-PSSi
並べ替え簡略化アプリケーションの印刷を有効または無効にします。 デフォルトは 0 です。

-PSST
静的ソフト タイピング アプリケーションの印刷を有効または無効にします。 削除されたすべての条項は、
印刷された。 デフォルトは 0 です。

-PMRR
一致する代替解像度アプリケーションの印刷を有効または無効にします。 デフォルトは
0.

-パンク
ユニット競合アプリケーションの印刷を有効または無効にします。 デフォルトは 0 です。

-有料
冗長な方程式が削除された句の印刷を有効または無効にします。
（代入式の削除）。

-PDer
推論によって導出された句の出力を有効または無効にします。 デフォルトは 0 です。

-Pギブン
推論を実行するために選択された、指定された句の印刷を有効または無効にします。
デフォルトは0です。

-Pラベル
ラベルの印刷を有効または無効にします。 -DocProof が設定されていて、ラベルがない場合
式が入力によって提供されると、SPASS が汎用ラベルを生成し、
このオプションを有効にすると印刷されます。 デフォルトは 0 です。

-Pケプト
保持された句の印刷を有効または無効にします。 これらは推論によって生成された句です
(バックトラッキング) 冗長ではありません。 入力中に派生した句
縮小/彩度は印刷されません。 デフォルトは 0 です。

-P問題
入力句セットの印刷を有効または無効にします。 デフォルトは 1 です。

-PEmptyClause
派生した空の句の出力を有効または無効にします。 デフォルトは 0 です。

-P統計
派生/バックトラック/キープト句に関する最終統計の出力を有効/無効にします。
実行されたスプリット、使用された時間、および使用されたスペース。 デフォルトは 1 です。

-FPモデル
最終的に見つかったモデルのファイルへの出力を有効または無効にします。 1 に設定すると、すべて
最終セットの句が出力されます。 2 に設定すると、生産的な可能性のある句のみが使用されます。
出力されます。これは、負のリテラルが選択されておらず、最大の正の値をもつ文節です。
XNUMXつ。 もし入力問題と最終的に生成される問題の名前です。
セットが飽和している場合、飽和度がファイルに出力されます.model、の
それ以外の場合は.節。 後者の場合は、たとえば、時間によって引き起こされる可能性があります。
限界。 デフォルトは 0 です。

-FPDFGプルーフ
最終的に見つかった証拠のファイルへの出力を有効または無効にします。 このオプションを使用する
オプション -DocProof を設定する必要があります。 もし入力の名前です
プルーフが印刷される問題.prf. デフォルトは 0 です。

-PFlags
すべてのフラグ値の出力を有効または無効にします。 フラグ設定は次の場所に出力されます。
DFG-Syntax 入力セクションの形式で実行される SPASS の終わり。 デフォルトは 0 です。

-POPtSkolem
最適化された Skolemization アプリケーションの出力を有効または無効にします。 デフォルトは 0 です。

-PStrSkolem
強力な Skolemization アプリケーションの出力を有効または無効にします。 デフォルトは 0 です。

-PBDC
バウンド制限により削除された句の出力を有効または無効にします。 デフォルト
0です。

-PBInc
バウンド制限の変更の出力を有効または無効にします。 デフォルトは 0 です。

-PApplyDefs
アトム定義の展開の印刷を有効または無効にします。 デフォルトは 0 です。

-選択する
SPASS の選択戦略を設定します。 0 に設定すると、負のリテラルは選択されません
終わらせる。 他の値に設定した場合、句内の負のリテラルは最大 XNUMX つになります。
選択されました。 複数の最大リテラルを持つ句で 1 つの負のリテラルに設定された場合
が選択されます。 選択リストからの述語を含む負のリテラル (「
以下) が選択されるか、そのような負のリテラルが使用できない場合は、次の負のリテラルが選択されます。
最大重量が選択されます。 2 に設定すると、負のリテラルが常に選択されます。 また、
選択リスト (以下を参照) からの述語を含む負のリテラルのいずれか
選択されるか、そのような負のリテラルが使用できない場合は、最大値を持つ負のリテラル
重さが選ばれます。 後者の場合、順序付けられたハイパーレゾリューションのような動作が発生します。
順序付けられた解決策。 3 に設定すると、述語が指定された負のリテラルが指定されます。
選択リスト (以下を参照) が選択されています。 デフォルトは 1 です。

-R入力
初期句セットの削減を有効または無効にします。 デフォルトは 1 です。

-ソート
最初の句のソート制約を構築したモナド リテラルを決定します。
セット。 0 に設定すると、並べ替え制約は構築されません。 1 に設定すると、すべて負のモナディックになります。
変数を引数として持つリテラルは、並べ替え制約を形成します。 2 に設定すると、すべて
負のモナド リテラルは並べ替え制約を形成します。 設定 - ソートを 2 にすると害を及ぼす可能性があります
ソート制約は基本戦略と静的制約に従うため、完全性が向上します。
ソフトタイピング。 デフォルトは 1 です。

-SatInput
入力飽和を有効/無効にします。 飽和は不完全ですが、確実に飽和します。
終了します。 デフォルトは 0 です。

-WDRatio
検索の重みまたは深さによって選択された特定の文節間の比率を設定します
空間。 重みは、-FuncWeight と -FuncWeight によって決定されるすべてのシンボルの重みの合計です。
-VarWeight オプション。 すべての初期句の深さは 0 であり、句は次によって生成されます。
推論は、親節の最大の深さに 1 を加えたものを取得します。デフォルトは 5 で、これは意味します。
4 つの節は重みによって選択され、XNUMX 番目の節は深さによって選択されます。

-PrefCon
推測節の重みを計算するための比率を設定するため、次のことが可能になります。
そちらの方がいいです。 デフォルトは 0 で、推測節の重み計算を意味します。
は変更されていません。

-フルレッド
完全な削減を有効または無効にします。 0 に設定すると、実行された句のセットのみが処理されます。
完全に相互還元されます。 1 に設定すると、現在すべての句が保持されます (無効になり、
使用可能) は完全に相互還元されます。 デフォルトは 1 です。

-FuncWeight
関数/述語記号の重みを設定します。 文節の重みはすべての文節の合計です
シンボルの重み。 この重みは、指定された文節の選択時に考慮されます。
デフォルトは1です。

-VarWeight
可変シンボルの重みを設定します (-FuncWeight を参照)。 デフォルトは 1 です。

-PrefVar
多くの変数を含む句の優先設定を有効または無効にします。 While 句は
重みで選択されている場合、このオプションが設定されており、XNUMX つの句の重みが同じである場合、
より多くの変数が出現する句が優先されます。 デフォルトは 0 です。

-バウンドモード
境界制限のモードを選択します。 モード 0 は制限なしを意味し、1 に設定するとすべて
新しく生成された句は重みによって制限されます (-BoundStart を参照)。2 に設定されている場合は、
句は深さによって制限されます。 デフォルトは 0 です。

-バウンドスタート
選択したバウンドモードの開始制限。 たとえば、バウンドモードが 1 の場合、
境界開始を 5 に設定すると、重みが 5 より大きいすべての句が削除されるまで削除されます。
セットは飽和状態です。 これにより、決定される使用される境界値が増加します。
最小限の増加により、削除される前の句が保存されます。 デフォルトは -1 で、制限なしを意味します
制限。

-バウンドループ
アクションの制限/制限の増加を適用するループの数。 番号が
ループの回数を超えると、すべての制限が解除されます。 デフォルトは 1 です。

-ApplyDefs
入力式へのアトム定義の適用の最大数を設定します。
デフォルトは 0 で、アプリケーションがまったく存在しないことを意味します。

-注文
用語の順序を設定します。 0 の場合は KBO が選択され、1 の場合は RPOS が選択されます。 デフォルト
0です。

-CNFQuantExch
設定すると、推測の節形式の非定数スコレム項が置き換えられます。
定数によって。 の最適化された関数変換用に自動的に設定されます。
モーダルまたは説明論理式。 デフォルトは 0 です。

-CNFOptSkolem
最適化された Skolemization を有効または無効にします。 デフォルトは 1 です。

-CNFStrSkolem
強力なスコーレム化を有効または無効にします。 デフォルトは 1 です。

-CNF証明ステップ
最適化された Skolemization 証明試行における証明ステップの最大数を設定します。
デフォルトは100です。

-CNFサブ
CNF プロシージャによって生成された句の包含を有効または無効にします。 デフォルト
1です。

-CNFコン
CNF プロシージャによって生成された句の圧縮を有効または無効にします。 デフォルトは
1.

-CNFRedTime
CNF 中に削減に費やす全体の時間を秒単位で設定します。
変換。 影響を受ける削減は、スコーレム化、凝縮、および
包摂。 デフォルトは -1 で、短縮時間はまったく制限されないことを意味します。

-CNF名前付け
数式の名前変更を有効または無効にします。 1 に設定すると、最適化された名前変更が有効になります。
最終的に生成される句の数を最小限に抑えます。 2 に設定すると、複雑な名前変更が行われます。
すべての複雑な式、つまり任意の式に対して新しい Skolem 述語を導入できるようになりました。
リテラルではない式。 3 に設定すると、数量化の名前変更が有効になります。
量指定子で始まるすべての部分式に新しい Skolem 述語が導入されます。
デフォルトは1です。

-CNFRenMatch
設定すると、名前変更バリアント部分式が同じ Skolem リテラルに置き換えられます。 デフォルト
1です。

-CNFP改名
数式の名前変更アプリケーションの印刷を有効または無効にします。 デフォルトは 0 です。

-CFFFEqR
数式レベルで特定の等価性削減手法を有効または無効にします。 デフォルト
1です。

-IEms
推論ルールの空のソートを有効または無効にします。 デフォルトは 0 です。

-ISOR
推論ルールのソート解決を有効または無効にします。 デフォルトは 0 です。

-IEqR
推論ルールの等価性解決を有効または無効にします。 デフォルトは 0 です。

-IERR
推論ルールの反射性の解決を有効または無効にします。 デフォルトは 0 です。

-IEqF
推論ルールの等価性ファクタリングを有効または無効にします。 デフォルトは 0 です。

-IMPm
推論ルール Merging Paramodulation を有効または無効にします。 デフォルトは 0 です。

-ISpR
推論ルールの重ね合わせ右を有効または無効にします。 デフォルトは 0 です。

-IOPm
推論ルール Ordered Paramodulation を有効または無効にします。 デフォルトは 0 です。

-ISPm
推論ルールの標準パラモジュレーションを有効または無効にします。 デフォルトは 0 です。

-ISpL
推論ルールの重ね合わせ左を有効または無効にします。 デフォルトは 0 です。

-IORe
推論ルールの順序付き解決を有効または無効にします。 1 に設定すると、注文済み
解像度は有効ですが、方程式を使用した解像度の推論は生成されません。 もし
2 に設定すると、方程式は順序解決ステップでも考慮されます。 デフォルトは
0.

-ISRe
推論ルールの標準解像度を有効または無効にします。 1 に設定すると、標準
解像度は有効ですが、方程式を使用した解像度の推論は生成されません。 もし
2 に設定すると、方程式は標準解像度ステップでも考慮されます。 デフォルトは
0.

-ISHy
推論ルールの標準ハイパーレゾリューションを有効または無効にします。 デフォルトは 0 です。

-IOHy
推論ルール Ordered Hyper-Resolution を有効または無効にします。 デフォルトは 0 です。

-IURR
推論ルールの単位結果の解決を有効または無効にします。 デフォルトは 0 です。

-IOFc
推論ルール Ordered Factoring を有効または無効にします。 1 に設定すると、注文済みファクタリング
は有効ですが、正のリテラルを使用した因数分解推論のみが生成されます。 設定されている場合
から 2 までは、負のリテラルも推論の対象となります。 デフォルトは 0 です。

-ISFc
推論ルールの標準ファクタリングを有効または無効にします。 デフォルトは 0 です。

-IUnR
推論ルールの単位解像度を有効または無効にします。 デフォルトは 0 です。

-イブル
推論ルールの境界深度単位解像度を有効または無効にします。 デフォルトは 0 です。

-IDEF
推論ルールの「定義の適用」を有効または無効にします。 現在サポートされていません。
デフォルトは0です。

-RFRew
リダクション ルール Forward Rewriting を有効または無効にします。 1単位に設定すると書き換えと
包含テストに基づく非単位書き換えが有効になります。 さらに2に設定すると
ユニットおよび非ユニットへの書き換えローカルコンテキスト書き換えがアクティブ化されます。 3に設定した場合
単位および非単位の書き換えに加えて、サブタームの文脈書き換えも行われます。
活性化されました。 サブターム文脈書き換えは、ローカル文脈書き換えを包含します。 設定されている場合
4 の書き換えルールに加えて、サブタームのコンテキスト書き換えもテストされます。
否定的なリテラルの削除用。 デフォルトは 0 です。

-RBリュー
リダクションルール「Backward Rewriting」を有効または無効にします。 と同じ価値観と意味
フラグ -RFRew 用ですが、逆方向に使用されます。 デフォルトは 0 です。

-RFMRR
削減ルールの前方一致置換解決を有効または無効にします。 デフォルト
0です。

-RBMRR
リダクション ルール後方一致置換解決を有効または無効にします。 デフォルト
0です。

-RObv
リダクションルール「明らかなリダクション」を有効または無効にします。 デフォルトは 0 です。

-RUNC
削減ルール「ユニット競合」を有効または無効にします。 デフォルトは 0 です。

-RTer
非単位句の最大数を設定することでターミネータを有効または無効にします。
検索時に使用します。 デフォルトは 0 です。

-RTaut
削減ルールのトートロジー削除を有効または無効にします。 1 に設定すると、構文のみ
トートロジーが検出され、削除されます。 2 に設定すると、さらに意味論的なトートロジーが追加されます。
が削除されます。 デフォルトは 0 です。

-RSST
リダクション ルールの静的ソフト タイピングを有効または無効にします。 デフォルトは 0 です。

-RSSi
削減ルールの並べ替えの簡略化を有効または無効にします。 デフォルトは 0 です。

-RFサブ
前方包含削除の削減ルールを有効または無効にします。 デフォルトは 0 です。

-RBサブ
削減ルール「後方包含削除」を有効または無効にします。 デフォルトは 0 です。

-レイド
リダクション ルールの割り当て方程式の削除を有効または無効にします。 このルールにより削除されるのは、
文節からの方程式の特定の出現。 1 に設定すると、削減量は次のようになります。
健全であることが保証されています。 2 に設定した場合、削減は可能性がある場合にのみ効果的です。
考慮されている問題のモデルには自明ではない領域があります。 デフォルトは 0 です。

-Rコン
縮小ルール「凝縮」を有効または無効にします。 デフォルトは 0 です。

-TDfg2Otterオプション
Otter オプション ヘッダーの組み込みを有効または無効にします。 このオプションは以下にのみ適用されます
dfg2カワウソ。 1 に設定すると、Otter をほぼ完成させる設定が含まれます。 設定されている場合
2 に設定すると auto モードがアクティブになり、3 に設定すると auto2 モードがアクティブになります。 デフォルトは
0.

-EML
モーダル ロジックまたは記述ロジック式用の特別な EML フラグ。 決してそうする必要はありません
明示的に設定します。 解析中に設定されます。

-EMLオート
EML Autonomous モードを対象としていますが、まだ機能していません。 デフォルトは 0 です。

-EML翻訳
様相ロジックまたは記述ロジック式に使用される変換方法を決定します。
0 に設定すると、標準のリレーショナル変換方法 (
通常の Kripke セマンティクス) が使用されます。 1 に設定すると、関数変換方法は次のようになります。
使用済み。 2 に設定すると、最適化された関数変換方法が使用されます。 3 に設定すると、
半関数変換法が使用されます。 最適化されたもののバリエーション
以下の設定が指定されている場合、関数変換方式が使用されます。
-EMLTranslation=2 -EMLFuncNary=1。 翻訳はn進数で行われます
単項述語とパスの代わりに述語を使用します。 現在の実装では、
標準のリレーショナル変換方法が最も一般的です。 いくつかの制限が適用されます
他の方法。 機能翻訳法と半機能翻訳
メソッドは基本的なマルチモーダル ロジックでのみ使用できます。 K(m) おそらくシリアル付き
(合計) モダリティ (-EML Theory=1)、プラス名目 (ABox ステートメント)、用語
公理と一般包含および等価公理。 最適化された機能
翻訳メソッドは以下に対してのみ実装されます。 K(m)、おそらくシリアルモダリティを使用します。
デフォルトは0です。

-EML2Rel
設定すると、命題/ブール型の式が関係式に変換されます。
一次ロジックに変換される前に。 デフォルトは 0 です。

-EML理論
どの背景理論を仮定するかを決定します。 0 に設定すると、背景理論は次のようになります。
空の。 1 に設定すると、シリアル性 (KD の背景理論) がすべてのオブジェクトに追加されます。
モダリティ。 2 に設定すると、反射性 (KT の背景理論) が追加されます。
すべてのモダリティ。 3 に設定すると、対称性 (KB の背景理論) が追加されます。
あらゆるモダリティに対応。 4 に設定すると、推移性 (K4 の背景理論) は次のようになります。
すべてのモダリティに追加されます。 5 に設定すると、ユークリッドネス (
K5) はすべてのモダリティに追加されます。 6 に設定すると、推移性とユークリッド性
(S4 の背景理論) がすべてのモダリティに追加されます。 7 に設定すると、
再帰性、推移性、ユークリッド性 (S5 の背景理論) を追加
あらゆるモダリティに対応。 デフォルトは 0 です。

-EMLFuncNdeQ
設定されている場合、ダイヤモンドの式は tr(dia(phi),s) = nde(s) /\ に従って変換されます。
x tr(phi,[sx]) (ande / 数量詞の式)、それ以外の場合、翻訳は次のようになります。
tr(dia(phi),s) = 存在する x nde(s) /\ tr(phi,[sx]) (量指定子 / nde に従う)
式）。 ボックス式の変換は二重に定義されます。 このフラグを設定するのは、
機能的または半機能的変換メソッドのフラグが設定されている場合にのみ意味があります。
が設定されています。 デフォルトは 1 です。

-EMLFuncNary
設定されている場合、溝付きロジックへの関数変換が使用されます。 これは n 進数を意味します
述語記号は、単項述語記号とパスの代わりに使用されます。 これを設定する
flag は、マルチモーダル K での局所的な充足可能性/妥当性をテストする場合にのみ意味があります。
デフォルトは0です。

-EMLFソート
設定すると、用語の並べ替えが使用されます。 デフォルトは 0 です。

-EMLEリムコンプ
設定されている場合は、モーダル パラメーター内のリレーショナル構成を排除するようにしてください。 デフォルトは 0 です。

-EMLPトランス
設定されている場合、EML から 0 次ロジックへの変換が文書化されます。 デフォルトは XNUMX です。

-TPTP
設定されている場合、SPASS は TPTP 構文の入力ファイルを想定します。 デフォルトは 0 です。

-rf 設定すると、SPASS は終了前に入力ファイルを削除します。 デフォルトは 0 です。

例

オプションを指定せずに単一のファイルに対して SPASS を実行するには:

スパスⅠ

最終結果を除くすべての SPASS 出力を無効にするには:

SPASS -PGiven=0 -P問題=0 I

注意事項

入力問題で SPASS のオプションを指定することもできます。 DFG 構文では、次のようになります。
つかいます

設定のリスト(SPASS)。
{*
set_flag(DocProof,1)。
*}
end_of_list。

DocProof フラグを設定します。

入力で設定できるオプションは XNUMX 種類あります。

set_flag( 、 ）。
フラグを値に設定します。 有効なフラグと値については、「オプション」セクションで説明します。

set_precedence( ）。
リストされたシンボルの優先順位を設定します。 優先順位は左から順に低くなります。
右、つまり、一番左のシンボルが最も高い優先順位を持ちます。

リスト内のすべてのエントリには次の形式があります

記号 | (シンボル、重み [, {l, r, m}])

XNUMX 番目の形式を使用して、シンボル (KBO の場合) またはステータス (KBO の場合) に重みを割り当てることができます。
RPOS）。 ステータスは、左から右の場合は @t{l}、マルチセットの場合は @t{m}、または左から右の場合は @t{r} のいずれかです。
右から左に。 重みは整数で与えられます。

set_DomPred( ）。
リストされた述語 (ドムプレド 支配的な述語の場合) シンボルは最初に次のように順序付けされます
引数のリストに従ってではなく、優先順位に従って。 等しい場合のみ
述語の場合、引数が検査されます。 たとえば、次のオプションを追加すると、

set_DomPred(P)。

それから条項の中で

-> R(f(x,y),a)、P(x,a)。

原子 P(x,a) は厳密に最大です。 によってリストされる述語 set_DomPred オプションは
優先順位に従って比較します。

set_selection( ）。
Select フラグで使用できる選択リストを設定します (上記を参照)。

set_ClauseFormulaRelation( 、のシーケンス
公理名の文字列))。
このリストは特に FLOTTER によって設定され、最終的に見つかったリストに対して SPASS を有効にします。
証明で使用される文節と入力との関係を示す証明
数式。 オプション DocProof と組み合わせる場合は、すべての項目にエントリが必要です。
条項番号。 それ以外の場合は、エラーが報告されます。

set_ClauseFormulaRelation((1,ax2),(2,ax1),(3,ax3,ax1)).

onworks.netサービスを利用してFLOTTERをオンラインで利用する