[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] PVS to Yices translation



Hi,

I noticed that the (yices) strategy proves, e.g., the goal:

l1 :

  |-------
{1}   -1 > 0

Rule? (yices)
ydefns =

yforms =
 (assert (not (>  (-  1) 0)))

Result = unsat
Logical context is inconsistent. Use (reset) to reset.
unsat
Statistics:
num. decisions:                   0
num. conflicts:                   1
num. bool vars:                   0
memory used:                      6.10938 Mb
cpu time:                         0.014997 secs

Yices translation of negation is unsatisfiable
Simplifying with Yices,
Q.E.D.


It seems like the translation of "-1" to "(- 1)" is incorrect, as per
the Yices FAQ:

http://yices-wiki.csl.sri.com/index.php/FAQ#Why_is_.28-_10.29_equal_to_10_.3F

Is there a quick fix to this, even if just to refuse translations
involving unary minus so as not to have unsound proofs?

Thanks,
Johannes

-- 
Johannes W. E. Eriksson, M.Sc.
Ph.D. Student / Turku Centre For Computer Science (TUCS)
Åbo Akademi University / Department of Information Technologies
e-mail: joheriks@abo.fi  www: http://www.abo.fi/~joheriks