View source for Subformulation property

''subformula property''

A property of certain logical calculi and logico-mathematical calculi (cf. [[Logical calculus|Logical calculus]]; [[Logico-mathematical calculus|Logico-mathematical calculus]]), in which the premisses of each rule in the calculus consist of subformulas of the formulas occurring in the conclusion of the rule. The subformula property enables one to organize a  "bottom-up"  derivation search (see [[Gentzen formal system|Gentzen formal system]]). To improve effectivity in such a search, various specializations and generalizations of the subformula property are used.



====Comments====


====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  H. Schwichtenberg,   "Some applications of cut-elimination"  J. Barwise (ed.) , ''Handbook of mathematical logic'' , North-Holland  (1977)  pp. 867–896 (esp. 876)</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  E.W. Beth,   "Formal methods" , Reidel  (1962)  pp. Sects. 27–28</TD></TR><TR><TD valign="top">[a3]</TD> <TD valign="top">  S.C. Kleene,   "Introduction to metamathematics" , North-Holland  (1950)  pp. 450</TD></TR></table>