Bottom-up Construction of Semantic Tableaux

We present a new proof procedure for first-order logic. Our approach is closely related to semantic tableaux, but it uses a more compact representation of the search space. The idea is to construct the tableau from the leaves to the root, which helps to factorize common subtrees and reduces the information that must be stored in a given branch. We prove that the method is sound and refutationally complete and we provide simplification rules in order to prune the search space and delete redundant inferences. We show that our procedure runs in polynomial time for several propositional classes, including the Horn-renamable class or the Krom class. This article is an extended version of Peltier (2007, LNAI 4548).