We present a new proof procedure for first-order logic. It is close in spirit to the usual tableaux-based procedures, but uses a more compact representation of the search space. Roughly speaking, it constructs the tableau from the leaves to the root, and tries to factorize common subtrees when possible. We study the complexity of our procedure for several prepositional classes and we show that it is polynomial for all these classes.
展开▼
