Instantiation Schemes for Nested Theories

Mnacho Echenim, Nicolas Peltier

This paper investigates under which conditions instantiation-based proof procedures can be combined in a nested way, in order to mechanically construct new instantiation procedures…