Bahareh Afshari, Stefan Hetzl & Graham E. Leigh (2015):
Herbrand disjunctions, cut elimination and context-free tree grammars.
In: Thorsten Altenkirch: 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015),
Leibniz International Proceedings in Informatics (LIPIcs) 38.
Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik,
Dagstuhl, Germany,
pp. 1–16,
doi:10.4230/LIPIcs.TLCA.2015.1.
Bahareh Afshari, Stefan Hetzl & Graham E. Leigh (2016):
Herbrand confluence for first-order proofs with Π_2-cuts.
In: Dieter Probst & Peter Schuster: Concepts of Proof in Mathematics, Philosophy, and Computer Science,
Ontos Mathematical Logic.
De Gruyter,
Berlin, Boston.
isbn: 978-1-5015-0262-0. Preprint avaiable at http://dmg.tuwien.ac.at/afshari/publications.html.
Samuel R. Buss (1995):
On Herbrand's theorem.
In: Logic and Computational Complexity,
Lecture Notes in Computer Science 960.
Springer,
pp. 195–209,
doi:10.1007/3-540-60178-3_85.
Sebastian Eberhard & Stefan Hetzl:
On the compressibility of finite languages and formal proofs.
In preparation, preprint available at http://www.logic.at/people/hetzl/research/.
Sebastian Eberhard & Stefan Hetzl (2015):
Compressibility of finite languages by grammars.
In: Jeffrey Shallit & Alexander Okhotin: Descriptional Complexity of Formal Systems (DCFS) 2015,
Lecture Notes in Computer Science 9118.
Springer,
pp. 93–104,
doi:10.1007/978-3-319-19225-3_8.
Sebastian Eberhard & Stefan Hetzl (2015):
Inductive theorem proving based on tree grammars.
Annals of Pure and Applied Logic 166(6),
pp. 665 – 700,
doi:10.1016/j.apal.2015.01.002.
Philipp Gerhardy & Ulrich Kohlenbach (2005):
Extracting Herbrand disjunctions by functional interpretation.
Archive for Mathematical Logic 44,
pp. 633–644,
doi:10.1007/s00153-005-0275-1.
Willem Heijltjes (2010):
Classical proof forestry.
Annals of Pure and Applied Logic 161(11),
pp. 1346–1366,
doi:10.1016/j.apal.2010.04.006.
Jacques Herbrand (1930):
Recherches sur la théorie de la démonstration.
Université de Paris.
Stefan Hetzl (2012):
Applying tree languages in proof theory.
In: Adrian-Horia Dediu & Carlos Martín-Vide: Language and Automata Theory and Applications (LATA) 2012,
Lecture Notes in Computer Science 7183.
Springer,
pp. 301–312,
doi:10.1007/978-3-642-28332-1_26.
Stefan Hetzl, Alexander Leitsch, Giselle Reis, Janos Tapolczai & Daniel Weller (2014):
Introducing quantified cuts in logic with equality.
In: Stéphane Demri, Deepak Kapur & Christoph Weidenbach: Automated Reasoning - 7th International Joint Conference, IJCAR,
Lecture Notes in Computer Science 8562.
Springer,
pp. 240–254,
doi:10.1007/978-3-319-08587-6_17.
Stefan Hetzl, Alexander Leitsch, Giselle Reis & Daniel Weller (2014):
Algorithmic introduction of quantified cuts.
Theoretical Computer Science 549,
pp. 1–16,
doi:10.1016/j.tcs.2014.05.018.
Stefan Hetzl, Alexander Leitsch & Daniel Weller (2012):
Towards algorithmic cut-introduction.
In: Andrei Bjørner, Nikolaj & Voronkov: Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18),
Lecture Notes in Computer Science 7180.
Springer,
pp. 228–242,
doi:10.1007/978-3-642-28717-6_19.
Stefan Hetzl & Daniel Weller (2013):
Expansion trees with cut.
Preprint available at http://arxiv.org/abs/1308.0428.
David Hilbert & Paul Bernays (1939):
Grundlagen der Mathematik II.
Springer.
Richard McKinley (2013):
Proof nets for Herbrand's theorem.
ACM Transactions on Computational Logic 14(1),
pp. 5:1–5:31,
doi:10.1145/2422085.2422090.
Dale Miller (1987):
A compact representation of proofs.
Studia Logica 46(4),
pp. 347–370,
doi:10.1007/BF00370646.
eptcs@eptcs.org