Herbrand's Theorem for Prenex Goedel Logic and Its Consequences for Theorem Proving

摘要

Herbrand's Theorem for G_∞~Δ, i.e., Goedel 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.