The resolution principle for ω+-valued logic
Ewa S. Orłowska · Fundamenta Informaticae · 1979
A resolution-style theorem proving system for the ω+-valued Post logic is developed. The soundness and the completeness of the system are proved. The two versions of the Herbrand theorem for the logic considered are given.