normalForms.CNF_CONV broken

[hol-theorem-prover]

normalForms.CNF_CONV broken

[mn200]

That depends on whether or not you think it should also be skolemizing.

[xrchz]

Is there a conv that just converts to cnf without touching the quantifiers? For preprocessing before calling HolQbfLib.decide, for example.

[mn200]

There's Canon_Port.PROP_CNF_CONV. But this one exposes you to a potential exponential blowup. I think you should use defCNF.DEF_CNF_VECTOR_CONV. Unfortunately, defCNF is only in examples/HolCheck at the moment, but I will change this. Using definitional CNF has to introduce quantifiers, but you can avoid messing with existing ones simply by applying the conversion under the quantifiers that are there (STRIP_QUANT_CONV).

There are also CNF conversions in Canon, and metis/normalForms. The latter may also skolemize.

[mn200]

Err, clearly normalForms.CNF_CONV does skolemize, becase that's the one you're complaining about.

[xrchz]

Has defCNF been moved to a better place?

[mn200]

Unfortunately, the vector version necessarily depends on the numbers so I couldn't figure out just where the "better place" should be.

[xrchz]

I think my original intention with this issue was to get the first item on the HolQbfLib Wishlist (in the Description manual), namely supporting arbitrary QBF via an appropriate conversion behind the scenes. The conversion should go to "prenex form", which is a quantifier prefix that ends in an existential quantifier followed by a quantifier-free CNF proposition. Whether that conversion is made from existing code or not I don't mind... If we can come up with a good plan of action, given what code exists (in any HOL-like theorem prover) and algorithms are known, in this issue I'd be happy to follow it through...

[mn200]

It strikes me that you don't want the vectorised CNF conversion for HOLQBF because you won't want to deal with quantifiers over functions from the naturals. So, defCNF's position is irrelevant to your project.

[xrchz]

A lot of good stuff appears to be in Canon, namely PRENEX_CONV, NNF_CONV, and PROP_CNF_CONV.

One thing missing is a conversion to remove innermost universal quantifiers. Do you know if such a conversion has been implemented? The idea: starting from a formula in prenex normal form with a matrix in CNF, if the innermost quantifier is universal, delete that quantifier and delete that variable wherever it appears. The justification: imagine taking two copies of the matrix, one for when the variable is true and one for when it is false. In the true case, the variable makes each clause where it appears true, so the clause can be deleted. In the false case, the variable can be deleted from each clause where it appears. If the variable doesn't appear in some clause, only one copy of the clause needs to be kept.

I don't have an LCF style algorithm to hand...

[mn200]

LCF algorithm suggestion:

1. move the quantifier in over each conjunct using FORALL_AND_THM
2. using EVERY_CONJ_CONV reorder each clause so that the bound variable comes first (|- (... ∨ x ∨ ..) = (x ∨ ...)) (you can probably do this with markerLib.move_disj_left)
3. apply rewrite |- (∀x. (x ∨ P)) = P to each conjunct (or the version with ¬x)

I’m assuming that variables only appear once in each clause.

[mn200]

Not clear that this requires any further work.

[xrchz]

Well, HolQbfLib.decide_any doesn't quite accept anything yet, but maybe we can wait for someone else who cares to open an issue about that...

[mn200]

On 24/05/12 3:42 PM, Ramana Kumar wrote:

Well, HolQbfLib.decide_any doesn't quite accept anything yet, but
maybe we can wait for someone else who cares to open an issue about
that...

Indeed. It seems to me that that is a separate issue from CNF_CONV not
working properly...