[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Simplify boolean formulas
I am a member of the Relational Formal Methods Research Group of the Universidad de Buenos Aires, headed by Marcelo Frias.
we are trying to simplify a formula (mainly boolean variables) using
PVS 4.0. The formulas are not theorems, but we expect that redundant
information is removed and some automated deduction be performed. Other
than booleans, there are some (not many) enum variables that are not
useful in the simplification process.
Despite some of the experiments are quite long, we were expecting better results.
* Theory size: 16 Kb, 140 booleans constants. 3 minutes were needed by grind to return a result.
* Theory size: 18 Kb, 170 booleans constants. We waited more than 40 minutes and cut the execution.
The main questions we have are:
* Are there any limitation we should know about using pvs for simplifying formulas with booleans variables?
* Is there any detailed information about how bddsimp is implemented that we could take advantage of?
If someone has any kind of feedback it would be great.
Brian J. Cardiff