今後のセミナー情報(Future schedule)
今後のセミナー情報(Future schedule)
Title: 算術における証明変換とspeed-up
Venue: Complex A 801
Time: 15:00-
Abstract: TがSのΓ-保存拡大であることを示す際に最もよく使われるのは、SのモデルMから、Γ-文の真偽がMと一致するようなTのモデルを構成する手法である。ただしこれは「T⊢φならばS⊢φ」の対偶を示しており、「Tで証明できるΓ-論理式はSでも証明できる」以上の情報はもたらさない。一方、T⊢φの証明図をS⊢φの証明図へと具体的に書き換える方法が得られれば、「もとのTにおける証明のサイズに対して、書き換え後のSにおける証明のサイズはどれくらい大きくなるのか」といった量的な情報も得られる。今回は、ACA_0からPAへの証明変換およびΣ^1_1-AC_0からACA_0への証明変換を具体例として取り上げ、superexponentialな証明変換およびpolynomialな証明変換を与える際の基本的な道具であるCut除去定理やshortening cutを紹介する。また、ACA_0におけるPAのspeed-up、すなわちACA_0からPAへの証明変換における証明サイズの増大についてsuperexponentialの上界が最良であることを、shortening cutを用いて示す。
Title: グラフから定まる Artin Gorenstein 環の Lefschetz 性と決定論的判定
Venue: Complex A 801
Time: 15:00-
Abstract: Artin Gorenstein 環は有限性（Artin 性）と対称性（Gorenstein 性）を兼ね備えた次数付き環である。
この環において 1 次の元による次数成分間の掛け算写像が単射または全射となる性質を Lefschetz 性と呼ぶが、どのような環が Lefschetz 性を満たすかについては未解明な点が多い。
本研究では、頂点数の少ないグラフから定まる Artin Gorenstein 環を列挙して調べることで、Lefschetz 性を満たさない具体例を発見した。
Lefschetz 性の有無は対応する多項式行列の正則性と同値であり、Schwartz-Zippel の補題を用いた確率論的判定法が一般的であるが、本研究ではさらに、計算機を用いた決定論的判定手法を提案した。
本講演では、多項式行列の構成などについて述べたのち、その非正則性を決定論的に判定する計算手法を解説する。