View in EDS PDF Full Text

Paramodulation with Well-founded Orderings.

Saved in:
Bibliographic Details
Title: Paramodulation with Well-founded Orderings.
Authors: BOFILL, MIQUEL1 mbofill@ima.udg.edu, RUBIO, ALBERT2 rubio@lsi.upc.edu
Source: Journal of Logic & Computation. Apr2009, Vol. 19 Issue 2, p263-302. 40p.
Subjects: Rewriting systems (Computer science), Equations, Proof theory, Monotonic functions, Completeness theorem, Mathematical logic
Abstract: For many years, all existing completeness results for Knuth-Bendix completion and ordered paramodulation required the term ordering ¿ to be well-founded, monotonic and total(izable) on ground terms. Then, it was shown that well-foundedness and the subterm property were enough for ensuring completeness of ordered paramodulation. Here we show that the subterm property is not necessary either. By using a new restricted form of rewriting, we obtain a completeness proof of ordered paramodulation for Horn clauses with equality, where well-foundedness of the ordering suffices. Apart from the theoretical significance of this result, some potential applications motivating the interest of dropping the subterm property are given. The proof of the results included in this article, being still technical in some parts, is pretty much shorter and easier to read than the one we have in the preliminary version of this work presented at the CADE, 2002 conference (Bofill, and Rubio, 2002, CADE, Vol. 2392 of LNAI, pp. 456-470). [ABSTRACT FROM AUTHOR]
Copyright of Journal of Logic & Computation is the property of Oxford University Press / USA and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Links:
  – Type: pdflink
Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 38604268
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Paramodulation with Well-founded Orderings.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22BOFILL%2C+MIQUEL%22">BOFILL, MIQUEL</searchLink><relatesTo>1</relatesTo><i> mbofill@ima.udg.edu</i><br /><searchLink fieldCode="AR" term="%22RUBIO%2C+ALBERT%22">RUBIO, ALBERT</searchLink><relatesTo>2</relatesTo><i> rubio@lsi.upc.edu</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Journal+of+Logic+%26+Computation%22">Journal of Logic & Computation</searchLink>. Apr2009, Vol. 19 Issue 2, p263-302. 40p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Rewriting+systems+%28Computer+science%29%22">Rewriting systems (Computer science)</searchLink><br /><searchLink fieldCode="DE" term="%22Equations%22">Equations</searchLink><br /><searchLink fieldCode="DE" term="%22Proof+theory%22">Proof theory</searchLink><br /><searchLink fieldCode="DE" term="%22Monotonic+functions%22">Monotonic functions</searchLink><br /><searchLink fieldCode="DE" term="%22Completeness+theorem%22">Completeness theorem</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematical+logic%22">Mathematical logic</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: For many years, all existing completeness results for Knuth-Bendix completion and ordered paramodulation required the term ordering ¿ to be well-founded, monotonic and total(izable) on ground terms. Then, it was shown that well-foundedness and the subterm property were enough for ensuring completeness of ordered paramodulation. Here we show that the subterm property is not necessary either. By using a new restricted form of rewriting, we obtain a completeness proof of ordered paramodulation for Horn clauses with equality, where well-foundedness of the ordering suffices. Apart from the theoretical significance of this result, some potential applications motivating the interest of dropping the subterm property are given. The proof of the results included in this article, being still technical in some parts, is pretty much shorter and easier to read than the one we have in the preliminary version of this work presented at the CADE, 2002 conference (Bofill, and Rubio, 2002, CADE, Vol. 2392 of LNAI, pp. 456-470). [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Journal of Logic & Computation is the property of Oxford University Press / USA and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=38604268
RecordInfo BibRecord:
  BibEntity:
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 40
        StartPage: 263
    Subjects:
      – SubjectFull: Rewriting systems (Computer science)
        Type: general
      – SubjectFull: Equations
        Type: general
      – SubjectFull: Proof theory
        Type: general
      – SubjectFull: Monotonic functions
        Type: general
      – SubjectFull: Completeness theorem
        Type: general
      – SubjectFull: Mathematical logic
        Type: general
    Titles:
      – TitleFull: Paramodulation with Well-founded Orderings.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: BOFILL, MIQUEL
      – PersonEntity:
          Name:
            NameFull: RUBIO, ALBERT
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 04
              Text: Apr2009
              Type: published
              Y: 2009
          Identifiers:
            – Type: issn-print
              Value: 0955792X
          Numbering:
            – Type: volume
              Value: 19
            – Type: issue
              Value: 2
          Titles:
            – TitleFull: Journal of Logic & Computation
              Type: main
ResultId 1