search

jonnybest / Alloy2RelSMT

This is Alloy2RelSMT, a converter. It translates Alloy models into SMT files with a specific relational theory.
1 stars 0 forks source link

prove lemmas #22

Open jonnybest opened 12 years ago

jonnybest commented 12 years ago

Course of action:

  1. Create blank new model
  2. add axioms
  3. negate lemmas and add to model
  4. Check-sat
jonnybest commented 12 years ago

Proof of TCL lemma 1 https://github.com/jonnybest/thesisalloy2smt/blob/master/smtexamples/transcloslemmaproof1.smt2 Proof of TCL lemma 2 https://github.com/jonnybest/thesisalloy2smt/blob/master/smtexamples/transcloslemmaproof2.smt2