| 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.
|
 Additional Information
|
Citation:
Nachum Dershowitz, Claude Kirchner,
"Abstract Saturation-Based Inference,"
lics,
p. 65,
18th Annual IEEE Symposium on Logic in Computer Science (LICS'03),
2003
|
