Paper: Abstract Saturation-Based Inference (at LICS 2003)

Authors: Nachum Dershowitz Claude Kirchner

Abstract

Solving goals-like deciding word problems or resolving constraints-is much easier in some theory presentations than in others. What have been called "completion processes", in particular in the study of equational logic, involve finding appropriate presentations of a given theory to solve easily a given class of problems. We provide a general proof-theoretic setting within which completion-like processes can be modelled and studied. This framework centers around well-founded orderings of proofs. It allows for abstract definitions and very general characterizations of saturation processes and redundancy criteria.

BibTeX

  @InProceedings{DershowitzKirchner-AbstractSaturationB,
    author = 	 {Nachum Dershowitz and Claude Kirchner},
    title = 	 {Abstract Saturation-Based Inference},
    booktitle =  {Proceedings of the Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2003)},
    year =	 {2003},
    month =	 {June}, 
    pages =      {65--74},
    location =   {Ottawa, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }