Automated theorem proving in a combination of theories with disjoint signatures

Abstract

We present a method for automated theorem proving in a combination of theories with disjoint signatures. The Nelson-Oppen combination technique for decision procedures is used to combine separate theorem provers in different theories. The provers being combined are based on the Prolog Technology Theorem Proving method and they use the SLD resolution (alternatively Model Elimination) as an inference system. Our approach enables to tune up the provers for different theories separately and increases the effciency of automated theorem proving in a combination of theories.