통합 논리 계산실

논리 체계 선택

계산 결과는 같은 판정 언어로 표시합니다.

논리식 편집실열기

논리식·증명·관계도 자유 작성

한국어 · English · Français

언어 확장열기

한국어·영어·독일어·프랑스어·스페인어·이탈리아어·포르투갈어·네덜란드어·일본어·중국어

L1~L12 · 직접 분석·의미 검증·출력 복원

분해·복수 태깅·기호 공유·실행 계획

실행·증거·인증서·최소 반례

다중 작업·외부 비교·설명 품질·RC 검증

61~66단계 · v3.2 RC

외부 연동열기

TPTP·QMLTP·독립 증명 검사·모호성 병렬 실행

67~70단계 · v4.0 외부 검증 알파

대규모 운영열기

실행 시각화·영속 캐시·작업 큐·shard 배치

71~73단계 · v4.1 운영 확장 알파

v4 검증열기

감사·사람 검토·조정·RC 동결

74~80단계 · 사람 검토 운영·RC 동결

한국어 입력열기

문장 분석·형식화 후보·의미 분기·엔진 연결

25~29 + 58~59단계 · 의미 확인 강화

논리학 훈련실열기

형식화·증명·오류 진단·맞춤 재훈련

학습 엔진 1~22단계 · 대규모 운영·공개 베타·RC

진리값·반례·진리표·자연연역

양화사·동일성·유한 반모형

K·T·S4·S5 타블로·크립키 모형

LTLf X·F·G·U·진행 오토마톤

O 의무·P 허용·F 금지

참·미정·거짓의 3값 의미론

0~1 연속 진리도

사건 확률·조건부확률

고전·K3·퍼지·확률 비교

16단계 · 논리 틀과 크립키 세계도

양상논리 계산실

타블로·반모형 판정을 문제지·정답지·해설지와 크립키 세계도로 연결합니다.

K·T·S4·S5 자동 판정 결과를 논리 틀로 보내고, 반모형의 가능세계·접근관계·진리배정을 자동 세계도로 조판할 수 있습니다.

□P접근 가능한 모든 세계에서 P◇P접근 가능한 어떤 세계에서 PwRvw에서 v를 가능세계로 본다

예제

기호box / diamond / [] / <> / ~ / & / | / -> / <-> 입력도 지원합니다.

양상논리식

검사할 식

표준식□(P → Q) → (□P → □Q)

양상 깊이1명제문자P, Q

크립키 모형

가능세계접근관계 R한 줄에 한 접근관계씩 입력합니다.세계별 명제의 참인 곳목록에 없는 세계에서는 해당 명제가 거짓입니다.기준 세계

모형 계산 결과

`□(P → Q) → (□P → □Q)`

w0에서 참

K조건 충족

D조건 충족

T조건 밖

K4조건 충족

B조건 밖

S4조건 밖

S5조건 밖

반사 ×대칭 ×추이 ○연속(serial) ○유클리드 ○

w0참

접근 가능: w1

참인 명제: 없음

w1참

접근 가능: w1

참인 명제: P, Q

접근관계 R
R	w0	w1
w0	·	●
w1	·	●

명제 진리값
명제	w0	w1
P	F	T
Q	F	T

□는 접근 가능한 모든 세계를, ◇는 접근 가능한 적어도 한 세계를 검사합니다. 접근 가능한 세계가 하나도 없으면 □A는 참이고 ◇A는 거짓입니다.

15단계 · 타블로 증명과 반모형

먼저 라벨드 타블로로 증명을 시도하고, 열린 가지가 남으면 작은 크립키 반모형을 찾습니다.

논리 체계

접근관계에 추가 조건을 두지 않는 기본 정상 양상논리입니다.

반사적 프레임: 모든 세계가 자기 자신에 접근합니다.

반사적이고 추이적인 프레임입니다.

반사·대칭·추이를 모두 만족하는 동치관계형 프레임입니다.

논리 체계 선택

양상논리식

크립키 모형

□(P → Q) → (□P → □Q)

자동 증명·반모형 판정

`□(P → Q) → (□P → □Q)`