Subformulation property
From Encyclopedia of Mathematics
subformula property
A property of certain logical calculi and logico-mathematical calculi (cf. Logical 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). To improve effectivity in such a search, various specializations and generalizations of the subformula property are used.
Comments
References
| [a1] | H. Schwichtenberg, "Some applications of cut-elimination" J. Barwise (ed.) , Handbook of mathematical logic , North-Holland (1977) pp. 867–896 (esp. 876) |
| [a2] | E.W. Beth, "Formal methods" , Reidel (1962) pp. Sects. 27–28 |
| [a3] | S.C. Kleene, "Introduction to metamathematics" , North-Holland (1950) pp. 450 |
How to Cite This Entry:
Subformulation property. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Subformulation_property&oldid=32086
Subformulation property. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Subformulation_property&oldid=32086
This article was adapted from an original article by S.Yu. Maslov (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article