ACM/IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Eighteenth Annual IEEE Symposium on

Logic in Computer Science (LICS 2003)

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

Authors: Nachum Dershowitz Claude Kirchner


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.


    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}

Last modified: 2022-10-3113:49
Sam Staton