Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

Publications Master Template :: Thesis :: Gaede, Bernd


Publications Master Template
Show all entries of:this year (2019)last year (2018)two years ago (2017)Open in Notes
Action:login to update

Thesis - Master's thesis | @MastersThesis | Masterarbeit


Author
Author(s)*:Gaede, Bernd
BibTeX citekey*:Gaede95-Mastersthesis
Language:English

Title, School
Title*:Superposition Extended with Sorts
School:Universität Kaiserslautern
Type of Thesis*:Master's thesis
Month:July
Year:1995


Note, Abstract, Copyright
LaTeX 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.

Referees, Status, Dates
Status:Completed
Date Kolloquium:22 September 2019

Correlation
MPG Unit:Max-Planck-Institut für Informatik
MPG Subunit:Programming Logics Group
Audience:experts only
Appearance:MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list

BibTeX Entry:

@MASTERSTHESIS{Gaede95-Mastersthesis,
AUTHOR = {Gaede, Bernd},
TITLE = {Superposition Extended with Sorts},
SCHOOL = {Universit{\"a}t Kaiserslautern},
YEAR = {1995},
TYPE = {Master's thesis}
MONTH = {July},
}



Entry last modified by Uwe Brahm, 03/12/2010
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

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