[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
subset of supported logic
I am a brand new user of Theorem Provers in general.
My first problem when considering which prover to choose
is that my problem subset is limited, so I am trying to
reason about the cabability of the prover *for this limited
I started by using ACL2, however the authors cannot guarantee
counter-example generation in all cases. And I am considering
to switch to PVS.
My problem is *satisfiability* proof with the presence of:
multiplication, addition and subtraction, bit- and part-selection,
uninterpreted functions, unsigned terms (vars) and constants, and
boolean logic. Like most satisfiability instances, it is
quantifiers free (only implicit EXISTS for all variables).
Including multiplication makes the above logic undecidable.
The question is, can we reason formally about the termination
of PVS with the *absence* of multiplication?
(e.g. see D. C. Cooper. "Theorem proving in arithmetic without
Machine Intelligence, volume 7, pages 91--99, New York, 1972. American
Does PVS terminate always, and if so, is the counter exmaple generation
guaranteed (i.e. might PVS stop and say "I can't prove (totally), or "I
can't prove without user interference" ??).
If the answer to these questions is "yes, PVS can screw your
life", then is there a special mode of PVS that switches to bit-level?
Meaning, since satisfiability in boolean logic is decidable,
does PVS attempt (in case it failed to prove) to "synthesize"
the arithmetic operations, turn the problem into satisfiability
in boolean logic, and send the problem to a sat solver or BDD?
The motivation behind these questions is that I am trying to
integrate PVS in a formal *automated* tool, something like
MS SLAM, and I want to see if a subset of the hardware units
I am trying to prove properties for can be guaranteed not
to get PVS stuck, and consequently get my whole flow stuck,
or "open ended".
Zaher S Andraus ACAL/EECS
University of Michigan - Ann Arbor