翻訳と辞書 Words near each other ・ Lowerhouse Cricket Club ・ Lowerhouses ・ Loweria ・ Loweriella ・ Lowering Gasoline Prices to Fuel an America That Works Act of 2014 ・ Lowerkoti ・ Lowermoor Water Treatment Works ・ LowerMyBills.com ・ LOWERN ・ Lowernine.org ・ Lowertown ・ Lowertown Historic District ・ Lowertown Historic District (Lockport, New York) ・ Lowertown Historic District (Saint Paul, Minnesota) ・ Lowertown, Cornwall ・ LowerUnits ・ Lowery Glacier ・ Lowery Stokes Sims ・ Lowerybane ・ Lowes ・ Lowes Barn ・ Lowes Cato Dickinson ・ Lowes Dalbiac Luard ・ Lowes Foods ・ Lowes Island, Virginia ・ Lowes Loch (Ayrshire) ・ Lowes Menswear ・ Lowes Moore ・ Lowes, Kentucky ・ Lowesby Dictionary Lists mini英和辞書 mini和英辞書 Webster 1913 Latin-English FOLDOC Wikipedia English ウィキペディア

翻訳と辞書　辞書検索 [ 開発暫定版 ] スポンサード リンク LowerUnits ： ウィキペディア英語版 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:〔Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno. ''Compression of Propositional Resolution Proofs via Partial Regularization''. 23rd International Conference on Automated Deduction, 2011.〕 Theorem: Let $\backslash varphi$ be a potentially redundant proof, and $\backslash eta$ be the redundant proof | redundant node. If $\backslash eta$’s clause is a unit clause, then $\backslash varphi$ 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 $\backslash eta$ 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 $\backslash eta^$ occurs above in the subproof that derives another unit node $\backslash eta$. In such cases, $\backslash eta$ depends on $\backslash eta^$. Let $\backslash ell$ be the single literal of the unit clause of $\backslash eta^$. Then any occurrence of $\backslash overline$ in the subproof above $\backslash eta$ will not be cancelled by resolution inferences with $\backslash eta^$ anymore. Consequently, $\backslash overline$ will be propagated downwards when the proof is fixed and will appear in the clause of $\backslash eta$. Difficulties with such dependencies can be easily avoided if we reinsert the upper unit node $\backslash eta^$ after reinserting the unit node $\backslash eta$ (i.e. after reinsertion, $\backslash eta^$ must appear below $\backslash eta$, to cancel the extra literal $\backslash overline$ from $\backslash eta$’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 $\backslash kappa$ and the proof is fixed, the clause $\backslash kappa^$ in the root node of the new proof is not equal to $\backslash kappa$ 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 $\backslash kappa^$ with the clauses of (some of) the collected unit nodes, in order to obtain a proof of $\backslash kappa$ again. == Algorithm == General structure of the algorithm Input: A proof $\backslash psi$ Output: A proof $\backslash psi^$ with no global redundancy with unit redundant node (unitsQueue, $\backslash psi\_$) ← collectUnits($\backslash psi$); $\backslash psi\_$ ← fix($\backslash psi\_$); fixedUnitsQueue ← fix(unitsQueue); $\backslash psi^$ ← reinsertUnits($\backslash psi\_$, fixedUnitsQueue); return $\backslash psi^$; We collect the unit clauses as follow Input: A proof $\backslash psi$ Output: A pair containing a queue of all unit nodes (unitsQueue) that are used more than once in $\backslash psi$ and a broken proof $\backslash psi\_$ $\backslash psi\_$ ← $\backslash psi$; traverse $\backslash psi\_$ bottom-up and foreach node $\backslash eta$ in $\backslash psi\_$ do if $\backslash eta$ is unit and $\backslash eta$ has more than one child then add $\backslash eta$ to unitsQueue; remove $\backslash eta$ from $\backslash psi\_$; end end return (unitsQueue, $\backslash psi\_$); Then we reinsert the units Input: A proof $\backslash psi\_$ (with a single root) and a queue $q$ of root nodes Output: A proof $\backslash psi^$ $\backslash psi^$ ← $\backslash psi\_$; while $q\backslash neq\backslash emptyset$ do $\backslash eta$ ← first element of $q$; $q$ ← tail of $q$; if $\backslash eta$ is resolvable with root of $\backslash psi^$ then $\backslash psi^$ ← resolvent of $\backslash eta$ with the root of $\backslash psi^$; end end return $\backslash psi^$; 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「LowerUnits」の詳細全文を読む スポンサード リンク 翻訳と辞書 : 翻訳のためのインターネットリソース Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.