Natural numbers in the TPTP

[Geoff Sutcliffe]

Hi TPTPers, especially those who use arithmetic,

In many of the examples I see these days, natural numbers (starting at 0, per the ISO standard) are used rather than integers. As such I am considering adding naturals as a fourth number type in the TPTP - $nat. That would also mean adding $is_nat and $to_nat. Does anyone have an opinion on this?

While I'm at is, is there a need for $pow?

Cheers,

Geoff

[Michael Rawson]

Hi Geoff,

Naturally I don't speak for them, but I think this might be welcomed by
some in the Vampire camp. We have some branches that support an SMTLIB
extension for natural numbers, mostly used for the Rapid software
verification tool. Internally I think it gets translated to the obvious
datatype with some heuristics.

Michael

> --
> You received this message because you are subscribed to the Google
> Groups "TPTP World" group.
> To unsubscribe from this group and stop receiving emails from it,
> send an email to tptp-world+...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/tptp-world/e3c0ee48-0755-4f26-bf84-c6242ade6a87n%40googlegroups.com
> .

[Martin Suda]

Hi Geoff,

My opinion is that for the modeling purposes, using just $int and adding "X >= 0" here and there solves the problem. In other words, I don't think it's worth extending the language (and all the provers) just for this. 

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?

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 ... 😬)

Cheers,

Martin

[Geoff Sutcliffe]

Hi Martin,

> 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!

Cheers,

Geoff