Herbrand’s Theorem for G
∞
Δ
, i.e., Gödel logic enriched by the projection operator Δ is proved. As a consequence we obtain a “chain normal form” and
a translation of prenex G
∞
Δ
into (order) clause logic, referring to the classical theory of dense total orders with endpoints. A chaining calculus provides
a basis for efficient theorem proving.
Partly supported by the Austrian Science Fund under grant P-12652 MAT
Research supported by EC Marie Curie fellowship HPMF-CT-1999-00301