Herbrand's theorem, automated deduction and semantic tableaux

A. Voronkov (logic seminar)


We make a complexity analysis of decision problems arising in connection with the use of Herbrand's theorem in automated deduction. We prove several results about 1. Formula Instantiation: the problem of instantiating a quantifier-free formula to a valid formula; 2. Strategies in tableau-like methods. We also formulate new research directions and associated open problems.