H. Comon, P. Narendran, R. Nieuwenhuis, M. Rusinowitch
Abstract. A term rewrite system (TRS) terminates if, and only if, its rules are contained in a reduction ordering?. In order to deal with any set of equations, including inherently non-terminating...
Deciding the Confluence of Ordered Term Rewrite Systems (2003)
H. Comon, P. Narendran, R. Nieuwenhuis, M. Rusinowitch
A term rewrite system (TRS) terminates if, and only if, its rules are contained in a reduction ordering ?. In order to deal with any set of equations, including inherently non-terminating ones (like...
Induction = I-axiomatization + first-order consistency (2000)
H. Comon, R. Nieuwenhuis, Hubert Comon, Robert Nieuwenhuis
In the early 80's, there was a number of papers on what should be called proofs by consistency. They describe how to perform inductive proofs, without using an explicit induction scheme, in the...
Decision Problems in Ordered Rewriting (1998)
H. Comon, P. Narendran, R. Nieuwenhuis, M. Rusinowitch
A term rewrite system (TRS) terminates iff its rules are contained in a reduction ordering ?. In order to deal with any set of equations, including inherently non-terminating ones (like...
Decision Problems in Ordered Rewriting (1997)
Comon Narendran, H. Comon, P. Narendran, R. Nieuwenhuis, M. Rusinowitch
A term rewrite system (TRS) terminates iff its rules are contained in a reduction ordering ?. In order to deal with any set of equations, including inherently non-terminating ones (like...
Orderings, AC-Theories and Symbolic Constraint Solving (Extended Abstract) (1995)
H. Comon, R. Nieuwenhuis, A. Rubio
We design combination techniques for symbolic constraint solving in the presence of associative and commutative (AC) function symbols. This yields an algorithm for solving AC-RPO constraints (where...
Orderings, AC-Theories and Symbolic Constraint Solving (Extended Abstract) (1995)
H. Comon, R. Nieuwenhuis, A. Rubio
) H. Comon R. Nieuwenhuis A. Rubio LRI & CNRS Technical Univ. of Catalonia Bat. 490, Univ. Paris-Sud Pau Gargallo 5 91405 ORSAY cedex, France 08028 Barcelona, Spain comon@lri.fr...
Orderings, ACTheories and Symbolic Constraint Solving (1995)
H. Comon, R. Nieuwenhuis, A. Rubio
) H. Comon R. Nieuwenhuis A. Rubio LRI & CNRS Technical Univ. of Catalonia Bat. 490, Univ. Paris-Sud Pau Gargallo 5 91405 ORSAY cedex, France 08028 Barcelona, Spain comon@lri.fr...
Sequentiality, Second Order Monadic Logic and Tree Automata (1995)
Given a term rewriting system R and a normalizable term t, a redex is needed if in any reduction sequence of t to a normal form, this redex will be contracted. Roughly, R is sequential if there is an...
Sequentiality, Second Order Monadic Logic and Tree Automata (1995)
Given a term rewriting system R and a normalizable term t, a redex is needed if in any reduction sequence of t to a normal form, this redex will be contracted. Roughly, R is sequential if there is an...