통합 논리 계산실

논리 체계 선택

계산 결과는 같은 판정 언어로 표시합니다.
논리식 편집실열기

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

한국어 · English · Français
언어 확장열기

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

L1~L12 · 직접 분석·의미 검증·출력 복원
복합 논리열기

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

37~46단계 · v3.0 RC
실행 오케스트레이터열기

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

47~60단계 · v3.2 알파
배치 실행열기

다중 작업·외부 비교·설명 품질·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 금지

30단계 · D 직렬 프레임
다치논리 K3현재

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

32단계 · 첫 확장 플러그인
퍼지논리열기

0~1 연속 진리도

33단계 · Zadeh + KD
확률논리열기

사건 확률·조건부확률

34단계 · 명시 확률모형
교차 논리열기

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

35단계 · 비교·안전 변환

32단계 · 첫 확장 플러그인

다치논리 K3 계산실

참과 거짓 사이에 ‘미정’을 둔 3값 논리를 계산합니다.

강한 클레이니 K3는 T·U·F 세 진리값을 사용합니다. 현재 시범판은 T만 지정값으로 두며, 모든 3값 배정을 전수 검사해 도출과 반례를 판정합니다.

T참U미정F거짓지정값T만 도출 판정에 사용

K3 논증

전제와 결론

강한 클레이니 3값 의미론
부정

¬T=F · ¬U=U · ¬F=T

논리곱

두 값 가운데 더 낮은 값을 취합니다.

논리합

두 값 가운데 더 높은 값을 취합니다.

조건문

A→B는 ¬A∨B로 계산합니다.