• DocumentCode
    2271276
  • Title

    Proof by consistency in equational theories

  • Author

    Bachmair, Leo

  • Author_Institution
    Dept. of Comput. Sci., State Univ. of New York, Stony Brook, NY, USA
  • fYear
    1988
  • fDate
    0-0 1988
  • Firstpage
    228
  • Lastpage
    233
  • Abstract
    A method is proven for proving that equations are valid in the initial model of an equational variety. This proof by consistency procedure can be applied to equational theories that are represented as ground convergent rewrite systems. In contrast with so-called inductive completion procedures, the method requires no specific ordering on terms and can handle unorientable equations. The method is linear and refutationally complete, in that it refutes any equation which is not an inductive theorem.<>
  • Keywords
    theorem proving; equational theories; ground convergent rewrite systems; proof by consistency; Algebra; Computer languages; Computer science; Equations; Logic functions; Terminology;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 1988. LICS '88., Proceedings of the Third Annual Symposium on
  • Conference_Location
    Edinburgh, UK
  • Print_ISBN
    0-8186-0853-6
  • Type

    conf

  • DOI
    10.1109/LICS.1988.5122
  • Filename
    5122
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=2271276