Basic algorithm for normalizing a first order logic formula into conjunctive normal form [Ruby]

logic.rb

module Formula
  class Expr
  end

  class Lit < Expr
    attr_reader :name
    def initialize(name)
      @name = name
    end

    def to_s
      name
    end
  end

  class And < Expr
    attr_reader :expr1, :expr2
    def initialize(expr1, expr2)
      @expr1 = expr1
      @expr2 = expr2
    end

    def to_s
      "(#{expr1} ∧ #{expr2})"
    end
  end

  class Or < Expr
    attr_reader :expr1, :expr2
    def initialize(expr1, expr2)
      @expr1 = expr1
      @expr2 = expr2
    end

    def to_s
      "(#{expr1} ∨ #{expr2})"
    end
  end

  class Not < Expr
    attr_reader :expr
    def initialize(expr)
      @expr = expr
    end

    def to_s
      "(¬#{expr})"
    end
  end

  def self.demorgan(expr)
    case expr
    when Not
      expr.expr
    when Or
      And.new(Not.new(expr.expr1), Not.new(expr.expr2))
    when And
      Or.new(Not.new(expr.expr1), Not.new(expr.expr2))
    when Lit
      Not.new(expr)
    end
  end

  def self.distribute(expr1, expr2)
    case expr2
    when And
      And.new(Or.new(expr1, expr2.expr1), Or.new(expr1, expr2.expr2))
    else
      Or.new(expr1, expr2)
    end
  end

  def self.normalize(expr)
    raise "invalid expression" unless expr.is_a? Expr
    case expr
    when Not
      demorgan(normalize(expr.expr))
    when Or
      distribute(normalize(expr.expr1), normalize(expr.expr2))
    else
      expr
    end
  end
end