컴퓨터 공학에서의 논리학

Logic in computer science
학술회의 LICS에 대해서는, 「컴퓨터 사이언스의 논리 심포지엄」을 참조해 주세요.
컴퓨터 로직 게이트의 도식적 표현

컴퓨터 공학에서 논리는 논리학과 컴퓨터 과학 분야 사이의 중복을 다룬다.토픽은 기본적으로 다음 세 가지 주요 영역으로 나눌 수 있습니다.

  • 이론적 기초 및 분석
  • 논리학자를 지원하기 위한 컴퓨터 테크놀로지 사용
  • 컴퓨터 응용 프로그램에 논리 개념 사용

이론적 기초 및 분석

논리는 컴퓨터 과학에서 기본적인 역할을 한다.특히 중요한 논리의 핵심 영역 중 일부는 계산 가능성 이론(이전에는 재귀 이론이라고 불림), 모달 논리 및 범주 이론입니다.계산 이론은 알론조 교회와 앨런 [1][2]튜링과 같은 논리학자들과 수학자들에 의해 정의된 개념에 기초한다.처치는 처음에 람다 정의성의 개념을 사용하여 알고리즘적으로 해결할 수 없는 문제의 존재를 보여주었다.튜링은 기계적 절차라고 불릴 수 있는 것에 대한 최초의 설득력 있는 분석을 했고, 쿠르트 괴델은 튜링의 분석이 "완벽하다"[3]고 단언했다.또한 논리와 컴퓨터 과학이 이론적으로 중복되는 다른 주요 분야는 다음과 같습니다.

  • 괴델의 불완전성 정리는 산수를 특징지을 만큼 강력한 논리체계는 그 체계 내에서 증명될 수도 반증될 수도 없는 진술들을 포함할 것이라는 것을 증명한다.이는 소프트웨어의 [4]완전성과 정확성을 입증하는 타당성과 관련된 이론적 문제에 직접 적용됩니다.
  • 프레임 문제는 인공지능 [5]에이전트의 목표와 상태를 나타내기 위해 1차 로직을 사용할 때 극복해야 하는 기본적인 문제입니다.
  • Curry-Howard 대응은 논리 시스템과 소프트웨어의 관계입니다.이 이론은 증명과 프로그램 사이의 정확한 일치성을 확립했다.특히 단순 유형 람다 계산의 항이 직관적 명제 논리의 증거에 해당한다는 것을 보여주었다.
  • 범주 이론은 구조 간의 관계를 강조하는 수학의 관점을 나타냅니다.이것은 컴퓨터 과학의 많은 측면과 밀접하게 관련되어 있습니다: 프로그래밍 언어, 전이 시스템 이론, 프로그래밍 언어 모델 및 프로그래밍 언어 [6]의미론.

논리학자를 지원하는 컴퓨터

인공지능이라는 용어를 사용한 최초의 응용 프로그램 중 하나는 앨런 뉴웰이 개발한 논리 이론가 시스템이다.쇼와 허버트 사이먼이 1956년에.논리학자가 하는 일 중 하나는 논리학에서 일련의 진술을 취하여 논리 법칙에 의해 진실이어야 하는 결론(추가 진술)을 추론하는 것입니다.예를 들어, "모든 인간은 죽는다"와 "소크라테스는 인간이다"라는 논리체계가 주어진다면, 유효한 결론은 "소크라테스는 죽는다"이다.물론 이것은 사소한 예시이다.실제 논리 시스템에서는 문장이 많고 복잡할 수 있습니다.이러한 분석은 컴퓨터를 사용함으로써 큰 도움이 될 수 있다는 것을 일찍부터 깨달았습니다.논리 이론가는 버트런드 러셀과 알프레드 노스 화이트헤드의 수학 논리에 대한 영향력 있는 연구인 프린키피아 매스매티카의 이론적 연구를 검증했다.또한 후속 시스템은 논리학자들이 새로운 논리 정리와 증거를 [7]검증하고 발견하기 위해 사용되었습니다.

컴퓨터용 논리 응용 프로그램

인공지능(AI) 분야에는 항상 수리논리의 영향이 컸다.논리 추론을 자동화하는 기술은 문제를 해결하고 사실로부터 결론을 도출할 수 있는 큰 잠재력을 가지고 있다는 것을 처음부터 깨달았습니다.Ron Brachman은 모든 AI 지식 표현 형식을 평가해야 하는 메트릭으로 FOL(First-order Logic)을 설명했습니다.정보를 기술하고 분석하는 데 FOL만큼 일반적이거나 강력한 방법은 없습니다.FOL 자체가 컴퓨터 언어로 사용되지 않는 이유는 FOL이 아무리 강력한 컴퓨터라도 해결할 수 없는 문장을 쉽게 표현할 수 있다는 점에서 사실 너무 표현력이 강하기 때문입니다.이러한 이유로 모든 형태의 지식 표현은 어떤 의미에서 표현성과 계산 가능성 사이에서 균형을 이룬다.표현력이 높은 언어일수록 FOL에 가까울수록 속도가 느려지고 무한 [8]루프가 발생할 가능성이 높아집니다.

예를 들어, 전문가 시스템에서 사용되는 IF THEN 규칙은 매우 제한된 FOL의 서브셋에 가깝습니다. 논리 연산자의 모든 범위를 갖는 임의의 공식보다는 논리학자들이 말하는 모더스 포넨이 시작점입니다.그 결과 규칙 기반 시스템은 특히 최적화 알고리즘과 [9]컴파일을 이용하는 경우 고성능 계산을 지원할 수 있습니다.

논리 이론의 또 다른 주요 연구 분야는 소프트웨어 공학이었다.Knowledge Based Software Assistant 및 Programmer's Apprentice 프로그램과 같은 연구 프로젝트에서는 논리 이론을 적용하여 소프트웨어 사양의 정확성을 검증했습니다.또한 다양한 플랫폼에서 규격을 효율적인 코드로 변환하고 구현과 [10]규격 간의 동등성을 증명하기 위해 이 규격을 사용했습니다.이러한 형식적인 혁신 중심 접근 방식은 기존 소프트웨어 개발보다 훨씬 더 많은 노력을 기울입니다.그러나 적절한 형식과 재사용 가능한 템플릿을 사용하는 특정 영역에서는 이 접근 방식이 상용 제품에 대해 실행 가능한 것으로 입증되었습니다.적절한 영역은 일반적으로 무기 시스템, 보안 시스템, 실시간 금융 시스템과 같은 영역이며, 시스템 장애로 인해 인적 또는 재정적 비용이 과도하게 많이 발생합니다.이러한 도메인의 예로는 디지털 디바이스의 CPU 및 기타 중요한 컴포넌트에 사용되는 칩을 설계하는 프로세스인 VLSI(Very Large Scale Integrated) 설계가 있습니다.칩의 에러는 치명적입니다.소프트웨어와는 달리 칩은 패치나 업데이트가 불가능합니다.그 결과 구현이 [11]사양에 대응하고 있음을 증명하기 위해 정식 방법을 사용하는 것이 상업적으로 정당화된다.

컴퓨터 기술에 대한 논리의 또 다른 중요한 적용 분야는 프레임 언어와 자동 분류기입니다.KL-ONE 등의 프레임 언어에는 엄밀한 의미가 있습니다.KL-ONE의 정의는 집합론과 술어 미적분에 직접 매핑될 수 있습니다.이를 통해 분류자라고 불리는 특수 정리 프로버는 주어진 모델에서 집합, 부분 집합 및 관계 사이의 다양한 선언을 분석할 수 있습니다.이 방법으로 모델의 유효성을 확인하고 일관되지 않은 정의에 플래그를 지정할 수 있습니다.분류자는 새로운 정보를 추론할 수도 있습니다.예를 들어 기존 정보를 기반으로 새 집합을 정의하고 새 데이터를 기반으로 기존 집합의 정의를 변경할 수 있습니다.유연성의 레벨은, 계속 변화하는 인터넷의 세계에의 대처에 최적입니다.분류기 기술은 Web Ontology Language와 같은 언어 위에 구축되어 기존 인터넷에 논리적인 의미 수준을 제공할 수 있습니다.이 레이어는 [12][13]시멘틱웹이라고 불립니다

시간 논리는 동시 시스템에서 [14]추론을 위해 사용됩니다.

「 」를 참조해 주세요.

레퍼런스

  1. ^ Lewis, Harry R. (1981). Elements of the Theory of Computation. Prentice Hall.
  2. ^ Davis, Martin (11 May 1995). "Influences of Mathematical Logic on Computer Science". In Rolf Herken (ed.). The Universal Turing Machine. Springer Verlag. ISBN 9783211826379. Retrieved 26 December 2013.
  3. ^ Kennedy, Juliette (2014-08-21). Interpreting Godel. Cambridge University Press. ISBN 9781107002661. Retrieved 17 August 2015.
  4. ^ Hofstadter, Douglas R. (1999-02-05). Gödel, Escher, Bach: An Eternal Golden Braid. Basic Books. ISBN 978-0465026562.
  5. ^ McCarthy, John; P.J. Hayes (1969). "Some philosophical problems from the standpoint of artificial intelligence" (PDF). Machine Intelligence. 4: 463–502.
  6. ^ Barr, Michael; Charles Wells (1998). Category Theory for Computing Science (PDF). Centre de Recherches Mathématiques.
  7. ^ Newell, Allen; J.C. Shaw; H.C. Simon (1963). "Empirical explorations with the logic theory machine". In Ed Feigenbaum (ed.). Computers and Thought. McGraw Hill. pp. 109–133. ISBN 978-0262560924.
  8. ^ Levesque, Hector; Ronald Brachman (1985). "A Fundamental Tradeoff in Knowledge Representation and Reasoning". In Ronald Brachman and Hector J. Levesque (ed.). Reading in Knowledge Representation. Morgan Kaufmann. p. 49. ISBN 0-934613-01-X. The good news in reducing KR service to theorem proving is that we now have a very clear, very specific notion of what the KR system should do; the bad new is that it is also clear that the services can not be provided... deciding whether or not a sentence in FOL is a theorem... is unsolvable.
  9. ^ Forgy, Charles (1982). "Rete: A Fast Algorithm for the Many Pattern/Many Object Pattern Match Problem*" (PDF). Artificial Intelligence. 19: 17–37. doi:10.1016/0004-3702(82)90020-0. Archived from the original (PDF) on 2013-12-27. Retrieved 25 December 2013.
  10. ^ Rich, Charles; Richard C. Waters (November 1987). "The Programmer's Apprentice Project: A Research Overview" (PDF). IEEE Expert. Archived from the original (PDF) on 2017-07-06. Retrieved 26 December 2013.
  11. ^ Stavridou, Victoria (1993). Formal Methods in Circuit Design. Press Syndicate of the University of Cambridge. ISBN 0-521-443369. Retrieved 26 December 2013.
  12. ^ MacGregor, Robert (June 1991). "Using a description classifier to enhance knowledge representation". IEEE Expert. 6 (3): 41–46. doi:10.1109/64.87683. S2CID 29575443.
  13. ^ Berners-Lee, Tim; James Hendler; Ora Lassila (May 17, 2001). "The Semantic Web A new form of Web content that is meaningful to computers will unleash a revolution of new possibilities". Scientific American. 284: 34–43. doi:10.1038/scientificamerican0501-34. Archived from the original on April 24, 2013.
  14. ^ Colin Stirling (1992). "Modal and Temporal Logics". In S. Abramsky; D. M. Gabbay; T. S. E. Maibaum (eds.). Handbook of Logic in Computer Science. Vol. II. Oxford University Press. pp. 477–563. ISBN 0-19-853761-1.

추가 정보

외부 링크