사용설명서 - Logic Tutor

Logic Tutor 설명서

이 웹 앱은 기호 논리학을 공부한 학생들이 기호 논리학 증명을 쉽고 효과적으로 연습할 수 있도록 도와주는 앱입니다. 현재는 명제 논리 증명만을 연습할 수 있습니다. 계속적으로 개발하여 양화 논리 증명까지 연습하는 것을 목표로 하고 있습니다. 이 기능은 현재 개발 중입니다. 내년 3월 전에는 양화 논리 증명도 가능하도록 노력하고 있습니다.

사용법

전반적인 사용법은 어렵지 않습니다. 단 이 앱을 사용하기 위해서는 아래와 같이 두 가지 것이 필요합니다. 이 두 가지가 있으면 이 이 앱을 사용하실 준비가 된 것입니다. 사용 방법과 사용하면서 주의할 점도 아래 적어 두었습니다. 한 번씩 읽어 보시면, 이 앱을 어렵지 않게 사용하실 수 있습니다.

본 앱을 사용하기 위해서 필요한 것들

이메일 주소

로그인하는데 필요합니다. 로그인을 하는 이유는 앱이 사용자의 증명 진행 과정과 풀었던 문제 목록을 사용자의 웹 브라우저에 암호화해서 저장하고 이를 토대로 작동하기 때문입니다. 따라서 제대로 작동하기 위해서는 로그인이 필수적으로 필요합니다. 이메일 주소만 필요하고 비번 같은 것은 입력할 필요도 없습니다.

기본적인 기호 논리 증명 방법에 대한 이해

이 앱은 기호 논리 증명 방법을 연습하는데 최적화되어 있습니다. 따라서 이 앱을 이용하기 위해서는 사용자가 기본적인 기호 논리 증명 방법을 알고 있어야 합니다. 현재는 명제 논리 증명에 대한 기본적인 지식만 있으면 됩니다.

이 앱을 가지고 추론 연습하기!

무턱대고 하는 것보다 다음 내용을 살펴보면 조금 더 편리하게 연습하실 수 있습니다.

  • 어떤 것을 추론하고자 하는가?

    주어진 전제를 가지고 결론을 도출하려면 무엇이 필요한지 생각합니다.

  • 추론하고자 하는 것을 추론하기 위해서 필요한 규칙이 있는가?

    현재 주어진 것들을 가지고 추론하고자 하는 것을 도출하기 위한 규칙이 있는지 확인합니다.(이 메뉴얼 하단부에 있습니다!)

  • 그 규칙에 필요한 근거가 지금 있는가?

    위에서 생각한 규칙에 대한 근거들을 지금 있는지 없는지 확인합니다. 있으면 그 근거과 규칙을 가지고 맞는 추론인지 검사합니다. 만약 근거가 없으면, 그 근거를 추론하기 위한 법칙이 있는지 살펴봅니다.

  • 앞에서 알아낸 것을 입력한다.

    우선 위에서 알아낸 규칙에 필요한 근거(들) 번호를 근거에 필요한 근거 줄 번호 입력에 입력합니다. 번호 입력을 하는 방법은 아래 주의에 상세히 썼습니다. 참고하세요! 다음으로 위에서 알아낸 규칙 이름을 추론 입력 란에 있는 추론 규칙, 동치 규칙, 가정에서 찾아서 선택합니다. 그런 다음 자신이 이 중 어떤 법칙을 선택했는지, 규칙 선택 아래에 있는 선택 버튼 중 하나를 누릅니다.

  • `P`, `not P` 같은 단순명제, 부정 명제를 소중히!

    위와 같은 명제가 복잡한 명제를 분해하고 조립해서 결론을 추론해 가는 것이 가장 쉽고 좋은 방법 중 하나 입니다.

자신의 추론을 앱에 입력하는 법

기본적으로 논증을 입력하는 방법은 다음과 같습니다. 입력한 다음 제출하면 이를 적절하게 논리식에 바꿔 화면에 보여줍니다. 참고하기 바랍니다.

입력 방법 이름 화면표시 주의할 점
-P 부정문 `not P` 키보드에서 -
P&Q 연언문 `P & Q` 키보드에서 &
PvQ 선언문 `P vv Q` 알파벳 'V'의 소문자, v
P->Q 조건문 `P -> Q` 키보드에서 -와 >
P<->Q 쌍조건문 `P harr Q` 키보드에서 <, - 그리고 >

주의!

규칙 설명

명제 논리에서 증명을 하는데 필요한 규칙은 크게 전반적인 사용법은 어렵지 않습니다.

추론 규칙(Rule of inference)

전건긍정식 (Modus Ponens)
`{:[P -> Q],[P],[:. Q]:}`
후건부정식(Modus Tollens)
`{:[P->Q],[not Q],[:.not P]:}`
조건삼단논법 (연쇄논법)
`{:[P->Q],[Q->R],[:.P->R]:}`
∨ 제거
`{:[PvvQ],[not P],[:.Q]:}`
∨ 도입
`{:[P],[:.PvvQ]:}`
∧ 도입(& 도입)
`{:[P],[Q],[:.P^^Q]:}`
∧ 제거(& 제거)
`{:[P^^Q],[:.P]:}`
조건 증명
`{:[|~P \qquad n],[| vdots],[|__Q  \qquad m],[P -> Q \qquad n\ ~\ m ]:}`
귀류법
`{:[|~P \qquad n],[| vdots],[|__ Q & not Q \qquad m],[not P \qquad n\ ~\ m ]:}`
↔ 도입
`{:[P->Q],[Q->P],[:.P harr Q]:}`
↔ 제거
`{:[P harr Q],[:.P -> Q]:}`
`{:[P harr Q],[:.Q -> P]:}`
양도 논법
`{:[P vv Q],[(P->R) ^^ (Q->R)],[:.R]:}`

Rule of replacement

여기서 '⇔' 의 의미는 논리 추론에서 서로 서로 바꿔쓸 수 있다는 의미입니다.

실질 함축(Material implication), 동치
`P->Q hArr not P vv Q`
이중부정
`not not P hArr P`
대우(Transposition)
`P -> Q hArr not Q -> not P`
드모르강의 법칙(드모르강:De Morgan's laws)
`{:[not(PvvQ) hArr not P ^^ not Q],[not(P^^Q) hArr not P vv not Q]:}`
교환법칙
`{:[PvvQ hArr QvvP],[P^^Q hArr Q^^P]:}`
결합법칙
`{:[Pvv(QvvR) hArr (PvvQ)vvR],[P^^(Q^^R) hArr (P^^Q)^^P]:}`
분배법칙
`{:[Pvv(Q^^R) hArr (PvvQ)^^(PvvR)],[P^^(QvvR) hArr (P^^Q)vv(P^^R)]:}`
항진(Tautology)
`{:[PvvP hArr P],[P^^P hArr P]:}`