Sahlqvist Formula - Definition

Definition

Sahlqvist formulas are built up from implications, where the consequent is positive and the antecedent is of a restricted form.

  • A boxed atom is a propositional atom preceded by a number (possibly 0) of boxes, i.e. a formula of the form (often abbreviated as for ).
  • A Sahlqvist antecedent is a formula constructed using ∧, ∨, and from boxed atoms, and negative formulas (including the constants ⊥, ⊤).
  • A Sahlqvist implication is a formula AB, where A is a Sahlqvist antecedent, and B is a positive formula.
  • A Sahlqvist formula is constructed from Sahlqvist implications using ∧ and (unrestricted), and using ∨ on formulas with no common variables.

Read more about this topic:  Sahlqvist Formula

Famous quotes containing the word definition:

    It is very hard to give a just definition of love. The most we can say of it is this: that in the soul, it is a desire to rule; in the spirit, it is a sympathy; and in the body, it is but a hidden and subtle desire to possess—after many mysteries—what one loves.
    François, Duc De La Rochefoucauld (1613–1680)

    It’s a rare parent who can see his or her child clearly and objectively. At a school board meeting I attended . . . the only definition of a gifted child on which everyone in the audience could agree was “mine.”
    Jane Adams (20th century)