resolutionとは？

辞典・百科事典の検索サービス - Weblio辞書

初めての方へ

参加元一覧


用語解説|動画|文献|商品|全文検索
Weblio 辞書 > 業界用語 > ビデオ用語 > resolutionの意味・解説 

三省堂 大辞林
三省堂三省堂

レゾリューション 3 [resolution]

⇒解像度(かいぞうど)

索引トップ用語の索引ランキング

ビデオ用語集
社団法人日本映像ソフト協会社団法人日本映像ソフト協会

レゾ 【resolution】

【参】レゾリューション 　

レゾリューション 【resolution】

解像度のこと。画像の良さを表す尺度の１つ。

【参】解像度

解像度 【resolution】

専用解像度チャートにより、テレビ画面の縦方向、横方向のくさび縞が何本まで分解描写出来るかという表示で、垂直解像度、水平解像度で表す。

定義上は、テレビ画面の縦方向に何本の横線が描写できるかが垂直解像度、縦方向と同じサイズのテレビ画面の横方向に何本の垂直線が描写出来るかが水平解像度であり、白黒で２本（2TV本）と数えるので注意が必要である。

【参】レゾリューション

索引トップ用語の索引ランキング

サラウンド用語辞典
サラウンドWebサラウンドWeb

解像度 (Resolution)

画質を表す尺度の一つ。テレビ方式では白と黒の縞模様が何本まで表現できるかを尺度としてきたが、デジタルテレビでは水平ドット数×有効走査線数が基本になる。コンピューター画面では水平方向と垂直方向に表示可能な画素数で表す。画面の縦方向の垂直解像度は走査線数に関係し、走査線数525本では355本程度、1125本の場合は750本程度である。画面の横方向の水平解像度はNTSC方式では映像信号の周波数帯域で決まり360本程度である。MPEG‐2で圧縮された場合は圧縮のやり方により一定しないが最高の解像度は画素数で決まる。

索引トップ用語の索引ランキング

画像技術用語集
日本画像学会日本画像学会

解像力

読み：かいぞうりょく
英語：resolving power, resolution

結像素子の光学性能を表す．2点または2線が分離して見える限界の幅の逆数をいう．1mmあたりに含まれる等間隔の白黒1組の縞本数で表現する（line paires/mm， 本/mm)．

解像度

読み：かいぞうど
英語：resolution

ファクシミリ，プリンタ，TVなどでどの程度細かく画像を表現できるかを表すもの．プリンターでは，単位長当りの描画ドット数で表し，慣用的に単位長としてインチを用い，dpi(dots/inch)と呼称する．レンズ，感光材料では解像力を用いる．

索引トップ用語の索引ランキング

IT用語辞典バイナリ
IT用語辞典バイナリIT用語辞典バイナリ

解像度

読み方：かいぞうど
別名：レゾリューション，画面解像度，表示解像度
【英】resolution

解像度とは、デジタル画像の細かさを表す度合いのことである。

解像度はデジタル画像を構成する個々の単位点（ドット、ピクセル）の細かさを数値化することによって表現される。個々の単位点が小さいほど、あるいはより多くの単位点によって構成されているほど、滑らかな文字や画像を表示することが可能である。細かくて精密な画像が表示できる様子を、一般的には「解像度が高い」などと形容する。

これに対して、ドットやピクセルが大きかったり総量が少なかったりすると、個々の点が点として独立に認識されてしまい、画像全体も粗く見える。

解像度を表す単位には、一般に「ドット」が用いられる。ディスプレイの場合は、多くの場合「1024×768ドット」のようにヨコ・タテに並んでいる数で表すされる（ディスプレイはおおむね4:3の比率で設計されている）。他方、プリンタやスキャナでは単位面積あたりに含まれる総数として表され、このとき、dpi（dots per inch）と呼ばれる単位が用いられる。ちなみに、写真印刷関係の業界ではドットに相当するものを「ピクセル」と呼んでおり、プリンタやスキャナ、デジカメといった機器について解像度を表現する場合には、「ピクセル」が用いられることが多い。

参照リンク
YOUART GROUP - 解像度と線数について
コンピュータのほかの用語一覧
表示装置：  液晶パネルの2012年問題  インテグラルイメージング方式  プロジェクター  解像度  マルチモニター  メディカルモニター  レゾリューション
>>表示装置カテゴリの他の用語

索引トップ用語の索引ランキング画像一覧カテゴリー

走査電子顕微鏡基本用語集
JEOLJEOL

解像力　resolution

SEM像のシャープさを表す量。どの位小さなものが見分けられるかを意味する。本来、画像の上で識別できる二点間の最小距離を言うが、SEMでは、慣用的に二つの物体の隙間を測定している。分解能がその装置を理想的な条件で使ったときに得られる値であるのに対して、解像力は実際に得られた画像上での値であり、試料、装置の状態、倍率などの撮影条件などによって数値は異なる。ただし、分解能と解像力は混同して使われることが多い。

関連する用語

索引トップ用語の索引ランキング

生物学用語辞典
JabionJabion

分解能

英訳・(英)同義/類義語：resolution, resolving power

分析機器や観察機器で、二つの異なる事象を区別できる最小の値。顕微鏡における分解能とは、二点間を有意に識別できる最短距離。
「生物学用語辞典」の他の用語
実験方法装置単位など：  分液漏斗  分画装置  分画遠心法  分解能  制限酵素切断地図  制限酵素切断点  制限酵素断片

索引トップ用語の索引ランキングカテゴリー

音楽用語辞典
ヤマハミュージックメディアヤマハミュージックメディア

分解能 [resolution]

シーケンサーやシーケンスソフトで表現できる一番短い長さの音符のこと。といっても絶対的な時間ではなく、４分音符を何分割することができるかという分割数で表す。４分音符といっても曲によってスピードが違うわけで、テンポが遅くなるほど分解能も粗くなる。パソコンで使われるソフトでは一時48のものがよく使われていたが、最近では「480」から「960」の高分解能が一般的になってきた。

索引トップ用語の索引ランキング

ウィキペディア
ウィキペディアウィキペディア

レゾリューション

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2011/09/08 14:23 UTC 版)

(resolution から転送)

レゾリューション（Resolution、英語で決断、断固たる気性などを意味する）

艦船

楽曲


導出

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2011/03/01 12:38 UTC 版)

(resolution から転送)

導出（どうしゅつ、英: resolution）とは、数理論理学における1つの演繹方法で、三段論法を一般化した導出規則と呼ばれるただ1つの推論規則を用いる。命題論理、述語論理のいずれにも使う事ができ、導出を繰り返すことで証明したい論理式の否定から空節が導かれることにより証明を行う。導出規則と単一化に基づく導出原理（どうしゅつげんり、英: resolution principle）はジョン・アラン・ロビンソン（英語）により1965年に提案され[1]、 その後の定理自動証明に大きな影響を与え、またPrologなどの論理プログラミング言語の基礎となった。

目次

背景

述語論理式 P が恒真であるかを証明する一般的な手続きは存在しないが、1930年に発表されたエルブランの定理はエルブラン領域の要素を論理式に代入して命題論理のレベルに落としその充足不能性を調べることで、¬P が充足不能（恒偽）であれば有限のステップで証明できることを保証している。また、エルブランの論文には単一化アルゴリズムなど他の様々なものが含まれていた[2]。

1950年代以降、計算機上での定理証明の研究が活発になり、ギルモアのアルゴリズム(1960)やデービス・パトナムのアルゴリズム(1958,1960) が考案された。デービス・パトナムのアルゴリズムには連言標準形の使用や導出規則の考え方が含まれていた。しかし、これらはエルブランの定理の証明を直接計算機上で実現したような方法で、エルブラン領域の要素を順次生成して変数を含まない論理式(基礎例)を作成し命題論理のレベルで充足不能性を調べるものだったため、不要な論理式が多数生成され、非常に効率が悪かった[3]。

プラウィツ（Dag Prawitz）は、論理式を生成してからチェックするのではなく、選言標準形に変換した論理式への適当な代入（単一化）によって充足不能性を調べる方法を1960年に提案した[4]。 この方法は必要な基礎例のみを生成するため、不要な論理式の生成が抑えられ効率的だったが、選言標準形は全ての連言項を調べなければならないため全体の効率はいいとは言えなかった。

ロビンソンはデービス・パトナムの枠組みにプラウィツのアイデアを組み合わせ、ただ1つの導出規則と単一化による代入操作とで充足不能性を調べる導出原理を1965年に発表した。単純な規則で関係する論理式のみを段階的に具体化していく方法は、従来の方法よりはるかに効率がよく、また理論的なエレガントさを持っていたため、その後の定理自動証明に大きな影響を与えた[3]。

定義

導出とは二つの節より新しい節を導き出す操作で、一方の節に含まれるリテラル l と、他方の節に含まれる否定リテラル \neg l をのぞき、その他のリテラルの論理和をとることで、新しい節を得ることをいう。

命題論理での導出規則を式で表せば、 \frac{ l \vee P, \quad \neg l \vee Q} {P \vee Q} と書ける。ここで上式は前提となる親節、下式はそれらから導かれる導出節（resolvent）を表す。

あるいは、別の表記法を用いて次のようにも表現できる。前提となる節を C1 と C2 とし, もしリテラル L \in C_1 と否定リテラル \overline{L}\in C_2 が存在するならば、導出節 CR は以下のようになる。

C_R = (C_1 \setminus\{L\}) \cup (C_2 \setminus \{\overline{L}\})

導出規則は三段論法や前件肯定を一般化した規則となっている。 導出は完全な証明系であることが知られている。

例

p \to q を節形式にすると \lnot p \lor q となる。CR をC1,C2 の導出節とすると、前件肯定は以下の導出と同じである。

\begin{array}{ll} C_1 = \lnot p \lor q & \left( p \to q \right) \\ C_2 = p \\ C_R = q & \left( \mathrm{resolvent} \right) \end{array}

同様に、 p \to q 、 q \to r の節形式 \lnot p \lor q 、 \lnot q \lor r による三段論法は以下のようになる。

\begin{array}{ll} C_1 = \lnot p \lor q & \left( p \to q \right) \\ C_2 = \lnot q \lor r & \left( q \to r \right) \\ C_R = \lnot p \lor r & \left( \mathrm{resolvent,\ }p \to r \right) \end{array}

一階述語論理での導出

述語論理のリテラルには個体変数が含まれるため、リテラルと否定リテラルとを単純に比較するだけでは削除できるかどうか分からない。一階述語論理ではリテラルと否定リテラルそれぞれの原子論理式が単一化できる場合に導出を行う。

また、導出の対象となる節は、冠頭標準形にして存在記号を削除したスコーレム連言標準形の論理式である。

例えば、一方の節がリテラル p(x,y)、もう一方の節がリテラル \lnot p(z, f(b)) を含む場合、適切な代入 \sigma =\left\{ z/x, y/f(b) \right\} により各リテラルは p(x,f(b))、 \lnot p(x, f(b)) と書き換えられ、同じにすることができる。ここで代入 \left\{ z/x, y/f(b) \right\} は z \to x、y \to f(b) に書き換えることを表す。

一般に論理式 F1,F2 を等しくする代入を F1,F2 の単一化子（unifier）といい、そのうち最も一般的な単一化子（最汎単一化子）を F1,F2 のmgu（most general unifier）という。上記の例の場合、両方の論理式を等しくする代入は \left\{ z/a, y/f(b), x/a \right\}、\left\{ z/x, y/c, f(b)/c \right\} など無数に存在する。これらは本来の代入 \left\{ z/x, y/f(b) \right\} に \left\{ x/a \right\} などの代入を合成したものなので、最汎単一化子 mgu は \left\{ z/x, y/f(b) \right\} である。

一階述語論理での導出は mgu を用いて次のように表現できる。

もしリテラル L_1 \in C_1 と否定リテラル \overline{L_2}\in C_2 が存在し、 L1 と L2 が mgu σ を持つ場合、以下の CR が2項導出節（binary resolvent）である。ここで、C1σ,C2σ などは、それぞれの節やリテラルに代入 σ を行ったものを表す。

C_R = (C_1\sigma \setminus\{L_1\sigma\}) \cup (C_2\sigma \setminus \{\overline{L_2\sigma}\})

同様のやり方での2以上の複数の節から同時に導出することも可能であり、超導出（hyper-resolution）と呼ばれる。

例

以下の節からの導出を考える。

C_1 = \lnot P (x) \lor \lnot Q (y) \lor R (x, y)
C_2 = Q \left(a \right)
C_3 = P \left(b \right)

Q を単一化する代入 \left\{y/a\right\} により C1 と C2の導出を行うと、

C_R = \lnot P (x) \lor R (x, a)

続いて、P を単一化する代入 \left\{ x/b \right\} により CR と C3の導出を行うと、

C_S = R \left(b, a \right)

を得ることができる。

反駁による証明

反駁（はんばく、英: refutation）とは、節の集合からの導出により空節 □ を導くことである。 反駁については以下の定理が成り立つ。

節の集合 S が充足不能である必要十分条件は、節の集合 S からの導出により空節 □ が導けることである。

これはエルブランの定理を導出に応用したものになっている。

論理式 P が恒真であれば \lnot P は充足不能（恒偽）であるため、節の集合に \lnot P を追加し導出を繰り返すことで空節 □ になれば、論理式 P が恒真であることが証明できる。

反駁により P が P_1, \dots ,P_n の論理的帰結か調べるアルゴリズムは以下のように表現できる。

  1. P_1, \dots ,P_n をスコーレム連言標準形 C_1, \dots ,C_n に変換する。
  2. \lnot P をスコーレム連言標準形 C に変換する。
  3. もし C, C_1, \dots ,C_n の反駁が存在すれば、 P は P_1, \dots ,P_n の論理的帰結である。
あるいは、別の表現をすれば、
  • C, C_1, \dots ,C_n が充足不能
  • \lnot P, P_1, \dots ,P_n が充足不能
  • P_1, \dots ,P_n の解釈が T ならば \lnot P の解釈は F
  • P_1, \dots ,P_n の解釈が T ならば P の解釈は T

例

以下の公式が成り立つ時、P\left(a\right) が成り立つかどうかを証明する場合を考える。反駁の対象となる論理式は以下の論理式に \lnot P(a) を追加したものである。

  1. \forall x \ ((S(x) \lor T(x)) \to P(x)),
  2. \forall x \ (S(x) \lor R(x)),
  3. \lnot R(a)

最初の論理式は (\forall x \ (S(x) \to P(x)) \land (\forall x \ (T(x) \to P(x)) と等価なため、次の2つの節で表現できる。

C_1 = \lnot S(x) \lor P(x)
C_2 = \lnot T(x) \lor P(x)

2番目の論理式は以下の節になる。

C_3 = S(x) \lor R(x)

さらに3番目は以下の節になる。

C_4 = \lnot R(a)

証明したい論理式の否定は以下の節である。

C_5 = \lnot P(a)

これらの節 C1,C2,C3,C4,C5 が反駁の対象となる節集合である。

C3 と C4 の R についての導出を考えると、\left\{ x/a \right\} の代入により以下が導かれる。

C_6 = S \left(a \right)

C1 と C6 の S についての導出を考えると、

C_7 = P\left(a\right)

最後に C5 と C7 の導出により空節 □ が導かれ、P\left(a\right) が成り立つことを証明できる。

証明戦略

導出は２つの節を前提として導出節を導くものであるので、どの節に導出規則を適用するかについては様々な選択肢があり、そのやり方により効率が大幅に異なる。代表的な証明戦略として以下のものがある。

  • 線形導出（linear resolution）
前提となる節の一方を、頂上節（top clause）として指定した節と、頂上節から導出された節に限定する方法。導出木を書くと導出の流れが線状に一列に並ぶため、線形導出と呼ばれる。論理プログラミング言語の代表であるPrologで用いられるSLD導出（Selective Linear resolution for Definite clause）は線形導出の一種である。
  • 入力導出（input resolution）
前提となる節の一方を最初に与えられた節集合の要素（導出された節以外の節）に限定する方法。
  • 支持集合戦略（set-of-support strategy）
あらかじめ支持集合という節の集合を指定しておき、前提となる節の一方を支持集合の節とそこから導出された節に限定する方法。節集合S、T がありS-T が充足可能であるときT はS の支持集合と言う。目標に関係ないところを探索しないよう導出の対象を制限することで、より効率的な導出を行うための手法で、1965年に Lawrence Wos らが提案した[5]。
  • 意味導出（semantic resolution）
論理式のモデルあるいは解釈を利用して導出の対象を制限し、探索の空間を狭めることで効率的な導出を行う手法。特定のモデルにおいて真となる可能性がある節と偽となる可能性のある節とを親節に選ぶ Slagle の Semantic Clash resolution[6] など様々な方法がある。

関連項目

参考文献

  • J. Alan Robinson. "A Machine-Oriented Logic Based on the Resolution Principle." J. Assoc. Comput. Mach. 12, pp.23-41, 1965.
  • Davis Martin. The Early History of Automated Deduction. in Handbook of Automated Reasoning, Volume I, Alan Robinson and Andrei Voronkov(ed), 2001. ISBN 9780444829498.
  • Wolfgang Bibel. Early History and Perspectives of Automated Deduction. in Advances in Artificial Intelligence, Lecture Notes in Computer Science, Springer-Verlag Berlin, 2007. ISBN 9783540745648.
  • Robert Kowalski. Logic for Problem Solving. North Holland, Elsevier, 1979.　ISBN 978-0444003683
  • Gallier, Jean H. (1986). Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Publishers. 
  • 佐藤 泰介. 導出原理による定理証明. 情報処理 22(11), pp.1024-1036, 1981.

脚注

  1. ^ J. Alan Robinson, A Machine-Oriented Logic Based on the Resolution Principle. JACM, Volume 12, Issue 1, pp. 23–41. 1965.
  2. ^ Buss, Samuel R., "On Herbrand's Theorem", in Maurice, Daniel; Leivant, Raphaël, Logic and Computational Complexity, Lecture Notes in Computer Science, Springer-Verlag, pp. 195–209. 1995.
  3. ^ a b Martin Davis. The Early History of Automated Deduction. in Handbook of Automated Reasoning, Volume I, Alan J.A. Robinson and Andrei Voronkov(ed), 2001. ISBN 9780444829498
  4. ^ Wolfgang Bibel. Early History and Perspectives of Automated Deduction. in Advances in Artificial Intelligence, Lecture Notes in Computer Science, Springer-Verlag Berlin, 2007. ISBN 9783540745648
  5. ^ Lawrence Wos, G.A. Robinson, D.F. Carson. Efficiency and Completeness of the Set of Support Strategy in Theorem Proving. Journal of the ACM, Volume12, Issue 4, pp.536-541. 1965.
  6. ^ James Slagle. Automatic Theorem Proving With Renamable and Semantic Resolution. Journal of the ACM, Volume14, Issue 4, pp.687-697. 1967.

外部リンク


索引トップ用語の索引ランキングカテゴリー


resolutionに関係した商品


>> 「resolution」を解説文に含む用語の一覧

>> 「resolution」を含む用語の索引
resolutionのページへのリンク
「resolution」の関連用語
1
RET
画像技術用語
78% |||||

2
FrameDimension.Resolution プロパティ
.NET Framework クラス ライブラリ リファレンス
56% |||||

3
ARP
ネットワーク用語
56% |||||

4
Resolution, Sonate op.158
ピティナ・ピアノ曲名
56% |||||

5
決心、ソナタ
ピティナ・ピアノ曲名
56% |||||

6
Resolution (ニック・ラシェイの曲)
百科事典
52% |||||

7
IntegerValidator コンストラクタ
.NET Framework クラス ライブラリ リファレンス
50% |||||

8
LongValidator コンストラクタ
.NET Framework クラス ライブラリ リファレンス
50% |||||

9
高精度モード
FA用語
50% |||||

10
FrameDimension プロパティ
.NET Framework クラス ライブラリ リファレンス
50% |||||

resolutionのお隣キーワード

RESISTANCE (TM NETWORKの曲)

RESISTANCE〜人類没落の日〜

RESISTANCE 〜報復の刻〜

RESISTANCE (中島美嘉のアルバム)

RESISTANCE (大西結花のアルバム)

Resistor-transistor logic

resolution

Resolution (ROMANTIC MODEの曲)

Resolution (ニック・ラシェイの曲)

resonance

Resonance apart

RESONANCE-T

Resonancia

モバイル
モバイル版のWeblioは、下記のURLからアクセスしてください。
http://m.weblio.jp/
» モバイルで「resolution」を見る
_ _   

resolutionのページの著作権
Weblio 辞書情報提供元は参加元一覧にて確認できます。

  
三省堂三省堂
Copyright (C) 2001-2012 Sanseido Co.,Ltd. All rights reserved.
株式会社 三省堂、三省堂 Web Dictionary
社団法人日本映像ソフト協会社団法人日本映像ソフト協会
Copyright © 2000-2012 Japan Video Software Association
サラウンドWebサラウンドWeb
Copyright Japan Audio Society All Rights Reserved.
日本画像学会日本画像学会
Copyright (C) 2012 The Imaging Society of Japan All rights reserved.
IT用語辞典バイナリIT用語辞典バイナリ
Copyright © 2005-2012 Weblio 辞書 IT用語辞典バイナリさくいん。 この記事は、IT用語辞典バイナリの解像度の記事を利用しております。
JEOLJEOL
Copyright © 1996-2012 JEOL Ltd., All Rights Reserved.
JabionJabion
Copyright (C) 2012 NII,NIG,TUS. All Rights Reserved.
ヤマハミュージックメディアヤマハミュージックメディア
Copyright(C) 2000-2012 YAMAHA MUSIC MEDIA CORPORATION. All Rights Reserved.
ヤマハミュージックメディア、音楽用語ダス
ウィキペディアウィキペディア
All text is available under the terms of the GNU Free Documentation License.
この記事は、ウィキペディアのレゾリューション (改訂履歴)、導出 (改訂履歴)の記事を複製、再配布したものにあたり、GNU Free Documentation Licenseというライセンスの下で提供されています。 Weblio辞書に掲載されているウィキペディアの記事も、全てGNU Free Documentation Licenseの元に提供されております。

©2012 Weblio RSS