LowerUnivalents explained

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]

Notes and References

  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 article is licensed under the GNU Free Documentation License. It uses material from the Wikipedia article "LowerUnivalents".

Except where otherwise indicated, Everything.Explained.Today is © Copyright 2009-2024, A B Cryer, All Rights Reserved. Cookie policy.