返回Google圖書搜尋

A Computational Proof Procedure; Axioms for Number Theory; Research on Hilbert's Tenth Problem

出版	Air Force Office of Scientific Research, Air Research and Development, United States Air Force, 1959
URL	http://books.google.com.hk/books?id=izGs-DR5tTgC&hl=&source=gbs_api

註釋Abstract for Part 1: A method is described whereby, given any valid formula of quantification theory, one may mechanically obtain a proof of the given formula. The method is based on Herbrand's theorem, and has essentially two parts: the first part is a scheme for generating a sequence of "quantifier-free lines" such that the conjunction of the first n of these lines must be inconsistent for some n if the given formular was inconsistent; and the second part is a method for testing the conjunction of the first n "quantifier-free lines" for consistency as n=1,2,3, ... (More abstract material excluded here).