Modular instantiation schemes

Instantiation schemes are proof procedures that test the satisfiability of clause sets by instantiating the variables they contain, and testing the satisfiability of the resulting ground set of clauses. Such schemes have been devised for several theories, including fragments of linear arithmetic or theories of data-structures. In this paper we investigate under what conditions instantiation schemes can be combined to solve satisfiability problems in unions of theories.

► A method is introduced for automatically combining instantiation schemes for unions of theories.
► Sufficient conditions are devised to ensure refutational completeness.
► Existing instantiation procedures are adapted to fulfill the considered requirements.
► Some examples of applications are provided.