Abstract
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.
Get full access to this article
View all access options for this article.
