Schematic Cut Elimination and the Ordered Pigeonhole Principle

详细信息    查看全文

• 刊名：Lecture Notes in Computer Science
• 出版年：2016
• 出版时间：2016
• 年：2016
• 卷：9706
• 期：1
• 页码：241-256
• 全文大小：271 KB
• 参考文献：1.Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: Ceres: An analysis of Fürstenberg’s proof of the infinity of primes. Theoret. Comput. Sci. 403(2–3), 160–175 (2008)MathSciNet CrossRef MATH
  2.Baaz, M., Leitsch, A.: On skolemization and proof complexity. Fundamenta Informaticae 20(4), 353–379 (1994)MathSciNet MATH
  3.Baaz, M., Leitsch, A.: Cut-elimination and redundancy-elimination by resolution. J. Symbolic Comput. 29, 149–176 (2000)MathSciNet CrossRef MATH
  4.Baaz, M., Leitsch, A.: Methods of Cut-Elimination. Springer Publishing Company, Incorporated (2013)
  5.Brotherston, J.: Cyclic proofs for first-order logic with inductive definitions. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol. 3702, pp. 78–92. Springer, Heidelberg (2005)CrossRef
  6.Brotherston, J., Simpson, A.: Sequent calculi for induction and infinite descent. J. Logic Comput. 22, 1177–1216 (2010)MathSciNet MATH
  7.Bundy, A.: The automation of proof by mathematical induction. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 845–911. Elsevier, Amsterdam (2001)CrossRef
  8.Cerna, D., Leitsch, A.: Analysis of clause set schema aided by automated theorem proving: Acase study (2015). arXiv:​1503.​08551v1 [cs.LO]
  9.Cerna, D., Leitsch, A.: Schematic cut elimination and the ordered pigeonhole principle [extended version] (2016). arXiv:​1601.​06548 [math.LO]
  10.Cerna, D.M.: Advances in schematic cut elimination. Ph.D. thesis, Technical University of Vienna (2015). http://​media.​obvsg.​at/​p-AC12246421-2001
  11.Comon, H.: Inductionless induction. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 913–962. Elsevier, Amsterdam (2001)CrossRef
  12.Dunchev, C.: Automation of cut-elimination in proof schemata. Ph.D. thesis, Technical University of Vienna (2012)
  13.Dunchev, C., Leitsch, A., Rukhaia, M., Weller, D.: Cut-elimination and proof schemata. In: Aher, M., Hole, D., Jeřábek, E., Kupke, C. (eds.) TbiLLC 2013. LNCS, vol. 8984, pp. 117–136. Springer, Heidelberg (2015)
  14.Gentzen, G.: Untersuchungen über das logische Schließen I. Math. Z. 39(1), 176–210 (1935)MathSciNet CrossRef MATH
  15.Girard, J.-Y.: Proof Theory and Logical Complexity. Studies in Proof Theory, vol. 1. Bibliopolis, Naples (1987)MATH
  16.Mcdowell, R., Miller, D.: Cut-elimination for a logic with definitions and induction. Theoret. Comput. Sci. 232, 2000 (1997)MathSciNet
  17.Takeuti, G.: Proof Theory. Studies in Logic and the Foundations of Mathematics, vol. 81. American Elsevier Pub., New York (1975)MATH
  18.Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 140–145. Springer, Heidelberg (2009)CrossRef
  
• 作者单位：David M. Cerna (15)
  Alexander Leitsch (16)
  
  15. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria
  16. Logic and Theory Group, Technical University of Vienna, Vienna, Austria
  
• 丛书名：Automated Reasoning
• ISBN：978-3-319-40229-1
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349
• 卷排序：9706

文摘

Schematic cut-elimination is a method of cut-elimination which can handle certain types of inductive proofs. In previous work, an attempt was made to apply the schematic CERES method to a formal proof with an arbitrary number of \(\varPi _{2}\) cuts (a recursive proof encapsulating the infinitary pigeonhole principle). However the derived schematic refutation for the characteristic clause set of the proof could not be expressed in the schematic resolution calculus developed so far. Without this formalization a Herbrand system cannot be algorithmically extracted. In this work, we provide a restriction of infinitary pigeonhole principle, the ECA-schema (Eventually Constant Assertion), or ordered infinitary pigeonhole principle, whose analysis can be completely carried out in the existing framework of schematic CERES. This is the first time the framework is used for proof analysis. From the refutation of the clause set and a substitution schema we construct a Herbrand system.