The Computational Complexity of Some Logical Theories

Abstract

Upper and lower bounds on the inherent computational complexity of the decision problem for a number of logical theories are established. A general form of Ehrenfeucht game technique for deciding theories is developed which involves analyzing the expressive power of formulas with given quantifier depth. The method allows one to decide the truth of sentences by limiting quantifiers to range over finite sets.