Herbrand’s proof procedure.
In Jacques Herbrand's formulation of the predicate calculus, with a formula F is associated a quantifier-free formula R(i,F) of order i. The first part of what is known as Herbrand's Theorem states that, given an integer p such that R(p,F) is valid, then we can find a proof of F. In this w...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Others |
| Language: | en |
| Published: |
McGill University
1964
|
| Subjects: | |
| Online Access: | http://digitool.Library.McGill.CA:80/R/?func=dbin-jump-full&object_id=115409 |