Herbrand's theorem has been extended to by using expansion-tree proofs.[3] The deep representation of expansion-tree proofs corresponds to a Herbrand disjunction, when restricted to first-order logic.
higher-order logic
Herbrand disjunctions and expansion-tree proofs have been extended with a notion of cut. Due to the complexity of cut-elimination, Herbrand disjunctions with cuts can be non-elementarily smaller than a standard Herbrand disjunction.
Herbrand disjunctions have been generalized to Herbrand sequents, allowing Herbrand's theorem to be stated for sequents: "a Skolemized sequent is derivable if and only if it has a Herbrand sequent".
Herbrand structure
Herbrand interpretation
Herbrand universe
Compactness theorem
(1995), "On Herbrand's Theorem", in Maurice, Daniel; Leivant, Raphaël (eds.), Logic and Computational Complexity, Lecture Notes in Computer Science, Berlin, New York: Springer-Verlag, pp. 195–209, ISBN 978-3-540-60178-4.