I would like to use Mathematica to automatically generate a semantic tableaux (truth tree) from a formula in propositional logic).

Here is an example formula:

$$(a \lor\lnot b )\land b$$

Here is the corresponding tree:

enter image description here

I am curious to know if anyone has tried to do this before. All ideas/help welcome.

For anyone interested: Here are the branching rules:

enter image description here

Finally here is the Mathematica code to manually create the tree (above).

description = {
  (a ∨ ¬ b) ∧ b -> b, 
   b -> (a ∨ ¬ b),
   (a ∨ ¬ b) -> ¬  b,
   (a ∨ ¬ b) -> a};

   (a ∨ ¬ b) ∧ b,
   VertexLabeling -> True]

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.