Axiom [eom-1] is ill-formed

[mereolog]

Axiom [eom-1] is ill-formed:

https://github.com/BFO-ontology/BFO-2020/blob/da7c40b6028d339f63bd0e9044d22a9b2b81ee6c/21838-2/common-logic/occurrent-mereology.cl#L172-L187

To see this try to run this axiom or the whole of occurrent-mereology.cl through http://rest.hets.eu.

I think that the correct form of its content should look like below:

(cl:comment "b temporal part c (both spatiotemporal regions) iff b temporal projection is part of c's temporal projection, and for all parts of b's existence, if it spatially-projects-onto s at that time, then so does c [eom-1]"
    (forall (b c)
     (if
      (and (exists (t) (instance-of b spatiotemporal-region t))
       (exists (t) (instance-of c spatiotemporal-region t)))
      (iff (temporal-part-of b c)
       (and (exists (tb tc)
        (and
            (temporally-projects-onto b tb)
            (temporally-projects-onto c tc)
            (occurrent-part-of tb tc)))
         (forall (tp)
          (if
           (and (occurrent-part-of tp tb)
            (exists (s) (spatially-projects-onto b s tp)))
           (exists (s)
            (and (spatially-projects-onto b s tp)
             (spatially-projects-onto c s tp))))))))))

[alanruttenberg]

When I run the whole of the file through HETS it seems to have trouble with the multi-line comment, in particular the @ sign. It's inside a stringquote. Try just (cl:comment 'foo@bar') as input and you also get an error. So that is a HETS bug it seems.

When you tried to use HETS did you explicitly tell it that the input is CLIF format? It parses fine for me if that's the case, but gives an error if under Input Type of File or Text Field [Try to determine automatically] is chosen.

temp20050:1.1:
unexpected '('
expecting "%", "library", "distributed-ontology", end of input, "specification", "spec", "ontology", "onto", "model", "OMS", "pattern", "view", "interpretation", "refinement", "import", "entailment", "query", "substitution", "result", "equivalence", "alignment", "module", "unit", "network", "arch", "from", "use", "logic", "serialization", "language", "newlogic", "newcomorphism", "local", "free", "cofree", "minimize", "closed-world", "maximize", "closed", "combine", "{", "<", ":", "/", digit, "?", "#", "esort", "sort", "op", "pred", "type", "etype", "generated", "var", "forall", "." or "axiom"

Or am I misunderstanding your report and you think the problem is with the axioms itself? As opposed to the syntax?

If you would, please just read the CLIF and see if you see an error and, if so, point out where the error is? It looks well formed to me - all the forms seem to have the right number of arguments.

[alanruttenberg]

I notice you aren't using the latest commit. You should always be using the latest because older commits may have errors that were subsequently fixed. Werner pointed out that there was an earlier error in eom-1. My check used the latest commit and that is what validated. The version you cite in your report does not. "No promises about anything but the latest commit"

[alanruttenberg]

Actually, I'm confused again. I don't see changes to the file after that commit. Am investigating.

[alanruttenberg]

Sigh. My bad. I did not check in the changes for that fix. I will update and then close. The version that validates is

(cl:comment "b temporal part c (both spatiotemporal regions) iff b temporal projection is part of c's temporal projection, and for all parts of b's existence, if it spatially-projects-onto s at that time, then so does c [eom-1]"
    (forall (b c)
     (if
      (and (exists (t) (instance-of b spatiotemporal-region t))
       (exists (t) (instance-of c spatiotemporal-region t)))
      (iff (temporal-part-of b c)
       (exists (?tb ?tc)
        (and (temporally-projects-onto b tb)
             (temporally-projects-onto c tc)
             (and (occurrent-part-of tb tc)
              (forall (tp)
               (if
                (and (occurrent-part-of tp tb)
                 (exists (s) (spatially-projects-onto b s tp)))
                (exists (s)
                 (and (spatially-projects-onto b s tp)
                  (spatially-projects-onto c s tp))))))))))))```

[alanruttenberg]

fixed now