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.
Editor(s) Uwe Brahm | Created 03/26/1996 03:49:51 PM | |
Revisions 2. 1. 0. | Editor(s) Uwe Brahm Uwe Brahm Uwe Brahm/MPII/DE | Edit Dates 03/25/98 07:21:32 PM 03/23/98 07:02:03 PM 03/26/96 03:51:41 PM |