논리 프레임워크

논리학에서 논리체계는 원논리에서 공식의 실현가능성이 프레임워크유형 이론에서 유형 거주 문제로 감소하는 방식으로 고차형 이론에서 서명으로 논리학을 정의(또는 제시)할 수 있는 수단을 제공한다.^[1]^[2]이 접근방식은 (상호작용) 자동화된 정리 증명에 성공적으로 사용되어 왔다.첫 번째 논리적인 틀은 오토마스였다. 그러나, 아이디어의 이름은 더 널리 알려진 에딘버러 논리 프레임워크, LF에서 왔다. 이사벨과 같은 최근의 몇 가지 증명 도구들은 이 생각에 기초하고 있다.^[1]직접 임베딩과 달리, 논리 프레임워크 접근방식은 많은 로직들이 동일한 유형 시스템에 임베딩될 수 있도록 한다.^[3]

개요

논리적인 틀은 의존적으로 타이핑된 람다 미적분학을 이용하여 구문, 규칙 및 증명에 대한 일반적인 처리에 기초한다.구문은 Per Martin-Löf의 예술 체계와 유사하지만 더 일반적인 스타일로 취급된다.

논리적 프레임워크를 설명하려면 다음을 제공해야 한다.

나타낼 개체 로직 클래스의 특성화.
적절한 메타 언어;
개체 로직을 나타내는 메커니즘의 특성화.

이를 요약하면 다음과 같다.

"프레임워크 = 언어 + 표현"

LF

LF 논리 프레임워크의 경우 메타 언어는 λπ-미적분이다.이는 제안이 유형원리로서 1차 최소논리에 관련되는 1차 종속 기능 유형 시스템이다.λ-미적분의 주요 특징은 3가지 수준의 개체, 유형 및 종류(또는 유형 분류 또는 유형 분류)로 구성된다는 것이다.그것은 전제적이며, 모든 잘 만들어진 용어들은 강하게 정상화되고 있으며, 잘 만들어진 것으로서 교회-로스터와 잘 만들어진 성질은 해독할 수 있다.그러나 유형 추론은 이해할 수 없다.

논리는 유형별 표현 메커니즘에 의해 LF 논리 프레임워크에 표현된다.이는 1983년 시에나 강의에서 페르 마르틴 뢰프가 칸트의 판단 개념을 발전시킨 데서 영감을 받은 것이다.두 개의 고차원의 판단인 가상 $J\vdash K$ $J\vdash K$ $J\vdash K$ ${\displaystyle$ J $\vdash$ K}과 $J\vdash K$ 일반 $J\vdash K$ $\Lambda x\in J.K(x)$ x $\Lambda x\in J.K(x)$ $\Lambda x\in J.K(x)$ . K $\Lambda x\in J.K(x)$ ( x $\Lambda x\in J.K(x)$ ) ${\displaystyle \Lambda$ x $\in J.K(x)}$ 는 각각 일반 및 종속 함수 공간에 해당한다 $\Lambda x\in J.K(x)$ 유형별 판단의 방법론은 판단을 증거의 유형으로 나타낸다는 것이다.논리 시스템 ${\mathcal {L}}$ ${\$ 은 ${\mathcal L}$ 구문, 판단 및 규칙 체계를 나타내는 유한한 상수 집합에 종류와 유형을 할당하는 서명으로 표현된다.사물 논리학자의 규칙과 증거는 $\Lambda x\in C.J(x)\vdash K$ $\Lambda x\in C.J(x)\vdash K$ $\Lambda x\in C.J(x)\vdash K$ $\Lambda x\in C.J(x)\vdash K$ . $\Lambda x\in C.J(x)\vdash K$ ( x $\Lambda x\in C.J(x)\vdash K$ ) $\Lambda x\in C.J(x)\vdash K$ $\Lambda x\in C.J(x)\vdash K$ ${\displaystyle \Lambda x\in C$ 의 저혈압 일반적 판단의 원시적 증거로 보여진다 $.$ $J(x)\vdash$ K $\Lambda x\in C.J(x)\vdash K$

LF 논리 프레임워크의 구현은 카네기 멜론 대학교의 12번째 시스템에 의해 제공된다.12는 다음을 포함한다.

논리 프로그래밍 엔진
로직 프로그램에 대한 메타 데이터 추론(프로토콜, 커버리지 등)
귀납적인 메타논리적인 정리.

참고 항목

참조

^ ^a ^b Bart Jacobs (2001). Categorical Logic and Type Theory. Elsevier. p. 598. ISBN 978-0-444-50853-9.
^ Dov M. Gabbay, ed. (1994). What is a logical system?. Clarendon Press. p. 382. ISBN 978-0-19-853859-2.
^ Ana Bove; Luis Soares Barbosa; Alberto Pardo (2009). Language Engineering and Rigourous (sic) Software Development: International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24 - March 1, 2008, Revised, Selected Papers. Springer. p. 48. ISBN 978-3-642-03152-6.

추가 읽기

Frank Pfenning (2002). "Logical frameworks – a brief introduction". In Helmut Schwichtenberg, Ralf Steinbrüggen (ed.). Proof and system-reliability (PDF). Springer. ISBN 978-1-4020-0608-1.
로버트 하퍼, 후리오 혼셀, 고든 플롯킨.로직 정의 프레임워크.컴퓨터 기계 협회 저널, 40(1):143-184, 1993.
아르논 에이브론, 후리오 혼셀, 이안 메이슨, 랜디 폴락.기계에 공식적인 시스템을 구현하기 위해 입력된 람다 미적분학을 사용한다.자동 추론 저널, 1992년 9시 309-354.
로버트 하퍼LF의 등분형성1988년 에든버러 대학의 기술 보고서.LFCS 보고 ECS-LFCS-88-67
로버트 하퍼, 도널드 산넬라, 안제이 탈레키.구조화된 이론 발표 및 논리 표현.순수 및 응용 논리 연보, 67(1-3):113-160, 1994.
Samin Ishtiaq와 David Pym.자연공제의 관련성 분석.논리와 연산 제8권, 809-838권, 1998.
Samin Ishtiaq와 David Pym.종속형 Bunched $\lambda$ $\lambda$ - 미적분학의 $\lambda$ Kripke 리소스 모델논리 연산 12(6), 1061-1104, 2002.
Per Martin-Löf. "논리적 상수의 의미와 논리적 법칙의 정당성에 대하여." "논리적 논리의 비논리적 저널", 1(1): 11-60, 1996.
벵트 노르드스트룀, 켄트 피터슨, 얀 M. 스미스.마틴 뢰프의 유형 이론에서의 프로그래밍.옥스퍼드 대학 출판부, 1990. (이 책은 절판되었지만 무료 버전이 나왔다.)
데이비드 핌. $\lambda \Pi$ $\lambda \Pi$ - 미적분학의 $\lambda \Pi$ 증명 이론에 대한 참고.Studia Logica 54: 199-230, 1995.
데이비드 핌과 링컨 월렌. $\lambda \Pi$ $\lambda \Pi$ $\lambda \Pi$ - 미적분학에서 $\lambda \Pi$ 교정 검색.인: G. Huet과 G. Plotkin (eds), Logical Frameworks, Cambridge University Press, 1991.
디디에 갈미쉬와 데이비드 핌.유형-이론적 언어로 된 교정 검색:소개이론 컴퓨터 과학 232(2000) 5-53.
필리파 가드너유형 이론에서 로직 표현.1992년 에든버러 대학의 기술 보고서.LFCS 보고서 ECS-LFCS-92-227.
길레스 다우크람다-피-미적분학에서 오타가 불분명함.M. Bezem, J.F. Groote(Eds.)에 람다 칼쿨리 및 응용 프로그램을 입력하십시오.컴퓨터 과학 강의 노트 제664권, 1993년 139-145.
데이비드 핌.일반 로직의 증명, 검색 및 계산.1990년 에든버러 대학의 박사 논문.
데이비드 핌. $\lambda \Pi$ { $\lambda \Pi$ - 미적분학을 $\lambda \Pi$ 위한 통일 알고리즘.컴퓨터 과학 국제 학술지 3(3), 333-378, 1992.

외부 링크

특정 논리적 프레임워크 및 구현(Frank Pfenning이 유지 관리하는 목록, 그러나 대부분은 1997년부터 사용 중지된 링크)

[Jacobs2001-1] Bart Jacobs (2001). Categorical Logic and Type Theory. Elsevier. p. 598. ISBN 978-0-444-50853-9.

[Gabbay1994-2] Dov M. Gabbay, ed. (1994). What is a logical system?. Clarendon Press. p. 382. ISBN 978-0-19-853859-2.

[BoveBarbosa2009-3] Ana Bove; Luis Soares Barbosa; Alberto Pardo (2009). Language Engineering and Rigourous (sic) Software Development: International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24 - March 1, 2008, Revised, Selected Papers. Springer. p. 48. ISBN 978-3-642-03152-6.

[1]

[2]

[3]

Search

논리 프레임워크

네임스페이스

더

목차

개요

LF

참고 항목

참조

추가 읽기

외부 링크