Math Logic / Logic & Formal Verification

명제 및 서술 논리부터 시작하여, 시스템의 올바름을 수학적으로 증명하는 형식 검증 기법을 다루는 학습 노드입니다.

이진 상태의 논리 연산을 수학적으로 정립한 불 대수와 이를 하드웨어로 구현한 논리 회로의 설계 및 최적화 원리를 다루는 학습 노드입니다.

시스템의 상태와 변화를 수학적으로 엄밀하게 기술하는 정형 명세 기법과, 특히 분산 시스템의 설계 결함을 탐지하는 데 탁월한 TLA+의 원리를 다루는 학습 노드입니다.

소스 코드 레벨에서 프로그램이 명세대로 동작함을 수학적으로 입증하는 호어 논리와 루프 불변량, 그리고 정적 분석 기법을 통해 소프트웨어 무결성을 다루는 학습 노드입니다.

컴퓨팅 사고의 가장 원자적인 논리 단위인 명제 논리와 변수 및 양화자를 포함한 서술어 논리를 정의하고, 선언적 스펙 정의와 인공지능 추론의 기초를 다루는 학습 노드입니다.