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

MPI-INF RG1 Publications :: Thesis :: Ludwig, Michel


MPI-INF RG1 Publications
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)*:Ludwig, Michel
BibTeX citekey*:LudwigDipl2006
Language:English

Title, School
Title*:Extensions of the {Knuth-Bendix} Ordering with {LPO}-like Properties
School:Universität des Saarlandes
Type of Thesis*:Master's thesis
Month:July
Year:2006


Note, Abstract, Copyright
LaTeX Abstract:The Lexicographic Path Order (LPO) and the Knuth-Bendix

Ordering (KBO) are two prominent term orders that are
utilised in automated theorem provers. The LPO features
some properties that allow it to be used in the context
of hierarchic signature extensions and in the presence
of term definitions, where special ordering criteria are
desired for the defined terms. The KBO, on the other
hand, can be computed more efficiently than the LPO and
it correlates better with the size of terms, but the KBO
cannot be used in the afore-mentioned situations, in
which a single term should supersede infinitely many
smaller terms of arbitrary sizes. In this diploma
thesis, we present two extensions of the KBO that
overcome these limitations. The first extension order is
suitable for hierarchic signature extensions and its
main characteristic is that it uses pairs of positive
real numbers as symbol weights, whereas the second
extension can handle the required ordering of term
definitions through the usage of ordinal numbers as
symbol weights.


Referees, Status, Dates
1. Referee:Christoph Weidenbach
2. Referee:Uwe Waldmann
Supervisor:Uwe Waldmann
Status:Completed
Date Kolloquium:- - -

Correlation
MPG Subunit:RG1
Audience:experts only
Appearance:MPG publications list


BibTeX Entry:
@MASTERSTHESIS{LudwigDipl2006,
AUTHOR = {Ludwig, Michel},
TITLE = {Extensions of the {Knuth-Bendix} Ordering with {LPO}-like Properties},
SCHOOL = {Universit{\"a}t des Saarlandes},
YEAR = {2006},
TYPE = {Master's thesis}
MONTH = {July},
}



Entry last modified by Uwe Waldmann, 04/27/2007
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 Waldmann
Created
12/20/2006 11:11:59 AM
Revision
0.



Editor
Uwe Waldmann



Edit Date
20.12.2006 11:11:59