未ログイン ／
ログイン
← ファイル一覧
（保存にはログインが要ります）
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 ★2026-10-04 現状へ直した＝記号変数（?R^ 等）は、どの投げ先でも Thm 全体で1つの決まった述語として扱う !txt （Satallax でも式ごとに ∀ で閉じない・0_tutorial_AI/HOL.book「推論関係とbackend」）。述語への代入が要るときは schema の実例を書く。 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 ◀ sos)|cls-elim +sos Wc. prover9 search:seconds 10 vampire search:seconds 90 prover+ problem:split
表示（保存しません）
保存にはMatheliaへのログインが要ります。