Herbrand Confluence for First-Order Proofs with Π2-Cuts
From MaRDI portal
Publication:5221602
Recommendations
- Herbrand-confluence for cut elimination in classical first order logic
- Herbrand's theorem and extractive proof theory
- Proof nets for Herbrand's theorem
- Herbrand's theorem, Skolemization and proof systems for first-order Łukasiewicz logic
- Herbrand's theorem for prenex Gödel logic and its consequences for theorem proving
- Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus
- scientific article; zbMATH DE number 3296226
- Lower and upper bounds for the provability of Herbrand consistency in weak arithmetics
- scientific article; zbMATH DE number 4204310
- Gentzen's second consistency proof and strong cut-elimination
Cited in
(10)- Herbrand disjunctions, cut elimination and context-free tree grammars
- Herbrand Proofs and Expansion Proofs as Decomposed Proofs
- Herbrand's theorem as higher order recursion
- On the generation of quantified lemmas
- Herbrand-confluence
- Herbrand-confluence for cut elimination in classical first order logic
- The \(\exists\forall^2\) fragment of the first-order theory of atomic set constraints is \(\Pi_1^0\)-hard
- Expansion trees with cut
- On the Herbrand content of LK
- On the compressibility of finite languages and formal proofs
This page was built for publication: Herbrand Confluence for First-Order Proofs with Π2-Cuts
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5221602)
