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

*To*: pvs-help@csl.sri.com*Subject*: subset of supported logic*From*: Zaher S Andraus <zandrawi@eecs.umich.edu>*Date*: Sat, 1 Nov 2003 18:11:13 -0500 (EST)*cc*: "Zaher Andraus @ EECS/U-M" <zandrawi@eecs.umich.edu>*Sender*: pvs-help-owner@csl.sri.com

Hi, 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 subset*. 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 multiplication". In Machine Intelligence, volume 7, pages 91--99, New York, 1972. American Elsevier) 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". Thanks -x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x Zaher S Andraus ACAL/EECS University of Michigan - Ann Arbor http://www.eecs.umich.edu/~zandrawi/ -x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x-x

- Prev by Date:
**Recursive Type Definition** - Next by Date:
**RE: PVS Specification for binary_tree datatype** - Prev by thread:
**RE: PVS Specification for binary_tree datatype** - Next by thread:
**Recursive Type Definition** - Index(es):