The following pages link to Descente Infinie + Deduction (Q4809499):
Displaying 15 items.
- \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps (Q429596) (← links)
- Mechanically certifying formula-based Noetherian induction reasoning (Q507366) (← links)
- Hilbert's epsilon as an operator of indefinite committed choice (Q946570) (← links)
- Herbrand's fundamental theorem in the eyes of Jean van Heijenoort (Q1942097) (← links)
- Historical and foundational details on the method of infinite descent: every prime number of the form \(4n+1\) is the sum of two squares (Q2151525) (← links)
- Combining induction and saturation-based theorem proving (Q2303240) (← links)
- Shallow confluence of conditional term rewriting systems (Q2518609) (← links)
- A study on the teaching of proofs using the method of infinite descent (Q2802087) (← links)
- Finite Arithmetic with Infinite Descent (Q3032254) (← links)
- Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables (Q3094165) (← links)
- Sequent calculi for induction and infinite descent (Q3103982) (← links)
- Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities (Q3522029) (← links)
- Computer-assisted human-oriented inductive theorem proving by descente infinie--a manifesto (Q4913999) (← links)
- Automated Cyclic Entailment Proofs in Separation Logic (Q5200020) (← links)
- Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs (Q6059221) (← links)
