Superposition Extended with Sorts

Gaede, Bernd

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Thesis

Superposition Extended with Sorts

MPS-Authors

/persons/resource/persons44467

Gaede, Bernd
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

Gaede, B. (1995). Superposition Extended with Sorts. Master Thesis, Universität Kaiserslautern, Saarbrücken.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-AD24-B

Abstract

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.