※ 이 글은 chatGPT를 기반으로 작성한 글입니다.
※ Coursera의 Automated Reasoning: satisfiability 강의를 기반으로 작성한 글입니다.
① 명제 공식(propositional formula)은 수리논리학에서 상요되는 기호와 연산자들로 구성된 식이다.
㉠ 주로 명제 논리에서 상용되며, 간단한 명제들과 논리 연산자를 사용하여 복잡한 명제를 구성한다.
② 명제 공식의 기본 구성 요소는 다음과 같다.
㉠ 원자 명제(Atomic Propositions)는 가장 기본적인 명제로, 추가적인 분해가 불가능하다. 예를 들어 P, Q, R과 같은 단일 문자들이 사용될 수 있다.
㉡ 논리 연산자(Logical Operatos)는 기본 명제들을 결합하거나 변형하는 데 사용된다.
ⓐ 부정(NOT, negoation, ¬) 논리 연산자는 명제의 진리값(truth value)을 반대로 변경한다.
ⓑ 논리곱(AND, conjunction, ∧) 논리 연산자는 두 명제가 모두 참일 때 참이 되는 명제를 만든다.
ⓒ 논리합(OR, disjunction, ∨) 논리 연산자는 두 명제 중 적어도 하나가 참일 때 참이 되는 명제를 만든다.
ⓓ 조건(If-then, implication →) 논리 연산자 또는 함의는 첫 번째 명제가 참이고 두 번째 명제가 거짓인 경우를 제외하면 모두 참이 되는 명제를 만든다.
ⓔ 쌍조건(Bi-conditional, bi-implicatino, ↔) 논리 연산자 또는 동치는 두 명제가 같은 진리값을 가질 때 참이 되는 명제를 만든다.
㉢ 괄호는 연산자의 우선 순위를 정하는 데 사용된다.
③ 예를 들어 명제 공식 \((P ∧ Q) → ¬R\) 는 P와 Q가 모두 참이면 R은 거짓이다라는 논리적 관계를 나타낸다.
'All about Programming Theories > SMT & Z3' 카테고리의 다른 글
SAT(Boolean Satisfiability Problem) (1) | 2024.01.04 |
---|---|
SAT(Boolean Satisfiability Problem)와 SMT(Satisfiability Modulo Theories) (1) | 2023.12.23 |