Crashing when free variable is synonymous to a bound one inside the same formula about vampire HOT 5 CLOSED

The bug was related to how the parser kept lists of sorts for bounded variables. The TPTP::sortOf function assumed that this list was non-empty but this was not the case where a variable was first quantified and then used freely. The fix is to add a check in TPTP::sortOf to see if the list of sorts is empty and if so treat the variable freely. A better fix would be to remove a sort list from the _variableSorts map when this list became empty, but Map.hpp does not support remove.

from vampire.

The formula is not well-sorted. Since the sort of X is not declared, it is
assumed to have the default sort $i. X = 1 should cause an syntax error
message. In general, TPTP forbids free variables, this syntax is
Vampire-only.

A

On 14 April 2015 at 14:03, Giles [email protected] wrote:

The bug was related to how the parser kept lists of sorts for bounded
variables. The TPTP::sortOf function assumed that this list was non-empty
but this was not the case where a variable was first quantified and then
used freely. The fix is to add a check in TPTP::sortOf to see if the list
of sorts is empty and if so treat the variable freely. A better fix would
be to remove a sort list from the _variableSorts map when this list
became empty, but Map.hpp does not support remove.

—
Reply to this email directly or view it on GitHub
#24 (comment).

from vampire.

The formula he gave was actually

fof(1, axiom, (![X]: (X = i)) | (X = i)).

so everything had type $i. But for

tff(ttype,type, (t : $tType)).
tff(1, axiom, (![X:t]: (X = i)) | (X = i)).

we have a syntax error as the uses of i have different types. Also for

fof(1, axiom, (![X]: (X = i)) | (X = 1)).

Vampire will treat 1 as being a constant of type $i as it is in an equality with a variable of type $i and fof formulas do not interpret integers as integers. For

tff(1, axiom, (![X]: (X = i)) | (X = 1)).

we get the syntax error you suggest. It is slightly odd that we can use integer symbols as constant symbols in fof.

This is what Vampire is currently doing rather than my suggestion for what it should do. The fact that free variables are not part of TPTP explains why this issue was not seen previously as one would expect it be very common in problems mixing quantified and free variables.

from vampire.

Giles is right. I remember now pointed out to Geoff, even more than once,
that this discrepancy between TFF and FOF is a nuisance and should be
abolished.

A

On 14 April 2015 at 15:15, Giles [email protected] wrote:

The formula he gave was actually

fof(1, axiom, (![X]: (X = i)) | (X = i)).

so everything had type $i. But for

tff(ttype,type, (t : $tType)).
tff(1, axiom, (![X:t]: (X = i)) | (X = i)).

we have a syntax error as the uses of i have different types. Also for

fof(1, axiom, (![X]: (X = i)) | (X = 1)).

Vampire will treat 1 as being a constant of type $i as it is in an
equality with a variable of type $i and fof formulas do not interpret
integers as integers. For

tff(1, axiom, (![X]: (X = i)) | (X = 1)).

we get the syntax error you suggest. It is slightly odd that we can use
integer symbols as constant symbols in fof.

This is what Vampire is currently doing rather than my suggestion for what
it should do. The fact that free variables are not part of TPTP explains
why this issue was not seen previously as one would expect it be very
common in problems mixing quantified and free variables.

—
Reply to this email directly or view it on GitHub
#24 (comment).

from vampire.

This was fixed a long time ago

from vampire.