Semantic Tableaux Generator info

Semantic Tableaux, often referred to as a truth tree, is a graphical method used in logic and formal semantics. It serves as a tool for determining the validity or satisfiability of logical formulas or sets of formulas.In this app, you can generate tree proofs for propositional logic. Work is currently in-progress to extend this app to FOL semantic Tableaux. The x at the end of each branch represents the absurdity marker for that branch.

For more detailed information, see Wikipedia

See Semantic Tableaux Generator here

Input Syntax

All uppercase alphabets are allowed as predicates. Use of empty premises is not allowed.

• Conjunction (And Operation): The operator for conjunction is represented by the symbol "∧" or "&". It combines two propositions and is true only when both propositions are true.
  Example: P ∧ Q, A & B
• Disjunction (Or Operation): The operator for disjunction is represented by the symbol "∨" or "|". It combines two propositions and is true when at least one of the propositions is true.
  Example: P ∨ Q, A | B
• Material Implication: The operator for material implication is represented by the symbol "->. It represents "if...then..." statements and is true unless the first proposition is true and the second is false.
  Example: P -> Q
• Biconditional: The operator for biconditional is represented by the symbol "<->". It represents "if and only if" statements and is true when both propositions have the same truth value.
  Example: P <-> Q
• Negation: For the operator of negation, the symbols "~", "!", and "¬" are permissible. It is used to reverse the truth value of a proposition.
  Example: ~P, !(P -> Q), ¬R

Supported Rules

• Conjunction Rule

  The Conjunction Rule is used to split a branch into two branches, each representing one of the conjuncts of a conjunction in the formula.

• Negation of Conjunction Rule

  The Negation of Conjunction Rule is used to create a branch that assumes the negation of a conjunction, effectively treating it as a disjunction of negations.

• Disjunction Rule

  The Disjunction Rule is used to create two branches, each assuming one of the disjuncts of a disjunction in the formula.

• Negation of Disjunction Rule

  The Negation of Disjunction Rule is used to create a branch that assumes the negation of a disjunction, effectively treating it as a conjunction of negations.

• Negation Rule

  The Negation Rule is used to create a branch that assumes the negation of a subformula, effectively changing the truth value of that subformula.

• Double Negation Rule

  The Double Negation Rule is used to eliminate double negations by simplifying them back to the original subformula.

• Implication Rule

  The Implication Rule is used to create two branches, one assuming the antecedent of an implication, and the other assuming the negation of the consequent.

• Negation of Implication Rule

  The Negation of Implication Rule is used to create a branch that assumes the negation of an implication, effectively treating it as a conjunction and a negation.

• Biconditional Rule

  The Biconditional Rule is used to create two branches, one assuming the conjunction of the implication in one direction, and the other assuming the conjunction of the implication in the opposite direction.

• Negation of Biconditional Rule

  The Negation of Biconditional Rule is used to create a branch that assumes the negation of a biconditional, effectively treating it as a disjunction of implications.