Documentation

ComplexityTheory.Foundations.BooleanFormula

Boolean formulas #

Tree syntax and semantics for Boolean formulas. Formula size counts tree nodes, so repeated subformulas are counted repeatedly rather than shared as in a Boolean circuit.

source
@[reducible, inline]
abbrev ComplexityTheory.BooleanAssignment :
Type

A total assignment maps every natural-number variable index to a truth value. It is the environment in which Boolean formulas receive their meaning.

Equations
Instances For
    source
    def ComplexityTheory.BooleanAssignment.AgreeOn (indices : Finset ℕ) (first second : BooleanAssignment) :
    Prop

    Two assignments agree on a finite set when they give every variable in that set the same value. Differences outside the set are deliberately ignored.

    Equations
    Instances For
      source
      inductive ComplexityTheory.BooleanFormula :
      Type

      A Boolean formula represented as a tree of variables, constants, and logical connectives. The explicit syntax lets later algorithms inspect and transform formulas rather than treating them as opaque Boolean functions.

      Instances For
        source
        def ComplexityTheory.instDecidableEqBooleanFormula.decEq (x✝ x✝¹ : BooleanFormula) :
        Decidable (x✝ = x✝¹)
        Equations
        Instances For
          source
          @[implicit_reducible]
          instance ComplexityTheory.instDecidableEqBooleanFormula :
          DecidableEq BooleanFormula
          Equations
          source
          def ComplexityTheory.instReprBooleanFormula.repr :
          BooleanFormula → ℕ → Std.Format
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[implicit_reducible]
            instance ComplexityTheory.instReprBooleanFormula :
            Repr BooleanFormula
            Equations
            source
            def ComplexityTheory.BooleanFormula.eval (assignment : BooleanAssignment) :
            BooleanFormula → Bool

            Evaluate a Boolean formula under an assignment. This supplies the semantics used by satisfiability and tautology.

            Equations
            Instances For
              source
              def ComplexityTheory.BooleanFormula.size :
              BooleanFormula → ℕ

              The number of nodes in a formula tree. This is the formula-size measure used by later resource bounds.

              Equations
              Instances For
                source
                def ComplexityTheory.BooleanFormula.vars :
                BooleanFormula → Finset ℕ

                The finite set of variables occurring in a formula. Variables outside this set cannot affect evaluation.

                Equations
                Instances For
                  source
                  def ComplexityTheory.BooleanFormula.Satisfies (assignment : BooleanAssignment) (formula : BooleanFormula) :
                  Prop

                  An assignment satisfies a formula exactly when evaluation returns true; in plain language, the assignment makes the formula true.

                  Equations
                  Instances For
                    source
                    def ComplexityTheory.BooleanFormula.IsSatisfiable (formula : BooleanFormula) :
                    Prop

                    A formula is satisfiable when some assignment satisfies it. Such an assignment is a witness to satisfiability.

                    Equations
                    Instances For
                      source
                      def ComplexityTheory.BooleanFormula.IsTautology (formula : BooleanFormula) :
                      Prop

                      A formula is a tautology when every assignment satisfies it; its truth does not depend on how its variables are assigned.

                      Equations
                      Instances For
                        source
                        theorem ComplexityTheory.BooleanFormula.one_le_size (formula : BooleanFormula) :
                        1 ≤ formula.size

                        Every formula tree contains at least one node. There is no empty formula.

                        source
                        theorem ComplexityTheory.BooleanFormula.eval_eq_of_agree (formula : BooleanFormula) {first second : BooleanAssignment} :
                        BooleanAssignment.AgreeOn formula.vars first second → eval first formula = eval second formula

                        Assignments that agree on every variable occurring in a formula evaluate it identically. In plain language, variables absent from the formula do not matter.