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

[PVS-Help] Simplify boolean formulas



Hi,

I am a member of the Relational Formal Methods Research Group of the Universidad de Buenos Aires, headed by Marcelo Frias.

Currently 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.

For example:
 * 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
bcardiff(?)gmail.com
.