科学・技術
タルスキの高校代数問題に対するSAT攻撃
A SAT Attack on Tarski's High School Algebra Problem (arxiv.org)
要約
本論文では、タルスキの高校代数問題における最小の反例モデルのサイズが12であることをSATソルバーを用いて証明した。さらに、12要素の反例モデルが8,957,952個存在することを示し、それらの分類も行った。このSATアプローチは、既存の専用ツールよりも優れており、結果の正しさはLeanで自動形式化により証明されている。
全文翻訳
数学 > 論理 arXiv:2608.08421 (math) [2026年8月9日投稿] タイトル:タルスキの高校代数問題に対するSAT攻撃 著者:Bernardo Subercaseaux, Benjamin Przybocki Bernardo SubercaseauxとBenjamin Przybockiによるタルスキの高校代数問題に関する論文のPDFを表示 PDF HTML (実験的) 表示 要旨:タルスキの高校代数問題は、正の整数における加算、乗算、指数演算に関する全ての真の恒等式が、11個の初等恒等式のリストから導き出せるかどうかを問うものである。驚くべきことに、Wilkieは、以下の恒等式が正の整数上で有効であるが、タルスキの公理からは導き出せないことを示した:
((1+x)^y + (1+x+x^2)^y)^x * ((1+x^3)^x + (1+x^2+x^4)^x)^y = ((1+x)^x + (1+x+x^2)^x)^y * ((1+x^3)^y + (1+x^2+x^4)^y)^x.
Gurevičは、タルスキの公理を満たすがWilkieの恒等式を満たさない59要素の代数を示し、長年にわたり数人の著者がそのような反例モデルのサイズを縮小し、BurrisとYeatsによる12個のサイズの反例モデルが最終的なものとなった。一方、Zhangは11個未満の要素を持つ反例モデルは存在しないことを証明した。SATを用いて、最小の反例モデルはBurrisとYeatsが推測した通り12個であることを証明する。さらに、同型写像を除いて12個の要素を持つ反例モデルが正確に8,957,952個存在することを示し、それらの単純な分類を提供する。我々のSATアプローチは、等式理論における反例モデルを見つけるための専用ツールであるMace4およびSEMを上回る。さらに、自動形式化を用いて、我々の主結果の正しさをLeanで証明する。コメント:21ページ 主題:論理 (math.LO); 計算機科学における論理 (cs.LO) 引用形式: arXiv:2608.08421 [math.LO] (またはこのバージョンの場合は arXiv:2608.08421v1 [math.LO]) https://doi.org/10.48550/arXiv.2608.08421 詳細はこちら arXiv-issued DOI via DataCite 投稿履歴 From: Bernardo Anibal Subercaseaux Roa [メール表示] [v1] Sun, 9 Aug 2026 02:32:31 UTC (32 KB) フルテキストリンク:論文にアクセス: Bernardo SubercaseauxとBenjamin Przybockiによるタルスキの高校代数問題に関する論文のPDFを表示 PDF HTML (実験的) TeXソース 表示ライセンス 現在のブラウジングコンテキスト: math.LO < 前 | 次 > 新着 | 最近 | 2026-08 のブラウジングに変更: cs cs.LO math 参考文献と引用 NASA ADS Google Scholar Semantic Scholar エクスポート BibTeX 引用の読み込み中... BibTeX形式の引用 ×読み込み中... Data provided by: ブックマーク 参考文献ツール 参考文献と引用ツール 参考文献エクスプローラー 参考文献エクスプローラーを切り替える (エクスプローラーとは？) Connected Papers Connected Papers を切り替える (Connected Papersとは？) Litmaps Litmaps を切り替える (Litmapsとは？) scite.ai scite Smart Citations を切り替える (Smart Citationsとは？) コード、データ、メディア この論文に関連するコード、データ、メディア alphaXiv alphaXiv を切り替える (alphaXivとは？) コード検索へのリンク この論文に関連するコード検索 CatalyzeX コードファインダー (CatalyzeXとは？) DagsHub DagsHub を切り替える (DagsHubとは？) GotitPub Gotit.pub を切り替える (GotitPubとは？) Huggingface Hugging Face を切り替える (Huggingfaceとは？) ScienceCast ScienceCast を切り替える (ScienceCastとは？) デモ Replicate デモを切り替える (Replicateとは？) Spaces Hugging Face Spaces を切り替える (Spacesとは？) Spaces TXYZ.AI を切り替える (TXYZ.AIとは？) 関連論文 レコメンダーおよび検索ツール Influence Flower へのリンク Influence Flower (Influence Flowersとは？) CORE レコメンダーを切り替える CORE レコメンダー (COREとは？) 著者はこの論文の推薦者ですか？ | MathJax を無効にする (MathJaxとは？)