search

CLEARSY / pptranspog

Encoding of proof obligations generated by Atelier B to typed first-order formats (SMT, TPTP) using the ppTrans approach
GNU General Public License v3.0
0 stars 2 forks source link

PPTransTPTP : ambiguous associativity #3

Closed dde-cls closed 2 months ago

dde-cls commented 12 months ago 
ERROR: Line 1096 Char 344 Token "=>" continuing with " $greatereq(X_1209," : Binary with ambiguous associativity

afile-3-53.tptp.txt

dde-cls commented 12 months ago

P & Q => R & S is considered ambiguous in TPTP and TPTP4X raises errors.

dde-cls commented 12 months ago

An almost minimal file to reproduce the problem (tentative) error.pog.txt