Fixed: missing assignment in Formula::Cnf::C::Substitute().
Since this bug is fixed, the fol_incompleteness test fails. The test asserts that (x. P(x)) v (Ex. ~P(x)) cannot be proven. But since in both branches there is just one variable, it just tries one standard name. Probably that should be more. Needs to be investigated.
Loading
Please register or sign in to comment