고정점 논리(영어: Fixed-point logic)는 수리 논리학 및 이론 컴퓨터 과학에서 사용되는 논리 체계로, 일차 논리(first-order logic, FO)에 고정점 연산자(fixed-point operator)를 추가한 확장형이다. 고정점 연산자는 어떤 정의된 관계에 대하여 가장 작은(최소) 또는 가장 큰(최대) 고정점을 형성하도록 허용함으로써, 재귀적·귀납적 정의를 논리식 안에서 직접 표현할 수 있게 한다.
고정점 논리의 발전은 기술 복잡도 이론(descriptive complexity theory)과 데이터베이스 질의어, 특히 Datalog와의 관계에 의해 촉진되었다. 최소 고정점 논리(least fixed-point logic)는 1974년 이안니스 N. 모스호바키스(Yiannis N. Moschovakis)에 의해 처음으로 체계적으로 연구되었고, 1979년 앨프리드 에이호(Alfred V. Aho)와 제프리 울먼(Jeffrey D. Ullman)이 고정점 논리를 표현적인 데이터베이스 질의어로 제안하면서 컴퓨터 과학자들에게 소개되었다.
고정점 논리는 크게 다음과 같은 하위 체계로 분류된다.
부분 고정점 논리(Partial Fixed-Point Logic, FO[PFP])는 부분 고정점 연산자 PFP를 사용하여, 반복 과정에서 고정점이 존재하면 그 값을 취하고, 그렇지 않으면 거짓으로 정의한다. 반복 술어는 일반적으로 단조적이지 않으므로 고정점이 항상 존재하지 않을 수도 있다. 정렬된 유한 구조에서 FO(PFP)로 표현할 수 있는 속성은 PSPACE에 속하는 속성임이 증명되었다.
최소 고정점 논리(Least Fixed-Point Logic, FO[LFP])는 부분 고정점이 P의 양의 발생(짝수 개의 부정에 선행된 발생)만 포함하는 공식에 대해서만 취해지는 FO(PFP)의 부분 집합이다. 이는 고정점 구성의 단조성을 보장한다. 닐 이머만(Neil Immerman)과 모셰 바르디(Moshe Y. Vardi)가 독립적으로 증명한 이머만-바르디 정리(Immerman–Vardi theorem)는 FO(LFP)가 모든 정렬된 구조에서 PTIME(P)을 특징짓는다는 것을 보여준다. 최소 고정점 논리의 표현성은 데이터베이스 질의 언어인 Datalog의 표현성과 정확히 일치한다.
팽창 고정점 논리(Inflationary Fixed-Point Logic, FO[IFP])는 반복의 모든 단계에서 새 튜플만 추가하고 기존 튜플을 제거하지 않는 방식으로 단조성을 보장한다. 모든 FO(IFP) 공식은 FO(LFP) 공식과 동등함이 알려져 있다.
전이 폐포 논리(Transitive Closure Logic, FO[TC])는 임의의 술어에 대한 귀납 대신 전이 폐포(transitive closure)만을 직접 표현할 수 있도록 한다. 정렬된 구조에서 FO[TC]는 복잡도 클래스 NL을 특징짓는다. 이 특징화는 NL이 보수 하에서 닫혀 있다는 이머만의 증명(NL = co-NL)의 중요한 부분이다.
결정적 전이 폐포 논리(Deterministic Transitive Closure Logic, FO[DTC])는 전이 폐포 연산자가 결정적인 FO(TC)로 정의된다. 정렬된 구조에서 FO[DTC]는 복잡도 클래스 L을 특징짓는다.
고정점 논리는 유한 모델 이론(finite model theory)과 서술 복잡도(descriptive complexity)의 핵심 분야로, 논리적 표현력과 계산 복잡도 사이의 관계를 연구하는 데 중요한 역할을 한다.
