TFF parsers were implemented as much as Skeptik's type system supports it.
Quantified typed couldn't be implemented producing that over 500 problems of theTPTP library fail to be parsed.
THF parsers present a similar problem, but quantified and other complex types constructions are less used. Hence, almost all the problems from the TPTP library can be successfully parsed. This represent around 3040 of the 3077 problems tested.
In both languages let expressions where not implemented but only 2 files in over
20000 present in the library make use of them.
A more abstract and general proof parser could be implemented.
ceilican
commented
8 years ago
TFF parsers were implemented as much as Skeptik's type system supports it. Quantified typed couldn't be implemented producing that over 500 problems of theTPTP library fail to be parsed.
THF parsers present a similar problem, but quantified and other complex types constructions are less used. Hence, almost all the problems from the TPTP library can be successfully parsed. This represent around 3040 of the 3077 problems tested.
In both languages let expressions where not implemented but only 2 files in over 20000 present in the library make use of them.
A more abstract and general proof parser could be implemented.