# LowerUnivalents

From HandWiki

Revision as of 09:46, 24 December 2020 by imported>JMinHep (add)

In proof compression, an area of mathematical logic, **LowerUnivalents** is an algorithm used for the compression of propositional resolution proofs. LowerUnivalents is a generalised algorithm of the LowerUnits, and it is able to lower not only units but also subproofs of non-unit clauses, provided that they satisfy some additional conditions.^{[1]}

## References

- ↑ Boudou, J., & Paleo, B. W. (2013). Compression of propositional resolution proofs by lowering subproofs. In Automated Reasoning with Analytic Tableaux and Related Methods (pp. 59-73). Springer Berlin Heidelberg.

Original source: https://en.wikipedia.org/wiki/LowerUnivalents.
Read more |