In
proof compression, an area of
mathematical logic
Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
, LowerUnivalents is an
algorithm
In mathematics and computer science, an algorithm () is a finite sequence of Rigour#Mathematics, mathematically rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algo ...
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.
[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.]
References
{{logic-stub
Mathematical logic