Résumé
We propose a simple but powerful framework for reasoning about properties of models specified in languages like AMPL, OPL, Zinc or Essence. Using this framework, we prove that reasoning problems like detecting symme- tries, redundant constraints or dualities between models are undecidable even for a very limited modelling language that only generates simple problem in- stances. To provide tools to help the human modeller (for example, to identify when a model has a particular symmetry), it would nevertheless be useful to au- tomate many of these reasoning tasks. To explore the possibility of doing this, we describe two case-studies. The first uses the ACL2 inductive prover to prove inductively that a model contains a symmetry. The second identifies a tractable fragment of MiniZinc and uses a decision procedure to prove that a model implies a parameterized constraint.