Notesclub

created by hec & contributors

terms privacy

Tableaux - Propositional

tableaux_propositional.livemd

David Fuenmayor

@davfuenmayor

automated-reasoning-elixi...

Share to X

Share to Bluesky

More notebooks

Tableaux - Propositional

Mix.install([
  {:picosat_elixir, "~> 0.2.3"}
])

One-sided Tableaux

The internal AST representation of boolean formulas employed in our tableaux procedures consists in:

Propositional variables: They are the “atomic” formulas of the language. As the name indicates, they are variables that can be assigned truth-values (true or false). Their internal representation is as pairs of the form: {:pvar, <variable_name>} where <variable_name> is an Elixir atom.
Connectives: They are the “constructors” for complex formulas of the language. They have an arity. For instance, the boolean constants (true, false) are nullary connectives; negation (not) is a unary connective; conjunction, disjunction and implication (and, or, ~>) are binary connectives. Connectives are divided into primitive and defined. Note that only primitive connectives get their own AST representation; defined connectives are interpreted in terms of primitive ones during parsing. Nullary connectives (when they are primitive) are represented in our AST as Elixir atoms, e.g. :true (or true as Elixir allows). Unary connectives are pairs of the form {<connective>, <argument>}, e.g. {:not, <some_formula>}. Binary connectives are triples of the form {<connective>, <argument1>, <argument2>}, e.g. {:and, <some_formula>, <another_formula>}.

Our AST for boolean expressions has been conveniently chosen as a slightly modified version of Elixir’s. This way we can employ Elixir’s syntax for boolean expressions as input syntax for our procedures, while reusing Elixir’s parser to seamlessly transform Elixir ASTs into our own ASTs (see quote/unquote).

Before diving into the tableaux procedures, we shall revisit some terminology commonly employed in the automated reasoning literature:

Literal: is either a propositional variable (positive literal) or a negated propositional variable (negative literal).
Clause: is a set of literals (often interpreted as a disjunction, but not in this case).

We represent clauses as pairs of sets of propositional variables {pos, neg}, thus keeping positive and negative literals conveniently separated.

The tableaux procedures presented below are tail recursive and each recursive execution is called a “branch”. The procedure works by recursively deconstructing formulas until obtaining their constituent literals, which are continuously agreggated into a clause (one per “branch”).

The initial execution can be intuitively understood as the “main branch”. At each point, the “current branch” grows as the procedure invokes itself once (as tail call). “Branching” occurs when the procedure invokes itself two (or more) times. When this happens, the “parent branch” blocks until (some) the “children branches” terminate. A “branch” terminates because of one of two reasons:

All formulas have been deconstructed (aka. “branch saturates”): Returns the constructed clause.
After finding a pair of contradictory literals (aka. “branch closes”). Returns nil.

Minimal-Signature Tableaux

As mentioned previously, we have a degree of freedom when it comes at choosing which connectives are primitive and which ones are defined in terms of them. A minimal-signature tableaux takes as primitive any functionally complete set of connectives. We illustrate this below by taking conjunction (AND) and negation (NOT) as primitive.

defmodule TableauxMin do
  @empty_clause {MapSet.new(), MapSet.new()}

  # Propositional variables are represented as (non-boolean) Elixir atoms
  def parse(v) when is_atom(v) and not is_boolean(v), do: {:pvar, v}

  # The primitive connectives are only conjunction and negation.  
  def parse({:and, _, [p, q]}), do: {:and, parse(p), parse(q)}
  def parse({:not, _, [p]}), do: {:not, parse(p)}

  # Disjunction is interpreted via de Morgan law: "p or q := -(-p and -q)"
  def parse({:or, _, [p, q]}), do: parse(quote do: not (not unquote(p) and not unquote(q)))

  # False is interpreted as a contradiction of the form "x and -x" (for an arbitrary prop. var "x")
  def parse(false), do: parse(quote do: :x and not :x)
  # True is interpreted as the negation of false
  def parse(true), do: parse(quote do: not false)

  # Implication is convenienty added as infix arrow "~>" and interpreted as: "p ~> q := -p or q".
  # Double implication infix arrow "<~>" is interpreted as: "p <~> q := (p ~> q) and (q ~> p)".
  # WARNING: "~>" and "<~>" have higher precedence than "and" and "or" (against convention!!)
  def parse({:~>, _, [p, q]}), do: parse(quote do: not unquote(p) or unquote(q))

  def parse({:<~>, _, [p, q]}),
    do: parse(quote do: unquote(p) ~> unquote(q) and unquote(q) ~> unquote(p))

  # Checks whether the given list of formulas is satisfiable by invoking the tableaux procedure
  def sat(formulas) when is_list(formulas) do
    formulas |> Enum.map(&parse/1) |> tableaux(@empty_clause) |> as_assignment()
  end

  # We can invoke sat on a single formula too
  def sat(formula), do: sat([formula])

  # Verifies that the conclusion follows from the given list of assumptions by checking whether the
  # negated conclusion together with the assumptions is unsatisfiable.
  def prove(conclusion, assumptions \\ []) do
    neg_conclusion = quote do: not unquote(conclusion)

    case sat([neg_conclusion | assumptions]) do
      :unsat -> :valid
      assignment -> {:countersat, assignment}
    end
  end

  # A minimalistic tableaux procedure (using only conjunction and negation as primitives)
  defp tableaux(formulas, {pos, neg} = clause) do
    case formulas do
      # Empty: branch has been fully expanded and we are done. Return clause
      [] ->
        clause

      # Literal: If the propositional variable appears in both the positive and the negative part
      # of the clause, then it cannot be assigned a truth-value, and thus we "close" the branch.
      # Otherwise, we add the propositional variable to the corresponding part of the clause.
      [{:pvar, v} | rest] ->
        if MapSet.member?(neg, v) do
          nil
        else
          tableaux(rest, {MapSet.put(pos, v), neg})
        end

      [{:not, {:pvar, v}} | rest] ->
        if MapSet.member?(pos, v) do
          nil
        else
          tableaux(rest, {pos, MapSet.put(neg, v)})
        end

      # Double negation: simplify away
      [{:not, {:not, a}} | rest] ->
        tableaux([a | rest], clause)

      # Conjunction: non-branching decomposition
      [{:and, a, b} | rest] ->
        tableaux([a | [b | rest]], clause)

      # Negated conjunction: (shortcut) branching    
      [{:not, {:and, a, b}} | rest] ->
        tableaux([{:not, a} | rest], clause) || tableaux([{:not, b} | rest], clause)
    end
  end

  # Converts a clause into an "assignment" (function that maps prop. variables to truth-values)
  defp as_assignment(nil), do: :unsat

  defp as_assignment({pos, neg}),
    do: Enum.map(pos, fn v -> {v, true} end) ++ Enum.map(neg, fn v -> {v, false} end)
end

Before testing our tableaux procedure, we shall note that having a minimal signature often blows up the size of formulas after parsing:

formula = quote do: (:a <~> (:b or :c)) ~> (:c ~> :a)
TableauxMin.parse formula

The previous formula is in fact a theorem

 TableauxMin.prove(formula)

We illustrate the use of our tableaux procedure with some more examples:

# An invalid formula (negation of the theorem: distributivity of disjunction over conjunction)
formula = quote do: not ((:a or (:b and :c)) <~> ((:a or :b) and (:a or :c)))
formula |> TableauxMin.prove() |> inspect() |> IO.puts()
# Moreover
formula |> TableauxMin.sat() |> inspect() |> IO.puts()

# A (non-trivially) valid inference
assumption1 = quote do: :p or :q
assumption2 = quote do: :s and not :q
conclusion = quote do: :p and :s
conclusion |> TableauxMin.prove([assumption1, assumption2]) |> inspect() |> IO.puts()
[conclusion, assumption1, assumption2] |> TableauxMin.sat() |> inspect() |> IO.puts()

# A trivially valid inference (assumptions are inconsistent)
assumption1 = quote do: :p and :q
assumption2 = quote do: :s and not :q
conclusion = quote do: :x
conclusion |> TableauxMin.prove([assumption1, assumption2]) |> inspect() |> IO.puts()
[assumption1, assumption2] |> TableauxMin.sat() |> inspect() |> IO.puts()

# A non-valid (yet consistent) inference
assumption1 = quote do: :p or :q
assumption2 = quote do: :s and not :r
conclusion = quote do: :p
conclusion |> TableauxMin.prove([assumption1, assumption2]) |> inspect() |> IO.puts()
[conclusion, assumption1, assumption2] |> TableauxMin.sat() |> inspect() |> IO.puts()

Maximal-Signature Tableaux

On the other hand, we can design our tableaux procedure to work with all connectives as primitive ones. This makes the definition of the procedure longer (we need to take more cases into account), but has the benefit of not blowing up the size of input formulas.

defmodule TableauxMax do
  @empty_clause {MapSet.new(), MapSet.new()}

  # Propositional variables are represented as (non-boolean) Elixir atoms
  def parse(v) when is_atom(v) and not is_boolean(v), do: {:pvar, v}

  # All connectives are primitive now  
  def parse({:and, _, [p, q]}), do: {:and, parse(p), parse(q)}
  def parse({:or, _, [p, q]}), do: {:or, parse(p), parse(q)}
  def parse({:not, _, [p]}), do: {:not, parse(p)}
  def parse(b) when is_boolean(b), do: b
  # WARNING: "~>" and "<~>" have higher precedence than "and" and "or" (against convention!!)
  def parse({:~>, _, [p, q]}), do: {:~>, parse(p), parse(q)}
  def parse({:<~>, _, [p, q]}), do: {:<~>, parse(p), parse(q)}

  # Checks whether the given list of formulas is satisfiable by invoking the tableaux procedure
  def sat(formulas) when is_list(formulas) do
    formulas |> Enum.map(&parse/1) |> tableaux(@empty_clause) |> as_assignment()
  end

  # We can invoke sat on a single formula too
  def sat(formula), do: sat([formula])

  # Verifies that the conclusion follows from the given list of assumptions by checking whether the
  # negated conclusion together with the assumptions is unsatisfiable.
  def prove(conclusion, assumptions \\ []) do
    neg_conclusion = quote do: not unquote(conclusion)

    case sat([neg_conclusion | assumptions]) do
      :unsat -> :valid
      assignment -> {:countersat, assignment}
    end
  end

  # A tableaux procedure with all connectives as primitive
  defp tableaux(formulas, {pos, neg} = clause) do
    case formulas do
      # Empty: branch has been fully expanded and we are done. Return clause
      [] ->
        clause

      # Literal: If the propositional variable appears in both the positive and the negative part
      # of the clause, then it cannot be assigned a truth-value, and thus we "close" the branch.
      # Otherwise, we add the propositional variable to the corresponding part of the clause.
      [{:pvar, v} | rest] ->
        if MapSet.member?(neg, v) do
          nil
        else
          tableaux(rest, {MapSet.put(pos, v), neg})
        end

      [{:not, {:pvar, v}} | rest] ->
        if MapSet.member?(pos, v) do
          nil
        else
          tableaux(rest, {pos, MapSet.put(neg, v)})
        end

      # Double negation: simplify away
      [{:not, {:not, a}} | rest] ->
        tableaux([a | rest], clause)

      # Constants true resp. false (and their negations): simplify away resp. close branch
      [true | rest] ->
        tableaux(rest, clause)

      [false | _rest] ->
        nil

      [{:not, false} | rest] ->
        tableaux(rest, clause)

      [{:not, true} | _rest] ->
        nil

      # Conjunction, negated disjunction, negated implication: non-branching decomposition
      [{:and, a, b} | rest] ->
        tableaux([a | [b | rest]], clause)

      [{:not, {:or, a, b}} | rest] ->
        tableaux([{:not, a} | [{:not, b} | rest]], clause)

      [{:not, {:~>, a, b}} | rest] ->
        tableaux([a | [{:not, b} | rest]], clause)

      # Disjunction, negated conjunction, implication: (shortcut) branching
      [{:or, a, b} | rest] ->
        tableaux([a | rest], clause) || tableaux([b | rest], clause)

      [{:not, {:and, a, b}} | rest] ->
        tableaux([{:not, a} | rest], clause) || tableaux([{:not, b} | rest], clause)

      [{:~>, a, b} | rest] ->
        tableaux([{:not, a} | rest], clause) || tableaux([b | rest], clause)

      # Double implication, and its negation (aka. XOR): both decomposition and (shortcut) branching
      [{:<~>, a, b} | rest] ->
        tableaux([a | [b | rest]], clause) || tableaux([{:not, a} | [{:not, b} | rest]], clause)

      [{:not, {:<~>, a, b}} | rest] ->
        tableaux([a | [{:not, b} | rest]], clause) || tableaux([{:not, a} | [b | rest]], clause)
    end
  end

  # Converts a clause into an "assignment" (function that maps prop. variables to truth-values)
  defp as_assignment(nil), do: :unsat

  defp as_assignment({pos, neg}),
    do: Enum.map(pos, fn v -> {v, true} end) ++ Enum.map(neg, fn v -> {v, false} end)
end

In contrast to the minimal-signature case, formulas don’t blow up after parsing:

formula = quote do: :a <~> (:b or :c) ~> (:c ~> :a)
TableauxMax.parse(formula)

And again, the previous formula is a theorem:

TableauxMax.prove(formula)

Feel free to test more examples, for instance:

# A (non-trivially) valid inference
assumption1 = quote do: :p or :q
assumption2 = quote do: :s and not :q
conclusion = quote do: :p and :s
conclusion |> TableauxMax.prove([assumption1, assumption2]) |> inspect() |> IO.puts()
[conclusion, assumption1, assumption2] |> TableauxMax.sat() |> inspect() |> IO.puts()

Sequent-based (two-sided) Tableaux

The tableaux procedure can also be seen from the point of view of the sequent calculus. Basically, by interpreting tableaux rules as sequent calculus rules read backwards (bottom-up).

The procedure below illustrates more functionalities than the ones shown previously. In particular, it allows to compute clause normal forms (CNF) which are useful intermediate representations of logical problems. CNF representations can be, for instance, fed as input to conventional SAT solvers like PicoSAT and others (via DIMACS CNF format).

defmodule TableauxSeq do
  @emptyset MapSet.new()

  def parse(v) when is_atom(v) and not is_boolean(v), do: {:pvar, v}
  def parse({:and, _, [p, q]}), do: {:and, parse(p), parse(q)}
  def parse({:or, _, [p, q]}), do: {:or, parse(p), parse(q)}
  def parse({:~>, _, [p, q]}), do: {:impl, parse(p), parse(q)}
  def parse({:not, _, [p]}), do: {:not, parse(p)}
  def parse(b) when is_boolean(b), do: b

  def parse({:<~>, _, [p, q]}),
    do: parse(quote do: unquote(p) ~> unquote(q) and unquote(q) ~> unquote(p))

  def clausify(left, right) do
    tableaux(&union_branching/4, {[parse(left)], [parse(right)]})
  end

  def clausify(formula) do
    tableaux(&union_branching/4, {[], [parse(formula)]})
  end

  def prove(formula) do
    countermodel = tableaux(&shortcut_branching/4, {[], [parse(formula)]})

    if countermodel != @emptyset do
      countermodel |> MapSet.to_list() |> List.first() |> as_assignment()
    else
      true
    end
  end

  def sat(formula) do
    model = tableaux(&shortcut_branching/4, {[parse(formula)], []})

    if model != @emptyset do
      model |> MapSet.to_list() |> List.first() |> as_assignment()
    else
      false
    end
  end

  def tableaux(strategy, seq, clause_left \\ @emptyset, clause_right \\ @emptyset) do
    case seq do
      ##########################################################
      # empty sequent: we are finished (branch is "saturated"), return clause (as singleton)
      {[], []} ->
        MapSet.new([{clause_left, clause_right}])

      ##########################################################
      # propositional variable: check whether clause becomes trivial (branch is "closed"),
      # if so, finish by returning no clauses, otherwise add atom to clause and continue
      {[{:pvar, p} | seq_left], seq_right} ->
        if MapSet.member?(clause_right, p) do
          @emptyset
        else
          tableaux(strategy, {seq_left, seq_right}, MapSet.put(clause_left, p), clause_right)
        end

      {seq_left, [{:pvar, p} | seq_right]} ->
        if MapSet.member?(clause_left, p) do
          @emptyset
        else
          tableaux(strategy, {seq_left, seq_right}, clause_left, MapSet.put(clause_right, p))
        end

      ##########################################################
      # constants true resp. false: simplify
      {[true | seq_left], seq_right} ->
        tableaux(strategy, {seq_left, seq_right}, clause_left, clause_right)

      {seq_left, [false | seq_right]} ->
        tableaux(strategy, {seq_left, seq_right}, clause_left, clause_right)

      {_seq_left, [true | _seq_right]} ->
        @emptyset

      {[false | _seq_left], _seq_right} ->
        @emptyset

      ##########################################################
      # negation: swap sides
      {[{:not, a} | seq_left], seq_right} ->
        tableaux(strategy, {seq_left, [a | seq_right]}, clause_left, clause_right)

      {seq_left, [{:not, a} | seq_right]} ->
        tableaux(strategy, {[a | seq_left], seq_right}, clause_left, clause_right)

      ##########################################################
      # conjunction, disjunction and implication - Part I: non-branching decomposition
      {[{:and, a, b} | seq_left], seq_right} ->
        tableaux(strategy, {[a | [b | seq_left]], seq_right}, clause_left, clause_right)

      {seq_left, [{:or, a, b} | seq_right]} ->
        tableaux(strategy, {seq_left, [a | [b | seq_right]]}, clause_left, clause_right)

      {seq_left, [{:impl, a, b} | seq_right]} ->
        tableaux(strategy, {[a | seq_left], [b | seq_right]}, clause_left, clause_right)

      ##########################################################
      # conjunction, disjunction and implication - Part II: branching (according to strategy)           
      {seq_left, [{:and, a, b} | seq_right]} ->
        strategy.(
          {seq_left, [a | seq_right]},
          {seq_left, [b | seq_right]},
          clause_left,
          clause_right
        )

      {[{:or, a, b} | seq_left], seq_right} ->
        strategy.(
          {[a | seq_left], seq_right},
          {[b | seq_left], seq_right},
          clause_left,
          clause_right
        )

      {[{:impl, a, b} | seq_left], seq_right} ->
        strategy.(
          {seq_left, [a | seq_right]},
          {[b | seq_left], seq_right},
          clause_left,
          clause_right
        )
    end
  end

  defp union_branching(seq1, seq2, clause_left, clause_right) do
    MapSet.union(
      tableaux(&union_branching/4, seq1, clause_left, clause_right),
      tableaux(&union_branching/4, seq2, clause_left, clause_right)
    )
  end

  defp shortcut_branching(seq1, seq2, clause_left, clause_right) do
    clauses = tableaux(&shortcut_branching/4, seq1, clause_left, clause_right)

    if clauses != @emptyset do
      clauses
    else
      tableaux(&shortcut_branching/4, seq2, clause_left, clause_right)
    end
  end

  def as_assignment({left, right}),
    do: Enum.map(left, fn v -> {v, true} end) ++ Enum.map(right, fn v -> {v, false} end)
end

formula1 = quote do: ((:a or (:b and :c)) <~> ((:a or :b) and (:a or :c)))
TableauxSeq.prove formula1

formula2 = quote do: ((:a or (:b and :c)) <~> ((:a or :b) or (:a or :c)))
TableauxSeq.prove formula2

The module below provides some useful functionality for pretty-printing as well as exporting as (DIMACS) CNF.

defmodule TableauxUtils do

  def print_clauses(clauses) do
    clauses |> MapSet.to_list() |> Enum.map(&as_sequent/1) |> Enum.join(", ")
  end

  def as_sequent({left, right}) do
    lhs = left |> MapSet.to_list() |> Enum.map(&Atom.to_string/1) |> Enum.join(", ")
    rhs = right |> MapSet.to_list() |> Enum.map(&Atom.to_string/1) |> Enum.join(", ")
    "(#{lhs} ⊢ #{rhs})"
  end

  # maps atoms to integers, alphabetically starting with 1
  def index_variables(clauses) do
    clauses
    |> Enum.flat_map(fn {left, right} -> MapSet.to_list(left) ++ MapSet.to_list(right) end)
    |> Enum.uniq()
    |> Enum.sort()
    |> Enum.with_index(1)
    |> Map.new()
  end

  # exports as list-based CNF format 
  def as_cnf_list(index, clauses) do
    clauses
    |> Enum.map(fn {neg, pos} -> Enum.map(neg, &(-index[&1])) ++ Enum.map(pos, &index[&1]) end)
  end

  # exports as DIMACS CNF format for SAT solvers
  def as_cnf_dimacs(index, clauses, comments \\ "") do
    problem =
      clauses
      |> Enum.map(fn {neg, pos} ->
        literals = Enum.map(neg, &(-index[&1])) ++ Enum.map(pos, &index[&1])
        Enum.join(literals, " ") <> " 0"
      end)
      |> Enum.join("\n")

    "c #{comments}\n" <> "p cnf #{map_size(index)} #{MapSet.size(clauses)}\n" <> problem
  end
end

formula2 |> TableauxSeq.clausify() |> TableauxUtils.print_clauses()

formula = quote do: not ((:a or :c) and (:a or :c)) ~> (:a or (:b and :c))
IO.puts (inspect (TableauxSeq.prove formula))
clauses = TableauxSeq.clausify formula
IO.puts (inspect clauses)
IO.puts TableauxUtils.print_clauses(clauses)
index = TableauxUtils.index_variables(clauses)
cnf= TableauxUtils.as_cnf_list(index,clauses)
IO.puts (inspect cnf)
IO.puts (inspect TableauxUtils.as_cnf_dimacs(index,clauses, "my example"))
Picosat.solve(cnf)

Other notebooks:

Marc Hayes
@Morgahl

req_noaa

NM Active Alerts

example.livemd

advanced gen-server iot kino kino_maplibre req_noaa

2024-12-31
Jeremy Brayton
@w0rd-driven

livebook_notebooks

Job Application Fields to Markdown

req--job_fields.livemd

tutorial intermediate kino kino_lab kino_vega_lite kino_db req req_easyhtml

2022-8-18
Ammar Massoud
@ammar-mohamed-massoud

Elixir-DockYard

Task Drills

task_drills.livemd

tutorial advanced gen-server otp jason kino youtube hidden_cell

2026-5-19
@DeSchoel

Elixir_Curriculum

Livebook

livebook.livemd

tutorial intermediate jason kino youtube hidden_cell smart_animation

2026-1-10
@DockYard-Academy

curriculum

Home Page

deprecated_home_page.livemd

tutorial beginner jason kino youtube hidden_cell

2026-5-23
Ryo Wakabayashi
@RyoWakabayashi

elixir-learning

農地のNDVI

fields_ndvi.livemd

tutorial advanced data-science nx evision exla geo jason kino kino_maplibre kino_vega_lite

2026-5-31
Marcio Klepacz
@marciok

2025-sf-tech-week

2025 SF Tech Week 🌉

tech-week-sf.livemd

tutorial advanced data-science apis jason req kino_maplibre kino_vega_lite kino_explorer kino_db exqlite kino_bumblebee exla

2025-9-23

Back