LowerUnits
In proof compression LowerUnits (LU) is an algorithm used to compress propositional logic resolution proofs. The main idea of LowerUnits is to exploit the following fact: Theorem: Let be a potentially redundant proof, and be the redundant proof | redundant node. If ’s clause is a unit clause, then is redundant.
Link from a Wikipage to another Wikipage
primaryTopic
LowerUnits
In proof compression LowerUnits (LU) is an algorithm used to compress propositional logic resolution proofs. The main idea of LowerUnits is to exploit the following fact: Theorem: Let be a potentially redundant proof, and be the redundant proof | redundant node. If ’s clause is a unit clause, then is redundant.
has abstract
In proof compression LowerUnit ...... er to obtain a proof of again.
@en
Wikipage page ID
42,158,354
page length (characters) of wiki page
Wikipage revision ID
984,658,968
Link from a Wikipage to another Wikipage
wikiPageUsesTemplate
comment
In proof compression LowerUnit ...... nit clause, then is redundant.
@en
label
LowerUnits
@en