Unsolved but not ranked goals

[mohit jangid]

Hi All,

While exploring the Interactive GUI for the standard FirstExample model, I found that there are unsolved goals in the bottom section that are not ranked in the top section.

Example 1:

      ---- 2 ranked goals

---- 3  unsolved Goals

Example 2 -- a little bit more deep into proof

----  2 ranked goals

----3  unsolved Goals

I am not sure if this is normal. My understanding is that every unsolved goal should be ranked for the next priority consideration. I am curious to know why some unsolved goals are not ranked.

With Tamarin 1.6.1 the command I used is:
tamarin-prover interactive FirstExample.spthy

--------------------------------------------------------------

Thank you

Mohit Kumar Jangid

[Jannik Dreier]

Hi Mohit,

This is actually done on purpose. Tamarin will only solve non-trivial KU
goals, as solving those would lead to non-termination, and is also not
necessary as open trivial goals can always be instantiated to extract a
solution. This is why trivial KU goals are not ranked in the top
section. However, Tamarin keeps them in the bottom list in case they
become instantiated with a non-trivial term later on, in which case they
need to be solved and will also show up on the top again. For more
details, see the extended version of the CSF'12 paper. (Constraint
reduction rule DG2_{2,e UP}, and Appendix C).

Cheers,
Jannik

On 29/12/2022 01:06, mohit jangid wrote:
> Hi All,
>
> While exploring the Interactive GUI for the standard FirstExample

> <https://tamarin-prover.github.io/manual/code/FirstExample.spthy> model,

> I found that there are unsolved goals in the bottom section that are not
> ranked in the top section.
>

> *Example 1:*
> *---- 2 ranked goals*
> first-ranked.png
>
> *---- 3  unsolved Goals*
> first-unsolved.png
>
> *Example 2 -- a little bit more deep into proof*
> *
> *
> *----  2 ranked goals
> *deep-ranked.png
>
> *----3  unsolved Goals*

>
> deep-unsolved.png
>
>
> I am not sure if this is normal. My understanding is that every unsolved
> goal should be ranked for the next priority consideration. I am curious
> to know why some unsolved goals are not ranked.
>
> With Tamarin 1.6.1 the command I used is:
> tamarin-prover interactive FirstExample.spthy
>
> --------------------------------------------------------------
> Thank you
> Mohit Kumar Jangid
>

> --
> You received this message because you are subscribed to the Google
> Groups "tamarin-prover" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to tamarin-prove...@googlegroups.com
> <mailto:tamarin-prove...@googlegroups.com>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/tamarin-prover/2574ac36-535d-4011-ac0a-8c0b50d589e5n%40googlegroups.com <https://groups.google.com/d/msgid/tamarin-prover/2574ac36-535d-4011-ac0a-8c0b50d589e5n%40googlegroups.com?utm_medium=email&utm_source=footer>.

--
Jannik Dreier
Maître de Conférences | Associate Professor
Université de Lorraine | TELECOM Nancy | LORIA
rese...@jannikdreier.net | +33 3 54 95 84 46

[mohit jangid]

Thank you, Dr. Jannik, for the explanation and the reference.