search

abau / co4

COmplexity COncerned COnstraint COmpiler
GNU General Public License v3.0
2 stars 3 forks source link

semantic labelling: compute usable rules #77

Closed jwaldmann closed 10 years ago

jwaldmann commented 10 years ago

compute usable rules for the labelled system - and do it after each removal.

we should then get proofs like this: http://termcomp.uibk.ac.at/termcomp/competition/resultDetail.seam?resultId=480566&cid=68

The plan is to change the type of second arg to constraint from

(Model MarkedSymbol, [ TerminationOrder MSL])

to

(Model MarkedSymbol, [ (Usable MSL, TerminationOrder MSL) ]
where  type Usable key = Map key Bool
jwaldmann commented 10 years ago

I have a commit in my branch: https://github.com/jwaldmann/co4/commit/5ba7181ddad0a5b880e529f3ab30e61d1d216fe6

before merging, should do some more tests (or, implement CPF output, to remove any doubts)