One criterion which a calculus should fulfill in order to be generally suited for automated deduction is the following. It should be possible to express a short informal proof of a formula as a short formal proof of the same formula in the calculus. Otherwise the search for a proof would take an extremely long time, and also the calculus would not be very adequate for expressing in the formal calculus the idea which lies behind an informal proof. Since the concept of an informal proof is very difficult to grasp theoretically, I concentrated on the problem of the comparison of two formal calculi with each other. So, one of the problems I am investigating is the question for two calculi K1 and K2 whether any proof P1 of a formula in K1 can be transformed to a proof P2 of the same formula in K2 such that the length of P2 can be bounded from above by a polynomial of the length of P1 and, moreover, whether the transformation of the proof P1 to the proof P2 can be done in a time which can be bounded by a polynomial of the length of P1. In this case we say that the calculus K2 can polynomially simulate the calculus K1. But using a particularly efficient transformation to normal form it is also possible for normal form calculi such as resolution to simulate a non-normal form calculus such as the cut-free sequent calculus. For a detailed discussion of this area of research see the book Relative Complexities of First Order Calculi.
Connection graph resolution is a refinement of resolution obtained by restricting the applicability of resolution steps. Strong completeness means that every fair maximal deduction starting from an unsatisfiable set of clauses is a refutation. A proof of the strong completeness of connection graph resolution for propositional logic is given in the paper Decomposition of Tautologies into Regular Formulas and Strong Completeness of Connection-Graph Resolution. This implies that backtracking is not necessary in a theorem prover based on connection graph resolution for propositional logic. The lifting to first order logic is under investigation.
Proof caluli consisting of analytic rules such as the cut-free sequent calculus are suited for automated deduction by backward reasoning. Reasoning systems based on this idea are the tableau calculu and the connection method. Backward reasoning cannot be applied in a direct way to the cut rule since a given conclusion of an instance of the cut rule can have infinitely many possible pairs of premises. So present-day backward reasoning systems do not use the cut rule since Gentzen's cut elimination theorem says that for any proof of a formula with cut there is also a proof of the same formula without cut. On the other hand, cut elimination may increase the length of a proof extremely (non-elementarily). Therefore, it would be highly desirable to have an efficient backward reasoning system using the cut rule. The idea how to overcome the problem of infinite branching of the search tree is to use a sort of second order unification in order to be able to combine two or more rules of the system. Since, in general, a single most general unifier cannot be determined (as is the case in first order unification), conditions enter into the rules. For more details see the paper Backward Reasoning in Systems with Cut