View of Linear clause generation by Tableaux and DAGs | Teaching Mathematics and Computer Science