Does anyone know how Semantic Tableaux works?.. Here is an example: || (a=>b) ^ c c||(a=>b) (a=>b) || c c,a|| || c, a, b b,c||a I need it to work in java.. any ideas? I am having problems developing it when the tableaux splits into 2 when 2 options are needed. this is what ive got so far.. Code: public class Algorithm { LinkedList left; LinkedList right; //Gains Node root from parser and passes to Algorithm and creates and new linkedlist left and right public Algorithm(Node root) { parent = new LinkedList(); left = new LinkedList(); right = new LinkedList(); right.addElement(root, 0); //adds root to rightList and sets the count of that tree to 0 (heirarchy/treeid) int count = 0; while((left.length() > 0) || (right.length() > 0)){ while (right.length() > 0) { Node temp = right.getElement(); if(temp.data == "^") { right.deleteElement(); left.addElement(temp.left, count); right.addElement(temp.right, count); count++; left.addElement(temp.right, count); right.addElement(temp.left, count); Node tmp = temp.left; System.out.println(tmp.data); tmp = temp.right; System.out.println(tmp.data); } if (temp.data == "=>") { System.out.println(temp.data ); Node tmp = temp.left; System.out.println(tmp.data); tmp = temp.right; System.out.println(tmp.data); right.deleteElement(); left.addElement(temp.left, count); right.addElement(temp.right, count); } if (temp.data == "v") { right.deleteElement(); left.addElement(temp.left, count); right.addElement(temp.right, count); count++; left.addElement(temp.right, count); right.addElement(temp.left, count); Node tmp = temp.left; System.out.println(tmp.data); tmp = temp.right; System.out.println(tmp.data); } if (temp.data == "-") { left.addElement(temp.right, count); right.deleteElement(); } } while(left.length() > 0) { Node temp = (Node) left.getElement(); if(temp.data == "^") { left.addElement(temp.left, count); left.addElement(temp.right, count); left.deleteElement(); Node tmp = (Node) left.data; System.out.println(tmp.data); tmp = (Node) right.data; System.out.println(tmp.data); } if(temp.data == "v") { left.addElement(temp.left, count); right.addElement(temp.right, count); count++; left.addElement(temp.right, count); left.addElement(temp.left, count); left.deleteElement(); Node tmp = (Node) left.data; System.out.println(tmp.data); tmp = (Node) right.data; System.out.println(tmp.data); } if(temp.data == "=>") { left.addElement(temp.right, count); right.addElement(temp.left, count); count ++; right.addElement(temp.right, count); right.addElement(temp.left, count); left.deleteElement(); Node tmp = (Node) left.data; System.out.println(tmp.data); tmp = (Node) right.data; System.out.println(tmp.data); } if(temp.data == "-") { right.addElement(temp.left, count); left.deleteElement(); } } } } } class Node { public String data; public Node left ; public Node right ; }