전산학의 많은 응용 분야에서 숫자의 배열이나 집합과 같은 단순한 자료 구조로는 표현하기 어렵거나 부자연스러운 묘사적 기술문을 데이터베이스에 저장하여 사용해야 할 경우에 정보를 표현하기 위하여 흔히 사용되는 형식 언어 1차 술어 논리.  

1차 술어 논리의 구문은 술어 심벌, 변수 심벌, 상수 심벌, 괄호, 쉼표 등을 알파벳으로 하여 구성되는 원자식(atomic formula)들을 ∧(and), ∨(or), →(implication) 등의 연결자로 연결하여 합법 구성식을 구성하고, 이 합법 구성식들을 허용 가능한 문장으로 하여 정의된다. 이러한 문장들의 진위 여부는 각 심벌들에 부가되는 의미에 의해 정의된다. 명제 논리는 1차 술어 논리의 부분 집합으로서 변수가 문장에 등장하지 않는다. 이러한 명제 논리는 실제로 많은 간단한 영역(domain)에서는 유용한 표현 수단이 되고 있다.