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.

翻译：本文通过将逻辑系统与有限抽象系统性地关联起来，为抽象解释开发了一种证明论框架。基于先前关于抽象内部逻辑的研究，我们提出了一种通用程序，用于生成其Lindenbaum-Tarski代数与给定抽象格同构的逻辑。该方法识别出由具体化映射保持的逻辑连接词，并推导出相应的证明规则与公理。本文在适当条件下建立了可靠性与完备性结果，将该框架推广至笛卡尔积与多变量设定，并研究了非笛卡尔抽象（如八边形）的逻辑结构。这些观察揭示了抽象解释、证明论与代数逻辑之间的新联系，为程序抽象的系统的逻辑分析奠定了基础。