Herbrand's theorem and term induction |
| |
| Authors: | Matthias Baaz Georg Moser |
| |
| Institution: | (1) Institut für Diskrete Mathematik und Geometrie, Vienna University of Technology, E104, Wiedner Hauptstrasse 8–10, Austria;(2) Computational Logic, University of Innsbruck, Technikerstrasse 21a, Austria |
| |
| Abstract: | We study the formal first order system TIND in the standard language of Gentzen's LK . TIND extends LK by the purely logical
rule of term-induction, that is a restricted induction principle, deriving numerals instead of arbitrary terms. This rule may be conceived as the
logical image of full induction. |
| |
| Keywords: | 03F07 03F20 03B10 03B35 |
| 本文献已被 SpringerLink 等数据库收录！ |
|
