search

spechub / Hets

The Heterogeneous Tool Set
http://hets.eu
GNU General Public License v2.0
57 stars 19 forks source link

CASL sublogic analysis for Prenex #1646

Open tillmo opened 8 years ago

mcodescu commented 8 years ago

see https://github.com/spechub/Hets/commit/08bdca75e65339de3790cf1842bef59895dd05ef and https://github.com/spechub/Hets/commit/d0550563cb7222c9b835a8fc5035b20f93b67fda

mcodescu commented 8 years ago

The spec

spec sp =
  sort s
  preds p,r,q:s
  forall x:s . p(x) /\ q(x) => r(x)
end

is now classified as Prenex, but it should be Horn.