[[분류:논리학]][[분류:언어학]][[분류:컴퓨터 공학]]
[include(틀:이론 컴퓨터 과학)]
[목차]
== 개요 ==
형식 언어(形式言語, formal language)는 형식언어이론(形式言語理論,formal language theory)을 알파벳 및 특수기호를 포함하는 예약된 기호열 집합에 기반한 결합(추론 또는 연산)으로서의 형식 언어 문법에 관한 논리적 이론의 구현이라고 정의해 본다면 형식 언어를 정의하는 방법에는 구조와 범위가 무결성에 기반하여 명확하게 규정되고 정의된 인공 언어를 말한다. 자연 언어에서의 [[생성 문법]] 등과 컴퓨터 [[프로그래밍 언어]]의 [[오토마타]](automata) 등이 있다.

[[논리학]], [[언어학]], [[수학]], [[컴퓨터과학]] 등에서 주로 다룬다.

== 언어 형식 ==
인공 언어인 형식 언어에서 언어 형식은 자연 언어에서 문법에 해당하는 것으로 볼 수 있으며, 이를 통해서 형식 언어를 정의함으로써 구조와 범위가 무결성을 갖도록 설계할 수 있다.

=== 퍼스트 오더 로직 ===
[[퍼스트 오더 로직]](1st order logic) 또는 1차 술어논리(first-order predicate logic)의 주요 원리중 하나이자 형식 언어에서의 [[드모르간 법칙]]의 예
> 논리학 : [math( \neg (\text{부정}), \lor (\text{논리합}), \land  (\text{논리곱}) )]
> [math(\neg (p \lor q) = \neg p \land \neg q)] [br]  [math(\neg (p \land q) = \neg p \lor \neg q)]

=== 기호논리학의 예 ===
기호논리학(Symbolic Logic) 또는 1차 술어 논리(first-order predicate logic)에서의 추론 형식의 예
|| 추론 형식 || 논리식 || 예 ||
|| F1 || [[삼단논법]] || 가언([math(\to)], [math(\supset)]), 선언([math(\lor)]), 연언([math(\land)]), [[정언 명제]]([math(\subset)]) 등 [[명제논리]] ||
|| F2 || 드모르간의 법칙 || [math(\neg (p \lor q) = \neg p \land \neg q)][br][math(\neg (p \land q) = \neg p \lor \neg q)] ||
|| F3 || 단순화 논리 || [[이중부정]]([math(\neg\neg)]) ,논리곱 논법 등 ||
|| F4 || 양화사 논리 || 존재양화사 [math(\exist)] (existential quantifier)[br]보편양화사 [math(\forall)] (universal quantifier)  ||
|| F5 || 등호 논리 || [math(g=m)] ||

기호논리(Symbolic Logic)의 추론 예
|| 자연언어 || 형식 언어 || 추론 형식 ||
|| 만일 __비가 온다__([math(\rm A)])면, __소풍을 가지__([math(\rm B)]) 않는다. || [math(\rm A \to \neg B)] || F1 (가언 명제) ||
||  소풍을 가지 않는다면, 우리는 __학교에 가야__([math(\rm C)])된다. || [math(\rm \neg B \to C)] || F1 (가언 명제) ||
|| 비가 오지 않는다([math(\rm \neg A)]), 그리고 우리는 __학교에 가지__([math(\rm \neg C)]) 않는다. || [math(\rm \neg A \land ¬C)] || F1 (연언 명제), F3(단순화 논리) ||
|| 비가 온다([math(\rm A)]) 또는 우리는 학교에 간다([math(\rm C)]) || [math(\rm \neg \left ( \neg A \lor \neg C \right ) = A \lor C)] || 이중부정(F3),드모르간의 법칙(F2), 등호 논리(F5) ||
|| 비가 오지 않는다([math(\rm \neg A)]) 우리는 소풍을 간다([math(\rm C)]) || [math(\rm A \subset C)] || 정언 명제 (F1, 결론) ||