Definitions

from Wiktionary, Creative Commons Attribution/Share-Alike License.

  • noun logic Given a formula, a formula that is part of the given formula.

Etymologies

from Wiktionary, Creative Commons Attribution/Share-Alike License

sub- +‎ formula

Support

Help support Wordnik (and make this page ad-free) by adopting the word subformula.

Examples

  • Formulas in derivations are arranged in a linear succession, but Jaskowski's paper of 1934 remained fragmentary and without substantial results such as a subformula property.

    Chores 2009

  • The standard terminology today is “cut elimination theorem” All of the logical rules of SC have the subformula property in a very immediate sense: each formula in a premiss is a formula or subformula in the conclusion.

    Chores 2009

  • Consistency would then follow from the normalization of derivations and the subformula property.

    Chores 2009

  • It would be impossible to restrict these formulas in advance, thus no subformula property can hold.

    Chores 2009

  • Disjunction and conjunction differ only by the player who has the choice of the immediate subformula with which the game will proceed: in a conjunction, the challenger may choose, confident that either disjunct can be refuted; in a disjunction the choice lies with the defender.

    Dialogical Logic Keiff, Laurent 2009

  • Prawitz gave first a normalization theorem and subformula property for a system of natural deduction for classical logic.

    Chores 2009

  • In contrast, an application of detachment results in a formula that is a proper subformula of the major premise (and in the exceptional case when the major premise is an instance of self-identity it is identical to the minor premise).

    Combinatory Logic Bimbó, Katalin 2008

  • The axioms are all formulas of the following forms, where in the last two schemas the subformula A (t) is the result of substituting an occurrence of the term t for every free occurrence of x in A (x), and no variable free in t becomes bound in A (t) as a result of the substitution.

    Intuitionistic Logic Moschovakis, Joan 2007

  • Fortunately, NK enjoys the subformula property in the sense that each formula entering into a natural deduction proof can be restricted to being a subformula of Γ ˆª Δ ˆª {α}, where Δ is the set of auxiliary assumptions made by the ~-Elimination rule.

    Automated Reasoning Portoraro, Frederic 2005

  • By exploiting the subformula property a natural deduction automated theorem prover can drastically reduce its search space and bring the backward application of the elimination rules under control (Portoraro 1998, Sieg and Byrnes

    Automated Reasoning Portoraro, Frederic 2005

Comments

Log in or sign up to get involved in the conversation. It's quick and easy.