de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Impressum Kontakt Einloggen
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Hochschulschrift

Superposition Extended with Sorts

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44467

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

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-0014-AD24-B
Zusammenfassung
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.