\em{Computability logic} \cite{Jap03,Japic,Japfin}에서 논의된 효율적인 증명 절차에 영감을 받아, 1차 논리(first-order logic)를 위한 휴리스틱 증명 절차를 서술한다. 이는 Gentzen 순차계(sequent system)의 한 변형이며, 다음과 같은 특징을 가진다: (a)~ 순차(sequent)를 기계와 환경 사이의 게임으로 본다, 그리고 (b)~ 증명을 기계의 승리 전략(winning strategy)으로 본다. 이러한 게임 기반 관점에서 강력한 휴리스틱을 추출할 수 있으며, 증명 탐색(proof search)에서 어느 정도의 결정론(determinism)을 확보할 수 있다. 이 논문은 1차 논리에 대하여 새로운 연역 체계 LKg를 제안하고, 그 건전성(soundness)과 완전성(completeness)을 증명한다. 또한 일부 최적화가 추가된 LKg의 변형인 LKg'에 대하여 논의한다.

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