LowerUnivalents

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.<ref>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.</ref>

==References== {{reflist}} {{logic-stub}}

[[Category:Mathematical logic]]