명제논리 (Propositional Logic)
쉽게 풀면
"내일 비가 온다"처럼 참 또는 거짓을 딱 잘라 말할 수 있는 문장을 명제라고 합니다. 반면 "오늘 날씨가 춥다"는 사람마다 기준이 달라 명제가 아닙니다. 명제논리는 이런 명제들을 레고 블록처럼 취급해서, "P이고 Q이다(AND)", "P이거나 Q이다(OR)", "P가 아니다(NOT)", "P이면 Q이다(조건문)"와 같은 방식으로 조립합니다. 중요한 점은 P와 Q의 실제 내용이 무엇이든 상관없이, 오직 참/거짓이라는 값만으로 전체 문장의 참거짓이 기계적으로 정해진다는 것입니다. 그래서 명제논리는 내용과 무관하게 "형식"만으로 추론이 타당한지 검증하는 도구로 쓰입니다.
왜 중요한가
명제논리는 컴퓨터과학의 회로 설계, 프로그램 검증, 자동정리증명, 데이터베이스 질의 등 형식적 추론이 필요한 거의 모든 분야의 기초 언어로 쓰입니다. 철학의 논증 분석이나 언어학의 의미론 연구에서도 자연어 문장의 논리적 구조를 명확히 하기 위한 도구로 활용됩니다. 명제논리 자체는 비교적 단순한 체계지만, 이를 확장한 술어논리(predicate logic)나 모달논리 등이 인공지능의 지식표현과 추론 시스템의 근간을 이루기 때문에 관련 연구에서 반복적으로 등장합니다.
논문에서는 이렇게 쓰입니다
이 문장은 알고리즘이 항상 올바르게 동작한다는 주장을, 자연어 대신 참거짓이 명확한 논리식으로 바꾸어 엄밀하게 증명했다는 뜻입니다.
소프트웨어 검증 연구에서 프로그램의 정확성 조건을 명제논리로 형식화한 뒤 자동화 도구로 확인하는 절차를 설명하는 문장입니다.
조금 더 깊게 보면
명제논리 식이 특정 참·거짓 대입에서 항상 참이 되는지 판별하는 문제를 충족가능성 문제(SAT)라 부르며, 이는 계산복잡도 이론에서 NP-완전 문제의 대표 사례로 다뤄집니다. 명제논리는 개별 대상이나 "모든", "어떤" 같은 양화사를 표현할 수 없다는 한계가 있어, 이를 확장한 1차 술어논리(first-order logic)가 더 정교한 추론이 필요한 분야에서 사용됩니다.
주의할 점
명제논리의 AND·OR·NOT 기호는 컴퓨터 회로에서 쓰이는 논리 연산 AND/OR/NOT과 표기가 같지만, 명제논리는 참거짓을 가진 "문장"을 다루고 불 논리 연산은 전압 신호 같은 "값"을 다룬다는 차이가 있어 서로 혼동하지 않아야 합니다.