Gaede, Bernd

Superposition Extended with Sorts

Sorted problem formulations often result in shorter proofs.
In this thesis, the integration of ordered inference rules and rules for
sort constraints in one calculus and the resulting system architecture
for its implementation SPASS are presented. Thus, SPASS (Synergetic Prover
Augmenting Superposition with Sorted logic) is a theorem-proving program
for first-order logic with equality and sorts.