> My opinion is that for the modeling purposes, using just $int and adding "X
> >= 0" here and there solves the problem.
In some cases it solves the problem, but in others you don't want to have
to define a function/predicate for negative numbers. As a case in point,
Nikolaj pointed out that "pow(2,-1) is not even an integer", and here it
would be nice to define $pow for the naturals. Another case that impacts
me right now is defining models with infinite domains. With integers it's
kinda messy, but with naturals it would be, well, kinda natural.
> In other words, I don't think it's
> worth extending the language (and all the provers) just for this.
I understand the pain it might cause, and I see Nikolaj's comments to
this point. I will reply with thoughts, to his post.
> One reason for talking about the naturals would be to motivate people to
> look at Peano arithmetic problems and induction (one of hot topics in the
> Vampire camp), but for that (as Michael mentions) using algebraic data
> types (and the "no junk, no confusion" semantics they bring with them)
> would seem to be more appropriate. But that's a big big chapter you
> probably decided a long time ago you didn't want to open for TPTP at least
> for now, right?
Alex Steen would also like (co)datatypes, and I do have a proposal lying
around that got developed at IJCAR in Oxford ... I havn't have time or
enough offers of help to bring it into the TPTP.
> Regarding $pow, that could be more interesting, if there is demand for it
> on the encoding/modeling side. (It will be some work to specify in the most
> general way, though. Maybe you only want to have $exp(_) for the reals...
> and $ln and $sin and $cos and $tan and ... 😬)
Sounds like a topic for a TPTP Tea Party!