함수형 프로그램 (functional programs)을 자동으로 검증하기 위한 여러 실용적인 도구들(예: Liquid Haskell 및 Scala 프로그램을 위한 Leon)은 재귀 함수 정의를 언롤링 (unrolling)한 후 SMT 솔버 (SMT solvers)를 사용하여 한정자 없는 추론 (quantifier-free reasoning)을 수행하는 휴리스틱 (heuristic)에 의존합니다. 우리는 이 휴리스틱의 근본적인 이론적 특성을 밝혀냈으며, 이것이 대수적 데이터 타입 (algebraic datatypes)의 1차 논리 (First-Order) 이론과 배경 이론 (background theories)이 결합된 추론에 대해 실제로 완전한 (complete) 기술로 일반화되고 공식화될 수 있음을 보여줍니다. 여기서 배경 이론은 결정 가능한 (decidable) 한정자 없는 추론을 지원합니다. 본 논문에서 개발된 이론은 이러한 휴리스틱이 성공할 때의 효능을 설명하고, 실패할 때 왜 실패하는지를 설명하며, 증명을 성공시키는 데 있어 사용자 지원 (user help)이 수행하는 정확한 역할을 설명합니다.