کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
6424847 | 1633492 | 2011 | 34 صفحه PDF | دانلود رایگان |
![عکس صفحه اول مقاله: CERES in higher-order logic CERES in higher-order logic](/preview/png/6424847.png)
We define a generalization CERESÏ of the first-order cut-elimination method CERES to higher-order logic. At the core of CERESÏ lies the computation of an (unsatisfiable) set of sequents CS(Ï) (the characteristic sequent set) from a proof Ï of a sequent S. A refutation of CS(Ï) in a higher-order resolution calculus can be used to transform cut-free parts of Ï (the proof projections) into a cut-free proof of S. An example illustrates the method and shows that CERESÏ can produce meaningful cut-free proofs in mathematics that traditional cut-elimination methods cannot reach.
⺠We give a method of cut-elimination for higher-order logic based on resolution. ⺠We prove soundness of a sequent calculus based on Skolem terms. ⺠The method is applied to a concrete mathematical proof. ⺠We find that it can obtain cut-free proofs not reachable by reductive methods.
Journal: Annals of Pure and Applied Logic - Volume 162, Issue 12, December 2011, Pages 1001-1034