Introduction to Cut Elimination


Manage episode 303395793 series 2823367
著作 Aaron Stump の情報はPlayer FM及びコミュニティによって発見されました。著作権は出版社によって所持されます。そして、番組のオーディオは、その出版社のサーバから直接にストリーミングされます。Player FMで購読ボタンをタップし、更新できて、または他のポッドキャストアプリにフィードのURLを貼り付けます。

We saw in the last few episodes that proofs in natural deduction can be simplified by removing detours, which occur when an introduction inference is immediately followed by an elimination inference on the introduced formula. What corresponds to this for sequent calculus proofs? The answer is cut elimination. This episode describes the cut rule and what is meant by a cut-elimination procedure. We will talk more about such a procedure in the next episode.

143 つのエピソード