התחל במצב לא מקוון עם האפליקציה Player FM !
Introduction to Cut Elimination
Manage episode 303395793 series 2823367
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.
161 פרקים
Manage episode 303395793 series 2823367
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.
161 פרקים
כל הפרקים
×ברוכים הבאים אל Player FM!
Player FM סורק את האינטרנט עבור פודקאסטים באיכות גבוהה בשבילכם כדי שתהנו מהם כרגע. זה יישום הפודקאסט הטוב ביותר והוא עובד על אנדרואיד, iPhone ואינטרנט. הירשמו לסנכרון מנויים במכשירים שונים.