In this thesis, we propose building a parallel system through the integration of semantic trees with resolution-refutation. The proposal comes from the observations that the appropriate strategy for one class of theorems is often very different from that for another class and many semantic trees tend to be linear. In the linear semantic tree, one of the two branches from each node leads to a failure node. Such linearity is attractive because we can focus our efforts on closing the remaining branch. Unfortunately, the strategy of building a closed linear semantic tree is incomplete. To help to achieve closure, we introduce the use of unit clauses derived from resolutions when necessary, leading to a strategy that combines the construction of semantic trees with resolution-refutation.