All about Programming Theories/SMT & Z3

명제 공식(Propositional Formula)

※ 이 글은 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은 거짓이다라는 논리적 관계를 나타낸다.