spechub / Hets

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

theory of a Common Logic module #1274

Open mcodescu opened 10 years ago

mcodescu commented 10 years ago

When I click Show theory on the node a Common logic text with cl-imports, I get e.g.

(cl-imports http://colore.oor.net/orderings/partial_ordering.clif)

in the displayed theory. I would normally expect here to get a flat theory and not a structured one.

cmaeder commented 10 years ago

the theory for orderings/partial_ordering.clif itself is flat as it also contains the imported orderings/quasiorder.clif. However, the sentences itself look odd as only the formulas should be sentences (and not the cl-imports and cl-text).

. (cl-text http://colore.oor.net/orderings/partial_ordering.clif (cl-imports http://colore.oor.net/orderings/quasiorder.clif)
                                                                 (forall (x
                                                                          y) (if (and (leq x
                                                                                           y)
                                                                                      (leq y
                                                                                           x)) (= x y))))
         %(http://colore.oor.net/orderings/partial_ordering.clif)%

. (cl-text http://colore.oor.net/orderings/quasiorder.clif (forall (x) (leq x
                                                                            x))
                                                           (forall (x
                                                                    y
                                                                    z) (if (and (leq x
                                                                                     y)
                                                                                (leq y
                                                                                     z)) (leq x
                                                                                              z))))
               %(http://colore.oor.net/orderings/quasiorder.clif)%

Another problem is that downloading from http://colore.oor.net/ does not work. Despite a catalog mapping hets still tries to download from http://colore.oor.net/.