# LowerUnivalents

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/LowerUnivalents
> Markdown URL: https://mediated.wiki/source/LowerUnivalents.md
> Source: https://en.wikipedia.org/wiki/LowerUnivalents
> Source revision: 712811692
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

In [proof compression](/source/Proof_compression), an area of [mathematical logic](/source/Mathematical_logic), **LowerUnivalents** is an [algorithm](/source/Algorithm) used for the compression of [propositional resolution](https://en.wikipedia.org/w/index.php?title=Propositional_resolution&action=edit&redlink=1) proofs. LowerUnivalents is a generalised algorithm of the [LowerUnits](/source/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

1. **[^](#cite_ref-1)** 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.

This logic-related article is a stub. You can help Wikipedia by adding missing information.

- [v](https://en.wikipedia.org/wiki/Template:Logic-stub)
- [t](/source/Template_talk%3ALogic-stub)
- [e](https://en.wikipedia.org/wiki/Special:EditPage/Template:Logic-stub)

---
Adapted from the Wikipedia article [LowerUnivalents](https://en.wikipedia.org/wiki/LowerUnivalents) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/LowerUnivalents?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.