4
나는 "Concrete semantics with Isabelle/HOL"을 읽고 있으며 고차원 논리에 매우 흥미로워지고 있습니다. 나는 보통의 1 차 논리와 몇 가지 모달 논리를 알고 있지만, 고차원 논리와 그 메타 이론에 대한 이전의 노출은 거의 없다. 그래서 나는 그 격차를 메꾸기를 원한다. 나는 HOL이 본질적으로 교회의 단순한 유형의 이론이고 순수한 것은 이전의 직관 주의적 변형이라고 읽었습니다. 문제는 "본질적으로"라는 단어입니다. Isabelle/HOL과 Isabelle/Pure 이론은 예를 들어 Andrews' textbook과 어떻게 다른가요? Isabelle/HOL과 Isabelle/Pure에서 사용되는 고차원 논리의 종류에 대한 교과서 소개가 있으며, 이들의 메타 속성 속성에 대한 논의가 있습니까?HOL, Isabelle 등과 같이 고차원 논리에 대한 참조 정의가 있습니까?