details "cyclic" and "from formulae" contradiction
48 views
Skip to first unread message
mohit jangid
unread,
Aug 26, 2021, 9:39:00 AM8/26/21
Reply to author
Sign in to reply to author
Forward
Sign in to forward
Delete
You do not have permission to delete messages in this group
Copy link
Report message
Show original message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to tamarin-prover
Hi All,
When proving a lemma step by step in the interactive GUI page, Tamarin lists the contradiction reason for branches as "cyclic" or "from formula". Is it possible to get the details about which cyclic dependency (of fact or the term) or which formula caused the contradiction on a given branch?
Thank you
Mohit Kumar Jangid
Jannik Dreier
unread,
Aug 30, 2021, 7:25:55 AM8/30/21
Reply to author
Sign in to reply to author
Forward
Sign in to forward
Delete
You do not have permission to delete messages in this group
Copy link
Report message
Show original message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to tamarin...@googlegroups.com
Hi,
Unfortunately Tamarin does not directly tell you which cycle or formula
caused the contradiction. But still you can get some information: in the
case of a cycle, you can inspect the graph to locate the cycle yourself.
In the case of a formula, you will find a formula "False" (or "bottom")
in the list of formulas, however this does not tell you which formula
turned false. To understand that, you can try to go one step back in
your proof (or more if necessary) and compare the formulas.
You do not have permission to delete messages in this group
Copy link
Report message
Show original message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to tamarin-prover
Thank you, Dr. Jannik, for the guidance. I am dealing with very large traces and navigating/finding the cycle, in the graph, seems difficult for now. For the formulae, I will try your tip!.