The resolution principle for ω + -valued logic

https://doi.org/10.3233/FI-1978-2102

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.

Keywords

theorem proving resolution Herbrand theorem semantic tree

Get full access to this article

View all access options for this article.