ZachJHansen
commented
4 months ago The agreed upon solution is to extend the current implementation of function constants (n$g, n$i, n$s) with placeholders. Placeholders, unlike function constants, are not a part of FOL, they are an extension based on io-programs. Syntactically, they are symbolic constants that should be replaced by general terms based on user-guide context. So they are parsed as symbolic constants and then subsequently replaced with function constants of the appropriate sort. Similar to the handling of io-programs.
Error: (input: n -> integer. lemma: q(n+1).) OG placeholders are of sort general, the -> integer is equivalent to adding the assumption exists N$ ( N$ = n)
New placeholders (function constants) are a different beast Not an error: (input: n$i., lemma: q(n$i+1).)
The proposed change is that input: n. lemma: q(n). means parse n as a symbolic constant, then replace it with n$g internally
whereas input: n -> integer. lemma: q(n). means parse n as a symbolic constant, then replace it with n$i internally
input: n -> integer, n$i. These represent different function constants (internally n$i should be named ni or n$i)
Hi Zach,
By making function constants explicitly sorted, parsing specs or lemmas can be accomplished independent of context (the provided user guide).
Let’s try to find a way to achieve your goal—parsing formulas independent of context—without the unfortunate side effect of introducing two different names for the same placeholder.
What if we treat every placeholder as a constant of the sort “general”? That will make p(n+1) syntactically incorrect even when n is a placeholder, but this is okay; we can write
exists N ( N = n and p(N+1) ).
This is the same trick that we use with general variables: since p(X+1) is not allowed, we write
exists N ( N = X and p(N+1) ).
The statement
input: n$i.
(or n -> integer, as in the old antem—whichever you like better) will have the same meaning as
input n. assumption: exists N (N = n).
As I understand, you can help vampire to speed up search by using the sort integer when you represent n in the TPTP language. But this is an implementation detail, not related to the meaning of the input statement.
What do you think?
Best, Vladimir