Typo in formalisation

[mereolog]

There is a "typo" in

ufo-formalization/src/axioms/17_characterization.p

Line 6 in 73250f5

& momentType(M)

and

ufo-formalization/ufo_2021.tex

Line 1139 in 2da0df3

& momentType(M)

Instead of 'momentType(M)' you should have 'momentType(MT)'.

Currently, the formalization is not TPTP-compliant.

There is a similar problem in:

ufo-formalization/src/axioms-clif/17_characterization.p.clif

Line 5 in 73250f5

(and (endurantType et) (momentType m) (forall (e w)

[claudenirmf]

Dear Pawel, thanks for reporting this issue! All the occurrences are actually the same issue since we declare our axioms only once and then generate declarations in other syntaxes, such as CLIFF and TeX.

Also, we are moving the formalization from the single file we inittially used (ufo_2021.tex) to split files (available in the folder src).

Could you please clarify how our formalization is not TPTP-compliant? We have been using on both System on TPTP and Hets with no complaints from these tools.

[mereolog]

Try to run this through https://www.tptp.org/cgi-bin/SystemOnTPTP:

fof(ax_endurantTypeCharacterizationByMomentTypes_a83, axiom, (
  ![ET,MT]: (characterizes(MT,ET) => (
    endurantType(ET)
    & momentType(M)
    & (![E,W]: (iof(E,ET,W) => (?[M]: (iof(M,MT,W) & inheresIn(M,E)))))
    & (![M2,W2]: (iof(M2,MT,W2) => (?[E2]: (iof(E2,ET,W2) & inheresIn(M2,E2)))))
  ))
)).

I think you should get this error:

% SZS end RequiredInformation
% Checking upload ... % Checker ran ... 
% That upload is not clean TPTP format ...
% ERROR: Line 4 Char 19 Token ")" continuing with "" : Unquantified variable M 
ERROR: Formatter did not create all the Paradox---4.0 format files
ERROR: Line 4 Char 19 Token ")" continuing with "" : Unquantified variable M

I believe that your intention was to quantify over MT not M in clause '& momentType(M)'.

[claudenirmf]

Now I understand what you meant, the source of the problem is the same then. Thank you for the deatiled response.

Yes, the correct statement is with the quantification of MT rather than M. I'll fix this at the earlist opportunity.