Ir al contenido (pulsa Retorno)

Universitat Politècnica de Catalunya

    • Català
    • Castellano
    • English
    • LoginRegisterLog in (no UPC users)
  • mailContact Us
  • world English 
    • Català
    • Castellano
    • English
  • userLogin   
      LoginRegisterLog in (no UPC users)

UPCommons. Global access to UPC knowledge

57.066 UPC E-Prints
You are here:
View Item 
  •   DSpace Home
  • E-prints
  • Grups de recerca
  • LOGPROG - Lògica i Programació
  • Reports de recerca
  • View Item
  •   DSpace Home
  • E-prints
  • Grups de recerca
  • LOGPROG - Lògica i Programació
  • Reports de recerca
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

An implementation of the KNS ordering

Thumbnail
View/Open
1400012071.pdf (373,1Kb)
Share:
 
  View Usage Statistics
Cita com:
hdl:2117/370491

Show full item record
Rivero Almeida, José MiguelMés informacióMés informacióMés informació
Document typeResearch report
Defense date1991-04
Rights accessOpen Access
Attribution-NonCommercial-NoDerivs 4.0 International
Except where otherwise noted, content on this work is licensed under a Creative Commons license : Attribution-NonCommercial-NoDerivs 4.0 International
Abstract
We describe an implementation of the KNS ordering within the TRIP system, a Quintus-Prolog written laboratory for experimenting with new rewrite-like approaches to theorem proving in first-order logic. The aim of the TRIP system is not to obtain high-performance theorem provers, but rather to test techniques that could be the basis for such theorem provers. The KNS ordering is a partial ordering scheme for proving the uniform termination of term rewriting systems, which is a crucial aspect of Knuth-Bendix completion-like theorem proving procedures. The KNS ordering is used within TRIP as a subsystem of a very general completion procedure for first-order clauses with equality, based on recent work done in this field by Bachmair and Ganzinger (1990,1991) subsuming and generalizing many known results. Our system contributes to the further development of these methods in several ways, and especially w.r.t. the definition of new techniques which are necessary for exploiting in their full power the redundancy notions that have now become available. We apply results from, where a highly simplified framework for defining Knuth-Bendix-like completion procedures for full first order clauses with equality is defined and instantiated by a new, simpler and more restrictive inference system. This implementation uses the notion of clausal rewriting (Nieuwenhuis and Orejas, 1991) for the definition of a single formalized method for proving the redundancy of clauses and inferences.
CitationRivero, J. An implementation of the KNS ordering. 1991. 
Is part ofLSI-91-40
URIhttp://hdl.handle.net/2117/370491
Collections
  • LOGPROG - Lògica i Programació - Reports de recerca [21]
  • Departament de Ciències de la Computació - Reports de recerca [1.104]
Share:
 
  View Usage Statistics

Show full item record

FilesDescriptionSizeFormatView
1400012071.pdf373,1KbPDFView/Open

Browse

This CollectionBy Issue DateAuthorsOther contributionsTitlesSubjectsThis repositoryCommunities & CollectionsBy Issue DateAuthorsOther contributionsTitlesSubjects

© UPC Obrir en finestra nova . Servei de Biblioteques, Publicacions i Arxius

info.biblioteques@upc.edu

  • About This Repository
  • Contact Us
  • Send Feedback
  • Inici de la pàgina