Abstract:This paper develops a proof-theoretic framework for abstract interpretation by systematically associating logical systems with finite abstractions. Building on earlier work on the internal logics of abstractions, we propose a general procedure for generating a logic whose Lindenbaum-Tarski algebra is isomorphic to a given abstract lattice. The approach identifies logical connectives preserved by the concretization map and derives corresponding proof rules and axioms. The paper establishes soundness and completeness results under suitable conditions, extends the framework to Cartesian products and multi-variable settings, and investigates the logical structure of non-Cartesian abstractions such as octagons. These observations suggest new connections between abstract interpretation, proof theory, and algebraic logic, providing a foundation for a systematic logical analysis of program abstractions.
| Subjects: | Logic in Computer Science (cs.LO); Logic (math.LO) |
| Cite as: | arXiv:2605.26591 [cs.LO] |
| (or arXiv:2605.26591v1 [cs.LO] for this version) | |
| https://doi.org/10.48550/arXiv.2605.26591 arXiv-issued DOI via DataCite (pending registration) |
From: Apostolos Tzimoulis [view email]
[v1]
Tue, 26 May 2026 06:23:07 UTC (13 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。