Proving with (co)free links does not work correctly

[sternk]

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

Free.het

---

In spechub/Hets:Proofs/InferBasic.hs, the information about the free and cofree definition links is not assembled correctly. Strangely, spechub/Hets@5cf0f23d6436a66629796c8d5b67698571dde55e seems to cause this problem. Moreover, the theory in the target of the (co)free link needs to be assembled, but also this does not work correctly. The attached file can be used as a test file (with prover truthtables).

[sternk]

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

---

The theory displayed at the target of the blue link (with "Show Theory") is:

prop harry, john, mary
. (harry=>john) %(Ax_0)%
. (john=>not(harry)) %(Ax_1)%

Whereas much less is displayed without the change in spechub/Hets:Proofs/TheoremHideShift.hs in computeTheory. Maybe "Proofs-Automatic" or Proofs.Global also need to consider (co)free definition links?

[sternk]

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

---

OK, I have found and fixed the problem. But another problem is that with the attached file, I get two free links, differing in the following way:

13,18c13
<  propMap = fromList [(harry,
< harry),
< (john,
< john),
< (mary,
< mary)]},
---
>  propMap = fromList []},

[sternk]

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

---

These are two different representations of the identity morphism. In CASL a I avoid the longer version

[sternk]

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

---

Can this ticket be closed? I get only one free link. Darwin disproves the target, truthtables proves it.

[sternk]

Comment by till Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/618#comment:5

---

Replying to maeder:

Can this ticket be closed? I get only one free link. Darwin disproves the target, truthtables proves it.

This behaviour is of course unsatisfactory. The function hidingWarning in spechub/Hets:EdgeUtils.hs should be (adapted and) also called in the case of incoming free definition links.