Injin Woo
禹仁眞
[ KO | EN ]
← 홈으로
∀
논리 타블로 & 자연연역 증명기
Logic Tableau & Fitch Natural Deduction (Priest · Garson · OLP)
교과서 표기 (Textbook Notation)
Priest — An Introduction to Non-Classical Logic
Garson — Modal Logic for Philosophers
Open Logic Project — Boxes and Diamonds
논리 체계 선택
고전 논리 — 명제 + 1차 (Classical, propositional + first-order)
기본 양상 논리 K (Basic Modal Logic K)
비정상 양상 논리 N / S2 / S3 (Non-normal, Priest Ch. 4)
L / S0.5 (Lemmon non-normal, Priest §4.4a)
자유 논리 — 내부 영역 E, 존재 술어 E! (Priest Ch. 13)
양화 양상 CK — 상수 영역 (Priest Ch. 14, Barcan)
시제 논리 Kᵗ / CKᵗ — [F] [P] ⟨F⟩ ⟨P⟩ (Priest §3.6a, §14.6)
양화 비정상 CL — 상수 영역 L (Priest Ch. 18)
양화 비정상 CN — 상수 영역 N (Priest §18.5)
양화 비정상 VL — 가변 영역 L (Priest §18.5)
양화 비정상 VN — 가변 영역 N (Priest §18.5)
양화 양상 VK — 가변 영역, 존재 술어 E! (Priest Ch. 15)
퍼지 논리 Łℵ — 연속값 (Priest Ch. 11, 검사기)
퍼지 논리 L(Gödel) — t-norm Min (Priest §11.7a)
퍼지 논리 L(Product) — t-norm 곱 (Priest §11.7a)
조건문 논리 C (Conditional Logic C, Priest Ch. 5)
조건문 논리 C+ (Conditional Logic C+)
조건문 논리 S — Lewis 구 모형 (의미론 검사기)
조건문 논리 C1 — S + 강한 중심화 (Lewis)
조건문 논리 C2 — S + 유일성 (Stalnaker, CEM)
직관주의 논리 (Intuitionistic Logic)
K4 — FDE + 세계
N4 — K4 + 비정상 세계
K* — Routley star
N* — star + 비정상 세계
B — 관련성 논리 (3항 관계)
K3 — 강한 클레이니 (gap)
LP — 역설의 논리 (glut)
Ł3 — 우카시에비치
RM3
FDE — 1차 함의 (gap+glut)
접근성 관계 조건 (Priest §3.2.3)
ρ 반사성 — T: □A→A
σ 대칭성 — B: A→□◇A
τ 추이성 — 4: □A→□□A
η 연장성 — D: □A→◇A
υ 보편성 — S5
NC 부정성 제약 — 참 원자문장의 항은 존재 (Priest §16.3, VK·CKᵗ)
CI 우연적 동일성 — IIR 없음, 아바타 의미론 (Priest §17.2)
자유 양화 — 내부 영역 E 위에서 양화, 존재 술어 E! (Priest §22.4)
관련성 체계 (Priest §10.4a.12 — 프레임 제약 C8–C16)
B — 제약 없음
BX = B + C13 (배중률)
DW = B + C8
DWX = DW + C13
TW = DW + C9 + C10
TWX = TW + C13
T = TW + C11 + C14
RW = TW + C12
R = RW + C11 (결정 불능)
RWK = RW + C15
RM = R + C16
Rwww (모든 세계, 문제 3)
T9–T12 는 새 세계를 만들어 R 계열은 종료 보장이 없다 — 반복 심화 + 4초 예산, 부당성은 Sugihara 행렬·RM3 로 보조 판정.
전제 및 결론 수식 입력
[ 지우기 ]
[ 복사 ]
[ 무작위 예제 ]
⊢
증명 생성 (Tableau & Fitch)
[ 체계 비교 ]
예제 프리셋
풀어본 문제
0
[ 초기화 ]
[ 문제집 모드 ]
대기 중 (Ready)
타블로 트리
자연연역 (Fitch)
ASCII 트리
LaTeX
단계 추적
규칙 참조
수동 구성
반례 구성
[ ＋ 확대 ]
[ － 축소 ]
[ ↺ 초기화 ]
[ ◀ ]
– / –
[ ▶ ]
[ 전체 ]
[ 보기: 박스형 ]
[ 연습 모드 ]
[ ND 빈칸 ]
[ ND 작성 ]
[ 인쇄·PDF ]
[ 인증서 JSON ]
[ TPTP ]
[ SVG 저장 ]
[ 가져오기 → 판정 ]
[ 복사 ]
[ 검사 ]
[ 전제 채우기 ]
[ 엔진 증명 보기 ]
[ ASCII 복사 ]
[ LaTeX 복사 ]