[서성현]

resolution rule을 적용하는 부분에서 뭔가 잘못된 것 아닌가요?
강의슬라이드에 나와 있는 방법대로 resolution rule을 적용하면 아래와 같이 됩니다.



이제 resolution rule을 적용하자.

{
A( u, u ),
￢A( v, w )∨A( w, v ),
￢A( x, y )∨￢A( y, z )∨A( x, z ),
￢A( a, b ),
A( a, c ),
A( b, c )
}


there are
￢A( x, y )∨￢A( y, z )∨A( x, z ),
￢A( a, b )
and { a/x, b/z } unifies
A( x, z ),
A( a, b )
therefore
add ￢A( a, y )∨￢A( y, b )


{
A( u, u ),
￢A( v, w )∨A( w, v ),
￢A( x, y )∨￢A( y, z )∨A( x, z ),
￢A( a, b ),
A( a, c ),
A( b, c ),
￢A( a, y )∨￢A( y, b )
}


there are
￢A( v, w )∨A( w, v )
A( b, c )
and { b/v, c/w } unifies
A( v, w ),
A( b, c )
therefore
add A( c, b )


{
A( u, u ),
￢A( v, w )∨A( w, v ),
￢A( x, y )∨￢A( y, z )∨A( x, z ),
￢A( a, b ),
A( a, c ),
A( b, c ),
￢A( a, y )∨￢A( y, b ),
A( c, b )
}


there are
A( a, c ),
￢A( a, y )∨￢A( y, b )
and { c/y } unifies
A( a, c ),
A( a, y )
therefore
add ￢A( c, b )


{
A( u, u ),
￢A( v, w )∨A( w, v ),
￢A( x, y )∨￢A( y, z )∨A( x, z ),
￢A( a, b ),
A( a, c ),
A( b, c ),
￢A( a, y )∨￢A( y, b ),
A( c, b ),
￢A( c, b )
}


there are
A( c, b ),
￢A( c, b )
and {} unifies
A( c, b ),
A( c, b )
therefore
add ;;


∴ unsatisfiable
∴ 원래의 명제는 valid



p.s. 흑.. 저도 퀴즈 볼 때 조교님같이 답이 not valid로 나왔었는데
다시 풀어보니 아니군요.. ㅠㅠ
_________________
http://snupl.wo.to

[김진현]

Resolution 을 안 쓰더라도, 쉽게 증명 가능할 것 같습니다.

요만 적으면(우리가 배운 rule이 아니더라도):

ㄱA(x, y)라고 합시다.

그리고 !z.( A(x, z) -> ㄱA(y, z) ) 는,

!z.( ㄱA(x, z) or ㄱA(y, z) ) 고,

ㄱ?z.( A(x, z) and A(y, z) ) 입니다.

A(x, z) 이고 A(y, z)인 z가 존재한다고 가정하면,

A(y, z) 에서 A(z, y) 가 나오고, A(x, z)가 있으므로 A(x, y) 가 나오는데,

애초에 ㄱA(x, y) 라고 했으니 모순이 됩니다.

따라서 valid 한 것 같습니다.
_________________
The kingdom of heaven has been forcefully advancing, and forceful men lay hold of it.

[정영범]

이전에 존재하는 식을 지우는 우를 범했습니다. ㅜㅡ
좋은 지적 감사합니다.
다시 고쳐서 올렸습니다.