English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse
  1. Item Summary / 
  2. View item

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
 Local TagsRelease HistoryDetailsSummary
  Extensions of the Knuth-Bendix Ordering with LPO-like Properties

Ludwig, M. (2006). Extensions of the Knuth-Bendix Ordering with LPO-like Properties. Master Thesis, Universität des Saarlandes, Saarbrücken.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-24CA-6 Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0024-AD1E-7
Genre: Thesis

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Ludwig, Michel1, Author           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 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.

Details

show
hide
Language(s): eng - English
 Dates: 20062006
 Publication Status: Issued
 Pages: -
 Publishing info: Saarbrücken : Universität des Saarlandes
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 521694
Other: Local-ID: C125716C0050FB51-EBE84532C34D57CAC125724A003807A4-LudwigDipl2006
 Degree: Master

Event

show

Legal Case

show

Project information

show

Source

show