OKlibrary  0.2.1.6
LeanKernel.hpp File Reference

Plans regarding computations of lean kernels. More...

Go to the source code of this file.


Detailed Description

Plans regarding computations of lean kernels.

Todo:
Lean kernel via variable-elimination
  • Implement the computation of the lean kernel via a SAT-solver, which in the unsat-case returns a set of variables used by some resolution refutation.
Todo:
Lean kernel via oracle for leanness-decision
  • See [Kullmann 2003 (DAM)], Lemma 8.6.
  • In [Kullmann, CSR 12-2007], Lemma 3.1 this is generalised to non-boolean clause-sets.

Definition in file LeanKernel.hpp.