公式图式的图式反驳
Schematic Refutations of Formula Schemata
摘要：
证明图式是归纳定义的无限证明序列。在本文中，我们提出了一个一般的框架，图式的条款，公式和统一和定义的解决演算模式的量词免费的公式。新的演算推广和改进了以往的方法，图式推理。作为应用的方法，我们提出了一个示意性的反驳形式证明的鸽子洞原则的弱形式。
英文摘要：
Proof schemata are infinite sequences of proofs which are defined inductively. In this paper we present a general framework for schemata of terms, formulas and unifiers and define a resolution calculus for schemata of quantifier-free formulas. The new calculus generalizes and improves former approaches to schematic deduction. As an application of the method we present a schematic refutation formalizing a proof of a weak form of the pigeon hole principle.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
