Herbrand-Confluence for Cut Elimination in Classical First Order Logic
From MaRDI portal
Publication:4649555
DOI10.4230/LIPICS.CSL.2012.320zbMath1252.03123OpenAlexW2240567774MaRDI QIDQ4649555
Lutz Straßburger, Stefan Hetzl
Publication date: 22 November 2012
Full work available at URL: https://inria.hal.science/hal-00759228
Automata and formal grammars in connection with logical questions (03D05) Classical first-order logic (03B10) Cut-elimination and normal-form theorems (03F05) Grammars and rewriting systems (68Q42)
Related Items (3)
Algorithmic introduction of quantified cuts ⋮ Expansion trees with cut ⋮ Inductive theorem proving based on tree grammars
This page was built for publication: Herbrand-Confluence for Cut Elimination in Classical First Order Logic