Natural numbers in the TPTP

3 views
Skip to first unread message

Geoff Sutcliffe

unread,
Oct 28, 2022, 10:01:40 AM10/28/22
to TPTP World
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

unread,
Oct 31, 2022, 4:30:40 AM10/31/22
to tptp-...@googlegroups.com
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

unread,
Oct 31, 2022, 7:39:22 AM10/31/22
to tptp-...@googlegroups.com
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

unread,
Oct 31, 2022, 4:37:51 PM10/31/22
to TPTP World
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
Reply all
Reply to author
Forward
0 new messages