[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?


Best regards,
Yegor Bryukhov, PhD student at GC CUNY
office:       4330
office phone: +1(212)817-8653
cell phone:   +1(917)650-2035
e-mail:       ybryukhov@gc.cuny.edu ynb@mail.ru
home-page:    http://www.cs.gc.cuny.edu/~yegor/