증명 또는 완전한 판정 근거가 확보되었습니다.
40단계 · v3 복합 논리 오케스트레이션 1차
통합 논리 계산실
v2.0 엔진은 동결하고, 그 위에서 여러 논리를 동시에 다루는 상위 계층을 시작했습니다.
36단계 v2.0 RC 계약은 그대로 보존합니다. 37~40단계에서는 복합 한국어를 의미 구간으로 분해하고, 한 구간에 여러 논리 체계를 태깅한 뒤 공통 기호·범위를 맞추고 병렬 실행 가능한 다중 엔진 작업 그래프를 만듭니다.
1한국어 분석→2논리식 후보→3의미 확인→4엔진 연결→5오류 진단→6형식 계산
통합 논리 계산실
논리 체계 선택
논리식 편집실열기
논리식·증명·관계도 자유 작성
한국어 · 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단계 · 비교·안전 변환반례·반모형·반례 시간흐름이 확보되었습니다.
전제들을 동시에 참으로 만드는 경우가 없습니다.
현재 계산 범위에서는 판정을 확정할 근거가 부족합니다.
교사용 시험 제작
논리 문제 자판기
명제논리·술어논리 증명 문제를 골라 시험지를 만들고, A/B/C 동급형과 교사용 정답·풀이를 A4로 출력합니다.
- 검증된 후보 20문제에서 선별·편집
- 문제은행·사용 이력·재출제 중복 관리
- 전 문항 재증명과 최종 PASS 뒤 인쇄
직접 계산하기
전제와 결론을 입력하세요
기호키보드 입력: ~ ! & | -> <->
전제
3개1
표준식P → Q
2
표준식Q → R
3
표준식P
결론
판정 대상표준식R
현재 시범판은 고전 명제논리의 진리값 의미론으로 판정합니다. 명제 문자는 최대 18개까지 검사합니다.
6단계 · 추가 검사
논리식 검사실
도출 계산과 별도로 두 식의 관계, 한 식의 성질, 여러 전제의 양립 가능성을 검사합니다.
01
동치 검사
두 식이 모든 진리값에서 같은지 확인합니다.
표준식P → Q
표준식¬P ∨ Q
02
식의 성질
항진식·모순식·우연식을 판정합니다.
표준식P ∨ ¬P
03
전제 일관성
여러 식을 동시에 참으로 만들 수 있는지 확인합니다.
1
표준식P → Q
2
표준식P
3
표준식¬Q
이 세 검사는 현재 명제 문자 16개까지 전수 계산합니다. 더 큰 식은 이후 SAT 기반 검사로 확장할 예정입니다.
현재 범위
자연어 해석과 형식 계산을 분리해서 정확하게
한국어·영어·독일어·프랑스어를 공통 의미 구조로 연결합니다.
복합 문장을 의미 구간으로 나누고 여러 논리 체계를 동시에 붙입니다.
공통 기호·범위를 맞춘 뒤 여러 엔진의 실행 순서와 병렬 작업을 구성합니다.
도출됨 · 도출되지 않음 · 전제 충돌 · 미확정
계산 결과를 문제용·정답용·해설용 조판으로 연결합니다.
각 논리 체계는 실제 브라우저·모바일·인쇄 검수 뒤 공개합니다.