에르브랑 구조

1차 논리에서 에르브랑 구조 ()는 어휘 (때로는 서명이라고도 함)에 대한 구조로, 의 통사적 속성에 의해서만 정의된다. 아이디어는 항의 기호 문자열을 값으로 취하는 것이다. 예를 들어, 상수 기호 의 표기는 단순히 "" (기호)이다. 이는 자크 에르브랑의 이름을 따서 명명되었다.

에르브랑 구조는 논리형 프로그래밍의 기초에서 중요한 역할을 한다.

 에르브랑 해석 영역 
 정의 
에르브랑 해석 영역은 에르브랑 구조에서 해석 영역 역할을 한다.

 예시 
어휘가 다음과 같은 1차 언어 가 있다고 하자.
 상수 기호: 
 함수 기호: 
그러면  (또는 )의 에르브랑 해석 영역 는 다음과 같다.

관계 기호는 관계만 포함하는 공식이 해석 영역의 원소에 해당하지 않으므로 에르브랑 해석 영역과는 관련이 없다.상수 또는 변수 집합에서 평가된 관계 로만 구성된 공식은 해석 영역 의 유한 거듭제곱의 부분집합에 해당하며, 여기서 은 의 항수이다.

 에르브랑 구조 
에르브랑 구조는 에르브랑 해석 영역 위에 항들을 해석한다.

 정의 
어휘 와 해석 영역 를 가진 구조 가 있다고 하자. 는 에 대한 모든 항들의 집합이고, 는 모든 변수 없는 항들의 부분집합이라고 하자. 가 에르브랑 구조인 것은 다음을 만족할 때이다.


 모든 항 함수 기호 와 에 대해 
 의 모든 상수 에 대해 

 비고 
 는 의 에르브랑 해석 영역이다.
 이론 의 모형인 에르브랑 구조는 의 에르브랑 모형이라고 불린다.

 예시 
상수 기호 와 단항 함수 기호 에 대해 다음 해석을 가진다.





 에르브랑 기저 
에서 정의된 해석 영역과 에서 정의된 항의 표기 외에, 에르브랑 기저는 관계 기호를 표기함으로써 해석을 완성한다.

 정의 
에르브랑 구조에 대한 에르브랑 기저 는 인자 항이 에르브랑 해석 영역의 원소인 모든 원자 공식들의 집합이다.

 예시 
이항 관계 기호 에 대해 위의 항들을 사용하면 다음과 같다.



 같이 보기 
 에르브랑의 정리
 Herbrandization
 에르브랑 해석

 내용주 

 각주 


분류:수리논리학