非表示:
キーワード:
-
要旨:
SPASS+T is an extension of the superposition-based theorem prover SPASS that
allows us to enlarge the reasoning capabilities of SPASS using an arbitrary SMT
procedure for arithmetic and free function symbols as a black-box. We discuss
the architecture of SPASS+T and the capabilities, limitations, and applications
of such a combination.