|
Description: |
1. generalization wrt to invariant parts of the proofs (e.g.graphs of rule applications etc).Here we distinguish generalizations of the simple form (as in cut-free proofs or in presence of least number principle) from
generalizations of more complex types (as in order induction). In this context,
identity scheme is the most powerful scheme. As a corollary, we show, that all
classical tautologies with at most n variables can be derived using a
Frege-type calculus with equivalence rule within a fixed number of steps.
2. generalization wrt to an underlying meaning. Here proofs and calculations are
considered as trees of formal expressions and a most general form of sound rule applications wrt subsequent expressions in the tree. These schematic rules are then unified. We analyze the famous calculation of Euler, that the 5th fermat number is compound.
3. generalization wrt premises of the proof. This type of generalization is the bases of a proof theory of analogical reasoning and in consequence of juridical reasoning.
Area(s): LOGIC AND COMPUTATION
|
