Abstract of Paper


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.