Herbrand's theorem, automated deduction and semantic tableaux
A. Voronkov (logic seminar)
Abstract:
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.