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, } where ` 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(ortrueas Elixir allows). Unary connectives are pairs of the form{, }, e.g.. Binary connectives are triples of the form{, , }, e.g.. 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](https://hexdocs.pm/elixir/quote-and-unquote.html)). 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](https://en.wikipedia.org/wiki/Tail_call) 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: 1. All formulas have been deconstructed (aka. "branch saturates"): Returns the constructed clause. 2. After finding a pair of contradictory literals (aka. "branch closes"). Returnsnil`. ## 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. elixir 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: elixir formula = quote do: (:a <~> (:b or :c)) ~> (:c ~> :a) TableauxMin.parse formula The previous formula is in fact a theorem elixir TableauxMin.prove(formula) We illustrate the use of our tableaux procedure with some more examples: elixir # 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() elixir # 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() elixir # 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() elixir # 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. elixir 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: elixir formula = quote do: :a <~> (:b or :c) ~> (:c ~> :a) TableauxMax.parse(formula) And again, the previous formula is a theorem: elixir TableauxMax.prove(formula) Feel free to test more examples, for instance: elixir # 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). elixir 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 elixir formula1 = quote do: ((:a or (:b and :c)) <~> ((:a or :b) and (:a or :c))) TableauxSeq.prove formula1 elixir 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. elixir 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 elixir formula2 |> TableauxSeq.clausify() |> TableauxUtils.print_clauses() elixir 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)