- Abstract:
-
This report states and sketches the proofs for some important properties of IsaCoSy's constraint generation algorithm. We claim that for any rewrite rule, the constraint generation algorithm produces constraints that will prohibit the synthesis of exactly the terms containing a redex which can be rewritten by that rule (and no others).
- Links To Paper
- 1st Link
- Bibtex format
- @Misc{EDI-INF-RR-1378,
- author = {
Moa Johansson
and Lucas Dixon
and Alan Bundy
},
- title = {Properties of IsaCoSy's Constraint Generation Algorithm},
- year = 2010,
- url = {http://dream.inf.ed.ac.uk/projects/lemmadiscovery/publications/IsaCoSyProperties.pdf},
- }
|
