[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] What kind of decision procedure is used for integerlinear inequalities
I'm preparing a performance comparison of decision procedures for
integer linear inequalities in modern proof assistants (Coq, HOL,
Isabelle, PVS, ...).
So I have a couple of questions about how it's done in PVS:
1.What algorithm is used (Sup-Inf, Fourier-Motzkin variable elimination,
Omega Test or something else)?
2.Is it a decision procedure or it actually generates proofs?
3.Which combination of tactics should I use for maximum speed?
for example, for
test1: conjecture forall (v1:int),(v2:int),(v3:int),(v4:int):
(v1 > v2 and v3 > v4 => v1+v3 > v2+v4)
I use (then (skosimp) (ground)) but may be it's not optimal...
4.I'm planning to use randomly generated tests of different kinds.
May be there are existing benchmark sets that you might suggest to use?
Yegor Bryukhov, PhD student at GC CUNY
office phone: +1(212)817-8653
cell phone: +1(917)650-2035
e-mail: firstname.lastname@example.org email@example.com