Jump to content

LowerUnivalents

From Wikipedia, the free encyclopedia

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

[edit]
  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.