search

spechub / Hets

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

SPASS problem with reverse of lists #9

Open sternk opened 10 years ago

sternk commented 10 years ago

Reported by till and assigned to till Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/9

SPASS cannot prove a simple fact about reverse of lists (ask Lutz for details).

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/9#comment:2

I've tried spechub/Hets:VSE/test/List_Rev.casl using more fine grained selection CASL2SoftFOLInduction.

    . reverse(app(l2, l1)) = app(reverse(l1), reverse(l2))

cannot be proven. However if this formula is added as axiom then the following goals

    . reverse(cons(e, empty)) = cons(e, empty)
    . reverse(reverse(l)) = l

can be proven, but ga_assoc_app will not be proven.

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/9#comment:3

then %implies
forall l:list[elem]; e:elem
    . reverse(app(l, cons(e, empty))) = cons(e, reverse(l))
    . reverse(reverse(l)) = l

This goes through with a bigger time limit (120)