Proof search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification (Q1272615)

In automated theorem proving methods the variable instantiation during proof search is usually controlled by a suitable unification algorithm. The author presents some analysis of the instantiation problem for intuitionistic logic with equality. This analysis shows close connections between variable instantiation problem and simultaneous rigid \(E\)-unification. It implies that simultaneous rigid \(E\)-unification is unavoidable in automatic proof procedures for intuitionistic logic with equality. Using a description of provability in terms of a derivation skeleton and constraints, the author shows that the existence of a derivation with a given skeleton is polynomial-time equivalent to simultaneous rigid \(E\)-unifiability. The author also shows that simultaneous rigid \(E\)-unifiability is polynomial-time reducible to intuitionistic logic with equality. These two facts show that a semi-decision algorithm for simultaneous rigid \(E\)-unifiability is necessary and sufficient for designing automated theorem-proving procedures for intuitionistic logic with equality.