Descente Infinie + Deduction
From MaRDI portal
Publication:4809499
DOI10.1093/jigpal/12.1.1zbMath1067.03021OpenAlexW2068793017MaRDI QIDQ4809499
Publication date: 30 August 2004
Published in: Logic Journal of IGPL (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/847f0ed0ab3a9fc9103dad4fcc5103294f061261
Related Items
Historical and foundational details on the method of infinite descent: every prime number of the form \(4n+1\) is the sum of two squares ⋮ Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs ⋮ Herbrand's fundamental theorem in the eyes of Jean van Heijenoort ⋮ \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps ⋮ Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities ⋮ Hilbert's epsilon as an operator of indefinite committed choice ⋮ Mechanically certifying formula-based Noetherian induction reasoning ⋮ Automated Cyclic Entailment Proofs in Separation Logic ⋮ Shallow confluence of conditional term rewriting systems ⋮ Combining induction and saturation-based theorem proving ⋮ Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables
