@InProceedings{10.1007/3-540-61780-9_64,
author="Cornes, Cristina
and Terrasse, Delphine",
editor="Berardi, Stefano
and Coppo, Mario",
title="Automating inversion of inductive predicates in {Coq}",
booktitle="Types for Proofs and Programs",
year="1996",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="85--104",
abstract="An inductive definition of a set is often informally presented by giving some rules that explain how to build the elements of the set. The closure property states that any object is in the set if and only if it has been generated according to the formation rules. This is enough to justify case analysis reasoning: we can read the formation rules backwards to derive the necessary conditions for a given instance to hold. The problem of inversion consists in finding out these conditions.",
isbn="978-3-540-70722-6"
}

