大阪大学 情報科学研究科 情報工学 2020年度 離散構造
Author
祭音Myyura (co-authored with GPT 5.6 SOL)
Description
(1) ロボットの動作
状態 s s s について、o n ( s ) on(s) o n ( s ) はロボットが台に乗っていること、s l ( s , x ) sl(s,x) s l ( s , x ) は台が位置 x x x にあること、h a v e ( s ) have(s) ha v e ( s ) はバッテリーを持つことを表す。m o v e ( s , x ) , c l i m b ( s ) , g r a s p ( s ) move(s,x),climb(s),grasp(s) m o v e ( s , x ) , c l imb ( s ) , g r a s p ( s ) はそれぞれ台を位置 x x x へ動かす、台に登る、バッテリーを掴む動作後の状態である。次を仮定する。
A = ∀ s ∀ x ( s l ( s , x ) → s l ( c l i m b ( s ) , x ) ) , B = ∀ s ( ( s l ( s , g o a l ) ∧ o n ( s ) ) → h a v e ( g r a s p ( s ) ) ) , C = ∀ s ∀ x ( ¬ o n ( s ) → s l ( m o v e ( s , x ) , x ) ) , D = ∀ s o n ( c l i m b ( s ) ) . \begin{aligned}
A&=\forall s\forall x(sl(s,x)\to sl(climb(s),x)),\\
B&=\forall s((sl(s,goal)\land on(s))\to have(grasp(s))),\\
C&=\forall s\forall x(\neg on(s)\to sl(move(s,x),x)),\\
D&=\forall s\ on(climb(s)).
\end{aligned} A B C D = ∀ s ∀ x ( s l ( s , x ) → s l ( c l imb ( s ) , x )) , = ∀ s (( s l ( s , g o a l ) ∧ o n ( s )) → ha v e ( g r a s p ( s ))) , = ∀ s ∀ x ( ¬ o n ( s ) → s l ( m o v e ( s , x ) , x )) , = ∀ s o n ( c l imb ( s )) .
(1-1) C , D C,D C , D の意味を説明せよ。
(1-2-1) バッテリーを持つ状態の存在を閉論理式 E E E で表せ。
(1-2-2) F = ( A ∧ B ∧ C ∧ D ) → E F=(A\land B\land C\land D)\to E F = ( A ∧ B ∧ C ∧ D ) → E の否定を、母式が連言標準形の冠頭標準形にせよ。A A A 〜E E E の略号を使わないこと。
(1-2-3) 上の冠頭標準形をスコーレム化して導出原理を適用したが空節を導けなかった。これは初期条件を考慮していないためである。導出原理により E E E を成立させるための初期状態 s 0 s_0 s 0 の条件 I I I を示し、導出過程も示せ。台の初期位置は g o a l goal g o a l ではない。
(1-2-4) I I I を前提に加えた後の導出で、E E E の状態変数への代入として得られる動作列を示せ。
(2) グラフ
頂点集合と辺集合がともに空でない無向グラフを考える。
G 1 G_1 G 1 の頂点は a , b , c , d , e a,b,c,d,e a , b , c , d , e 、辺は a b , b c , a d , b d , c d , b e , d e ab,bc,ad,bd,cd,be,de ab , b c , a d , b d , c d , b e , d e 。G 2 G_2 G 2 の頂点は a , b , c , d , e , f a,b,c,d,e,f a , b , c , d , e , f 、辺は a b , b c , c a , b e , d e , e f , f d ab,bc,ca,be,de,ef,fd ab , b c , c a , b e , d e , e f , fd である。
(2-1) 各グラフで、任意の1辺を取り除いても連結か判定し、そうでなければ切断する辺を示せ。
(2-2-1) 自己ループを持たず、各頂点が少なくとも1本の辺に接続し、全頂点の次数が偶数の連結無向グラフ G G G を考える。任意の辺 ( u , v ) (u,v) ( u , v ) を除いた G ′ G' G ′ にも v v v から u u u への経路があることを示せ。G ′ G' G ′ が連結でないと仮定し、「任意のグラフの全頂点の次数和は偶数」という補題を用いて矛盾を導くこと。
(2-2-2) 任意の頂点 u u u を含み、各辺を高々1回しか使わない閉路があることを示せ(頂点の重複は許す)。(2-2-1)は成り立つものとしてよい。
Kai
(1)
(1-1) C C C は、ロボットが台に乗っていなければ台を任意の位置へ移動できることを表す。D D D は、登る動作の後ではロボットが台に乗っていることを表す。
(1-2-1) E = ∃ s h a v e ( s ) \boxed{E=\exists s\ have(s)} E = ∃ s ha v e ( s ) 。
(1-2-2) 束縛変数を相互に区別すると、求める式は
∀ s 1 ∀ x 1 ∀ s 2 ∀ s 3 ∀ x 3 ∀ s 4 ∀ s 5 [ ( ¬ s l ( s 1 , x 1 ) ∨ s l ( c l i m b ( s 1 ) , x 1 ) ) ∧ ( ¬ s l ( s 2 , g o a l ) ∨ ¬ o n ( s 2 ) ∨ h a v e ( g r a s p ( s 2 ) ) ) ∧ ( o n ( s 3 ) ∨ s l ( m o v e ( s 3 , x 3 ) , x 3 ) ) ∧ o n ( c l i m b ( s 4 ) ) ∧ ¬ h a v e ( s 5 ) ] . \forall s_1\forall x_1\forall s_2\forall s_3\forall x_3\forall s_4\forall s_5\left[\begin{aligned}
&(\neg sl(s_1,x_1)\lor sl(climb(s_1),x_1))\\
{}\land{}&(\neg sl(s_2,goal)\lor\neg on(s_2)\lor have(grasp(s_2)))\\
{}\land{}&(on(s_3)\lor sl(move(s_3,x_3),x_3))\\
{}\land{}&on(climb(s_4))\land\neg have(s_5)
\end{aligned}\right]. ∀ s 1 ∀ x 1 ∀ s 2 ∀ s 3 ∀ x 3 ∀ s 4 ∀ s 5 ∧ ∧ ∧ ( ¬ s l ( s 1 , x 1 ) ∨ s l ( c l imb ( s 1 ) , x 1 )) ( ¬ s l ( s 2 , g o a l ) ∨ ¬ o n ( s 2 ) ∨ ha v e ( g r a s p ( s 2 ))) ( o n ( s 3 ) ∨ s l ( m o v e ( s 3 , x 3 ) , x 3 )) o n ( c l imb ( s 4 )) ∧ ¬ ha v e ( s 5 ) .
(1-2-3) I = ¬ o n ( s 0 ) \boxed{I=\neg on(s_0)} I = ¬ o n ( s 0 ) を加える。m = m o v e ( s 0 , g o a l ) m=move(s_0,goal) m = m o v e ( s 0 , g o a l ) 、c = c l i m b ( m ) c=climb(m) c = c l imb ( m ) と書くと、次の単位節が順に導かれる。
¬ o n ( s 0 ) , C ⊢ s l ( m , g o a l ) , s l ( m , g o a l ) , A ⊢ s l ( c , g o a l ) , D ⊢ o n ( c ) , s l ( c , g o a l ) , o n ( c ) , B ⊢ h a v e ( g r a s p ( c ) ) , h a v e ( g r a s p ( c ) ) , ¬ h a v e ( s 5 ) ⊢ □ . \begin{aligned}
\neg on(s_0),\ C&\vdash sl(m,goal),\\
sl(m,goal),\ A&\vdash sl(c,goal),\\
D&\vdash on(c),\\
sl(c,goal),\ on(c),\ B&\vdash have(grasp(c)),\\
have(grasp(c)),\ \neg have(s_5)&\vdash\square.
\end{aligned} ¬ o n ( s 0 ) , C s l ( m , g o a l ) , A D s l ( c , g o a l ) , o n ( c ) , B ha v e ( g r a s p ( c )) , ¬ ha v e ( s 5 ) ⊢ s l ( m , g o a l ) , ⊢ s l ( c , g o a l ) , ⊢ o n ( c ) , ⊢ ha v e ( g r a s p ( c )) , ⊢ □ .
(1-2-4)
s = g r a s p ( c l i m b ( m o v e ( s 0 , g o a l ) ) ) . \boxed{s=grasp(climb(move(s_0,goal)))}. s = g r a s p ( c l imb ( m o v e ( s 0 , g o a l ))) .
すなわち「台を g o a l goal g o a l へ移動→台に登る→バッテリーを掴む」である。
(2)
(2-1) G 1 G_1 G 1 は全ての辺が閉路上にあるので、どの1辺を除いても連結。G 2 G_2 G 2 は b e \boxed{be} b e を除くと二つの三角形に分かれ、連結でなくなる。
(2-2-1) ( u , v ) (u,v) ( u , v ) を除いて非連結になると仮定し、u u u を含む連結成分を C C C とする。C C C 内では u u u だけ次数が奇数、他は偶数である。よって次数和が奇数となり、握手補題に反する。したがって G ′ G' G ′ は連結で、所要の経路がある。
(2-2-2) u u u に接続する辺 ( u , v ) (u,v) ( u , v ) を一つ選ぶ。(2-2-1)により、その辺を使わない v v v から u u u への単純経路がある。これに ( u , v ) (u,v) ( u , v ) を加えれば、u u u を含み辺の重複がない閉路を得る。