Make logic projections work

[tillmo]

E.g. the following should go through (example from ESSLLI course):

logic OWL
ontology Genealogy =
  ObjectProperty: parentOf SubPropertyOf: ancestor
  ObjectProperty: ancestor
  ObjectProperty: ancestor Characteristics: Transitive
end

ontology Inbred_OWL =
  Genealogy 
and 
logic CASL :  {
  sort Thing
  preds Inbred : Thing
        parentOf, ancestor : Thing*Thing
  forall u:Thing 
  . Inbred(u) <=> exists x,y,z:Thing . 
       parentOf(x,u)
    /\ parentOf(y,u)
    /\ not x=y
    /\ ancestor(z,x)
    /\ ancestor(z,y) } hide along CASL2OWL2
end

[mcodescu]

This is a bit more complicated, if CASL2OWL2 is supposed to be an institution morphism. In order to be able to compute the theory of the node with hiding, we would need to be able to compute colimits of heterogeneous diagrams with both institution morphisms and comorphisms on the edges. Or we need to code institution morphisms as spans, cf. #68

[tillmo]

In the first place, it would be nice to just make the static analysis work. Computing the theory is a different issue. Note that for DG nodes involving homogeneous hiding, you cannot compute the theory either (unless you compute a normal form, but this is a second step here).

[mcodescu]

While trying to do this, I realized that I must label the hiding definition link with a GMorphism, which requires a comorphism. We only have an institution morphism here. Should I refactor this type such that institution morphisms are allowed too as labels of links in a development graph, or should I try to solve #68? Either way, it might be non-trivial work.

[mcodescu]

But, do I get it right that we are hiding along an institution morphism here? Because CASL2OWL is a comorphism in the logic graph of Hets.

[tillmo]

Interesting, I did not know CASL2OWL. See #1682.

Concerning institution morphisms, I suggest that we concentrate on those that are adjoint to a comorphism in the sense of section4 of http://www.informatik.uni-bremen.de/~till/papers/disthet.pdf Then, the GMorphism of the hiding link would be filled with the adjoint comorphism and the signature morphism obtained by the unit of the adjunction.