未ログイン ／
ログイン
← ファイル一覧
（保存にはログインが要ります）
common/zf.thmel
ヘッダ
行番号
!txt zf.thmel — default.thmel と同じだが、Vampire の探索秒数だけを伸ばす。 !txt ★search: の印が付く行は探索設定＝同じ問題を同じ形で投げ、待つ長さだけが変わる !txt （数学的な意味は変えない・default.thmelの同じ注記を参照）。 !txt ★1_basis/4_ZF.book のax_r0系補題（схема経由でR_の関係グラフを明示するもの）は、 !txt 本が紹介した語彙が増えた分だけ背景公理も増え、既定20秒ではVampireが間に合わない段が !txt 出た（実測・elim_X0：孤立させると即座に証明できるが、本全体の文脈では20秒timeout）。 !txt 60秒では依然timeoutし、90秒に伸ばすと同じ入力・同じ判定のまま証明できることを実測した。 !txt ★2026-09-16＝backend/targetへ s=satallax+ を追加（須田さん指示「satallax+を強くする」）。 !txt 命題/述語変数（?R^等）を含む多ソートの主張はSatallax+（`--| … s;`）でのみ証明できる !txt （Vampireは記号変数を1つの固定記号へbar化するため、あらゆる値を動く自由変数と !txt 結び付けられない。Satallaxは本物の高階∀量化として扱えるので、記号変数を含む式1本を !txt ∀で閉じて渡す。詳細はax_s0/tff_emitter.php::schemaVariable()）。 backend p=prover+ v=vampire+ h=hyperion s=satallax+ target p v h s sort s c f translate 0 sc inference goal -| sos <-> (goal ◀ sos)|cvt+|0 inference goal --| sos <-> goal|sc ◀ sos|sc prover9 search:seconds 10 vampire search:seconds 90 prover+ problem:split
表示（保存しません）
保存にはMatheliaへのログインが要ります。