Decision problems in ordered rewriting

Hubert Comon (1) , Paliath Narendran , Robert Nieuwenhuis , Michaël Rusinowitch

1 PROTHEO - Constraints, automatic deduction and software properties proofs

Nous montrons que la confluence de la réécriture ordonnée est décidable lorsque les regles sont orientées par un ordre lpo. La confluence des systemes contraints est indécidable ainsi que la réductibilité close

Mots clés: Automated deduction; Réécriture ordonnée; Ordered rewriting; Confluence; Preuve automatique

Domaines: Autre [cs.OH]

Hubert Comon, Paliath Narendran, Robert Nieuwenhuis, Michaël Rusinowitch. Decision problems in ordered rewriting. Proceedings 13th IEEE Symposium on Logic in Computer Science, 1998, none, 11 p. ⟨inria-00098606⟩