关于LK的Herbrand含量
On the Herbrand content of LK
摘要：
我们提出了一个结构表示的Herbrand内容的LK证明与削减的复杂性prenex Sigma-2/Pi-2。该表示采取的形式，一个类型的非确定性树文法的顺序2生成一个有限的语言的一阶项出现在Herbrand扩展通过削减消除。特别是，对于每一个根岑风格的减少之间的LK证明，我们研究的诱导语法和分类的情况下，语言平等和包容举行。
英文摘要：
We present a structural representation of the Herbrand content of LK-proofs with cuts of complexity prenex Sigma-2/Pi-2. The representation takes the form of a typed non-deterministic tree grammar of order 2 which generates a finite language of first-order terms that appear in the Herbrand expansions obtained through cut-elimination. In particular, for every Gentzen-style reduction between LK-proofs we study the induced grammars and classify the cases in which language equality and inclusion hold.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
