Unrealizability logic (UL) was proposed by Kim et al. as the first Hoare-style proof system for proving properties that hold for an infinite set of programs (defined by a regular tree grammar). The goal of our work is to automate reasoning and proof generation for UL. A key ingredient in UL is the notion of nonterminal summaries-inductive facts that characterize recursive nonterminals in the grammar that defines the set of programs. They are analogous to procedure summaries in Hoare logic. The goal of automating UL led us to reformulate the inference rules-in particular, introducing a unified rule for nonterminal summaries, called the rule of adaptation, which draws inspiration from how procedure summaries are handled in Hoare logic. In the same way that verification conditions can be used to synthesize loop invariants for Hoare logic proofs, our reformulation of UL reduces the problem of synthesizing a nonterminal summary to a Syntax-Guided Synthesis problem. We implement Wuldo, the first checker and synthesizer for UL. Wuldo can express proofs beyond the reach of existing tools, including proofs that establish how infinitely many programs behave on infinitely many inputs, and in some cases Wuldo can even synthesize the needed nonterminal summaries.

翻译：非现实逻辑（UL）由Kim等人提出，是首个用于证明由正则树文法定义的无限程序集合所满足性质的霍尔风格证明系统。本研究的目标是实现UL推理与证明生成的自动化。UL的核心要素是"非终结符摘要"——表征定义程序集合的文法中递归非终结符的归纳事实，类似于霍尔逻辑中的过程摘要。自动化UL的目标促使我们重新表述推理规则，特别是引入一个统一的非终结符摘要规则"适配规则"，其灵感源自霍尔逻辑中处理过程摘要的方式。正如验证条件可用于合成霍尔逻辑证明中的循环不变量，我们对UL的重新表述将非终结符摘要的合成问题简化为语法引导的合成问题。我们实现了Wuldo——首个UL验证器与合成器。Wuldo能表达现有工具无法企及的证明，包括建立无限程序在无限输入上行为的证明，并在某些情况下能自动合成所需的非终结符摘要。