Abstract : We provide a general proof theoretical setting under which the so-called ``completion processes'' (as used for equational reasoning) can be modeled, understood, studied, proved and generalized. This framework---based on a well-founded ordering on proofs---allows us to derive saturation processes and redundancy criteria abstractly.
https://hal.inria.fr/inria-00107627
Contributor : Publications Loria
<>
Submitted on : Thursday, October 19, 2006 - 9:03:24 AM
Last modification on : Thursday, January 11, 2018 - 6:19:57 AM
Long-term archiving on: Wednesday, March 29, 2017 - 12:50:16 PM
