논리 프로그래밍에서 오랫동안 이어져 온 연구 문제 중 하나는 cut 술어를 논리적이고 고수준의 방식으로 취급하는 것이다. 우리는 이러한 문제는 선형 논리와, G0 ⊕ G1 형태의 선택-이항(disjunctive) 목표 공식(choice-disjunctive goal formulas)을 채택함으로써 해결될 수 있음을 주장한다. 여기서 G0, G1는 목표이다. 이러한 목표가 갖는 의도된 의미는 다음과 같다. 참인 이항 Gi를 선택하고, i (= 0 또는 1)인 해당 Gi를 실행하되, 선택하지 않은 이항은 폐기한다. 실행 중에는 오직 하나의 목표만이 살아 있을 수 있음을 주의하라. 이 목표들은 따라서 서로 배타적인 과업을 고수준의 방식으로 명시할 수 있게 해준다. 또한 cut에는 실패에 의해 구동되는 반복 루프에서 벗어나기 위한 사용과, 효율적인 힙(heap) 관리를 위한 사용이라는 또 다른 용도가 있음을 주의하라. 그러나 불행히도 이와 같은 종류의 cut은 선택-이항 목표의 사용으로 대체할 수 없다.

*본 초록은 AI를 통해 원문을 번역한 내용입니다. 정확한 내용은 하기 원문에서 확인해주세요.