20.6 STRIPS 연산자(Operator)의 형식적 정의