Automated Theorem Proving in a Combination of Theories with Disjoint Signatures
by Pavel Vanousek
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 the separate 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 efficiency of automated theorem proving in a combination of theories.