Analytic tableaux and model elimination

That there exist relationships between Model Elimination and Analytic Tableaux has been known for some time. However, the mapping between these procedures has not been shown explicitly to date. In order to define the mapping between the procedures, we need to use two reduction techniques which avoid the generation of duplicate subtrees in tableaux. By identifying the parallels between the two procedures, we have been able to develop a technique so that lemmas can be produced as a side-effect of closing branches within the tableau. Further, we have developed a control structure for Model Elimination which bears many similarities to that used for analytic tableau.