#
64e89c4f |
|
11-Apr-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Self test was failing.
|
#
01ae37c5 |
|
11-Apr-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Remove some Unicode from sources.
|
#
7cc051a3 |
|
08-Nov-2011 |
Ramana Kumar <ramana.kumar@gmail.com> |
improve definition of QbfConv.remove_forall now use CHANGED_CONV. also some readability tweaks.
|
#
11a4bfb3 |
|
07-Nov-2011 |
Ramana Kumar <ramana.kumar@gmail.com> |
Improve HolQbfLib.decide_any (Progress on #1) It should now deal with free variables in the input term. Also, fixed a bug for dealing with a sequence of multiple innermost universal quantifiers, and in so doing redesigned qbf_prenex_conv substantially. Also, added another self test and made the self test check for decide_any check whether an appropriate theorem was produced (rather than assuming any theorem returned is ok).
|
#
bf6d5fce |
|
04-Nov-2011 |
Ramana Kumar <ramana.kumar@gmail.com> |
Progress on HolQbfLib.decide_any It should now accept any closed QBF (variables, conjunctions, disjunctions, implications, quantifiers) as long as all quantified variables occur somewhere (or maybe even some examples where they don't). Improvements to functions in QbfConv welcome.
|