Make injections be identities in SuleCFOL2SoftFOL

spechub / Hets

The Heterogeneous Tool Set

http://hets.eu

GNU General Public License v2.0

57 stars 19 forks source link

Make injections be identities in SuleCFOL2SoftFOL #645

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/645

According to the paper Klaus Lüttich and Till Mossakowski. Reasoning Support for CASL with Automated Theorem Proving Systems. WADT 2006, Springer LNCS, injections have to be axiomatised with inj(x)=x. Perhaps they can even be completely omitted (depending on their use in the translation of sort generation constraints).

sternk commented 10 years ago

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

this ticket seems to relate to spechub/Hets@9cfab8b7773f2541676d22b40bafb1ae800c46a0.