Strategies in Rigid-Variable Methods

We study complexity of methods using rigid variables, like the method of matings or the tableau method, on a decidable class of predicate calculus with equality. We show some intrinsic complications introduced by rigid variables. We also consider strategies for increasing multiplicity in rigid-variable methods, and formally show that the use of intelligent strategies can result in an essential gain in efficiency.

• Type: Conference
• Year: 1997
• Where: IJCAI
• Authors: Andrei Voronkov
• Keywords: IJCAI 1997, IJCAI 2007, Predicate Calculus, Rigid Variables, Tableau Method