This HTML5 document contains 26 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

Prefix	IRI
dcterms	http://purl.org/dc/terms/
dbo	http://dbpedia.org/ontology/
foaf	http://xmlns.com/foaf/0.1/
n13	https://global.dbpedia.org/id/
dbt	http://dbpedia.org/resource/Template:
rdfs	http://www.w3.org/2000/01/rdf-schema#
freebase	http://rdf.freebase.com/ns/
rdf	http://www.w3.org/1999/02/22-rdf-syntax-ns#
owl	http://www.w3.org/2002/07/owl#
wikipedia-en	http://en.wikipedia.org/wiki/
dbc	http://dbpedia.org/resource/Category:
dbp	http://dbpedia.org/property/
prov	http://www.w3.org/ns/prov#
xsdh	http://www.w3.org/2001/XMLSchema#
wikidata	http://www.wikidata.org/entity/
dbr	http://dbpedia.org/resource/

Statements

Subject Item

dbr:LowerUnits

rdfs:label

LowerUnits

rdfs:comment

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.

dcterms:subject

dbc:Automated_theorem_proving dbc:Proof_theory

dbo:wikiPageID

42158354

dbo:wikiPageRevisionID

984658968

dbo:wikiPageWikiLink

dbc:Automated_theorem_proving dbr:Directed_acyclic_graph dbr:Clause_(logic) dbr:Redundant_proof dbr:Proof_compression dbr:Unit_clause dbc:Proof_theory dbr:Propositional_logic

owl:sameAs

freebase:m.0_yd_d0 wikidata:Q15964440 n13:agjg

dbp:wikiPageUsesTemplate

dbt:Reflist dbt:Algorithm-begin dbt:Algorithm-end dbt:Technical dbt:One_source

dbo:abstract

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. The algorithm targets exactly the class of global redundancy stemming from multiple resolutions with unit clauses. The algorithm takes its name from the fact that, when this rewriting is done and the resulting proof is displayed as a DAG (directed acyclic graph), the unit node appears lower (i.e., closer to the root) than it used to appear in the original proof. A naive implementation exploiting theorem would require the proof to be traversed and fixed after each unit node is lowered. It is possible, however, to do better by first collecting and removing all the unit nodes in a single traversal, and afterwards fixing the whole proof in a single second traversal. Finally, the collected and fixed unit nodes have to be reinserted at the bottom of the proof. Care must be taken with cases when a unit node occurs above in the subproof that derives another unit node . In such cases, depends on . Let be the single literal of the unit clause of . Then any occurrence of in the subproof above will not be cancelled by resolution inferences with anymore. Consequently, will be propagated downwards when the proof is fixed and will appear in the clause of . Difficulties with such dependencies can be easily avoided if we reinsert the upper unit node after reinserting the unit node (i.e. after reinsertion, must appear below , to cancel the extra literal from ’s clause). This can be ensured by collecting the unit nodes in a queue during a bottom-up traversal of the proof and reinserting them in the order they were queued. The algorithm for fixing a proof containing many roots performs a top-down traversal of the proof, recomputing the resolvents and replacing broken nodes (e.g. nodes having deletedNodeMarker as one of their parents) by their surviving parents (e.g. the other parent, in case one parent was deletedNodeMarker). When unit nodes are collected and removed from a proof of a clause and the proof is fixed, the clause in the root node of the new proof is not equal to anymore, but contains (some of) the duals of the literals of the unit clauses that have been removed from the proof. The reinsertion of unit nodes at the bottom of the proof resolves with the clauses of (some of) the collected unit nodes, in order to obtain a proof of again.

prov:wasDerivedFrom

wikipedia-en:LowerUnits?oldid=984658968&ns=0

dbo:wikiPageLength

5639

foaf:isPrimaryTopicOf

wikipedia-en:LowerUnits