翻訳と辞書 Words near each other ・ Red and Black in Willisau ・ Red and Blue ・ Red and Blue (album) ・ Red and Blue Chair ・ Red and blue damsel ・ Red and Charline McCombs Field ・ Red and Rio Grande ・ Red and Rio Grande (song) ・ Red and Rover ・ Red and White ・ Red and White Army ・ Red and White Brand ・ Red and White Bundle ・ Red and white giant flying squirrel ・ Red Anderson ・ RecycleUnits ・ Recycling ・ Recycling (disambiguation) ・ Recycling and Waste Management Exhibition ・ Recycling antimatter ・ Recycling bin ・ Recycling by material ・ Recycling by product ・ Recycling codes ・ Recycling cooperative ・ Recycling in Brazil ・ Recycling in Canada ・ Recycling in Japan ・ Recycling in Northern Ireland ・ Recycling in the Netherlands Dictionary Lists mini英和辞書 mini和英辞書 Webster 1913 Latin-English FOLDOC Wikipedia English ウィキペディア

翻訳と辞書　辞書検索 [ 開発暫定版 ] スポンサード リンク RecycleUnits ： ウィキペディア英語版 RecycleUnits In mathematical logic, proof compression by RecycleUnits〔Bar-Ilan, O.; Fuhrmann, O.; Hoory, S. ; Shacham, O. ; Strichman, O. ''Linear-time Reductions of Resolution Proofs''. Hardware and Software: Verification and Testing, p. 114–128, Springer, 2011.〕 is a method for compressing propositional logic resolution proofs. Its main idea is to make use of intermediate (e.g. non input) proof results being unit clauses, i.e. clauses containing only one literal. Certain proof nodes can be replaced with the nodes representing these unit clauses. After this operation the obtained graph is transformed into a valid proof. The output proof is shorter than the original while being equivalent or stronger. ==Algorithms== The algorithms treat resolution proofs as directed acyclic graphs, where each node is labeled by a clause and each node has either one or two predecessors called parents. If a node has two parents it is also labeled with a propositional variable called the pivot, which was used to compute the nodes clause using resolution. The following algorithm describes the replacement of nodes. It is assumed that in the resolution proof for all non leaf nodes with two parent nodes, the left parent node contains the positive and the right parent node the negative pivot variable. The algorithm first iterates over all non leaf unit clauses and then over all non ancestor nodes of the proof. If the node's pivot element is the variable of the present unit clause's literal, one of the parent nodes can be replaced by the node corresponding to the unit clause. Because of the above assumption, if the literal is equal to the pivot, the left parent contains the literal and can be replaced by the unit clause node. If the literal is equal to the negation of the pivot the right parent is replaced. 1 function RecycleUnits(Proof $P$): 2 Let $U$ be the set of non leaf nodes representing unit clauses 3 for each $u\; \backslash in\; U$ do 4 Mark the ancestors of u 5 for each unmarked $n\; \backslash in\; P$ do 6 let $p$ be the pivot variable of $n$ 7 let $l$ be the literal contained in the clause of $u$ 8 if $p\; ==\; l$ then 9 replace the left parent of $n$ with $u$ 10 else if $\backslash neg\; p\; ==\; l$ then 11 replace the right parent of $n$ with $u$ In general after execution of this function the proof won't be a legal proof anymore. The following algorithm takes the root node of a proof and constructs a legal proof out of it. The computation begins with recursively calls to the children nodes. In order to minimize the algorithm calls, it is beingt kept track of which nodes were already visited. Note that a resolution proof can be seen as a general directed acyclic graph as opposed to a tree. After the recursive call the clause of the present node is updated. While doing so four different cases can occur. The present pivot variable can occur in both, the left, the right or in none of the parent nodes. If it occurs in both parent nodes the clause is calculated as resolvent of the parent clauses. If it is not present in one of the parent nodes the clause of this parent can be copied. If it misses in both parents one has to choose heuristically. 1 function ReconstructProof(Node $n$): 3 if $n$ is visited return 4 mark $n$ as visited 5 if $n$ has no parents return 6 else if $n$ has only one parent $x$ then 7 ReconstructProof($x$) 8 $n$.Clause = $x$.Clause 9 else 10 let $l$ be the left and $r$ the right parent node 11 let $p$ be the pivot variable used to compute $n$ 12 ReconstructProof($l$) 13 ReconstructProof($r$) 14 if $p\; \backslash in\; l.Clause$ and $p\; \backslash in\; r.Clause$ 15 $n$.Clause = Resolve($l$,$r$,$p$) 16 else if $p\; \backslash in\; l.Clause$ and $p\; \backslash notin\; r.Clause$ 17 $n$.Clause = $r$.Clause 18 delete reference to $l$ 19 else if $p\; \backslash in\; r.Clause$ and $p\; \backslash notin\; l.Clause$ 20 $n$.Clause = $l$.Clause 21 delete reference to $r$ 22 else 23 let $x\; \backslash in\; \backslash$ and $y\; \backslash in\; \backslash \; \backslash setminus\; \backslash$ //choose x heuristically 24 $n$.Clause = $x$.Clause 25 delete reference to $y$ 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「RecycleUnits」の詳細全文を読む スポンサード リンク 翻訳と辞書 : 翻訳のためのインターネットリソース Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.