HOL Parsing Error

[joe-hauns]

Master fails to parse the folloing HOL problem:

> vampire --input_syntax tptp TPTP-v8.2.0/Problems/SYO/SYO355^5.p

User error: Non-boolean term X0 of sort $i is used in a formula context (detected at or around line 33)

The problem itself looks right to me. I didn't find the same error in other problems and we're not supporting HOL on master atm anyways, so I this is not urgent but I wanted to park the issue here still.

[Rockjack00]

I encountered a similar issue parsing a file with formula of the form:
thf(name, axiom, myfunction(x) = y).
where myfunction has signature type_of_x * type_of_y which are each sub-types of $tType.

However, rewriting the formula as an application fixes the problem:
thf(name, axiom, (myfunction @ x) = y). pv pv

Some snooping around uncovered this comment at /Parse/TPTP.cpp:1776:

//At the moment, APP and LAMBDA are the only connectives that can take terms of type
// Other than $o as arguments

Attempting to solve this problem by changing the formula from thf to tff causes the same error message, but it seems to be an unrelated issue.
Once the parser sees a THF formula, _isThf is set causing any formula thereafter to be marked as an HOF_FORMULA and parsed accordingly (/Parse/TPTP.cpp:145).
These calls to TPTP::holFormula then eventually get to the same thread of execution as above.

Similarly using the $distinct predicate within a thf formula fails to be parsed because it is treated as an HOL_TERM rather than a FORMULA. It never reaches the normal treatment within TPTP::createPredicateApplication. This problem could be different enough that it merits its own issue though.

[joe-hauns]

Thanks for looking into that! Is this issue limiting your use of vampire right now, or was the mitigation of using applicative encoding a good-enough work around? depending on that i will decide whether i'll put in the time to fix the issue :)

[Rockjack00]

Given the other parsing issues, for now I have decided to try modelling my problem using TFF instead of THF, but I haven't yet determined which is going to be more suitable in the long run.