要約:本論文は、抽象解釈のための証明理論的枠組みを開発し、論理システムを有限の抽象化と体系的に関連付けます。抽象化の内部論理に関する先行研究を基に、与えられた抽象格子と同型なリンデンブルク＝タルスキー代数を持つ論理を生成するための一般的な手順を提案します。このアプローチは、コンクリート化マップによって保存される論理結合を特定し、対応する証明規則と公理を導出します。論文は適切な条件のもとで、 soundness と completeness の結果を確立し、カートезиアン積と多変数設定への枠組みの拡張、および八角形などのカートезиアンでない抽象化の論理構造の調査を行います。これらの観察は、抽象解釈、証明理論、および代数的論理の間の新しい関連性を示唆し、プログラム抽象化の体系的な論理的分析の基礎を提供します。
| 科目： | コンピュータサイエンスにおける論理 (cs.LO); 論理 (math.LO) |
| 引用： | arXiv:2605.26591 [cs.LO] |
| (または arXiv:2605.26591v1 [cs.LO] このバージョン用) | |
| https://doi.org/10.48550/arXiv.2605.26591 DataCiteを通じてarXiv発行のDOI（登録保留中） |
送信者: Apostolos Tzimoulis [メールを表示]
[v1]
木, 26 5月 2026 06:23:07 UTC (13 KB)
このコンテンツは慣性聚合(RSSリーダー)によって自動集約されています。参考としてご覧ください。 原文出典 — 著作権は原著者に帰属します。