P/1 · Q/1
통합 논리 계산실
논리 체계 선택
논리식 편집실열기
논리식·증명·관계도 자유 작성
한국어 · 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단계 · 비교·안전 변환12단계 · 관계 검사와 논리 틀 연결
술어논리 계산실
관계·동일성 계산 결과를 전용 검사와 수업·시험용 조판으로 연결합니다.
동일성 치환과 관계 성질 추론을 유지하면서, 유한 관계의 반사·대칭·추이를 직접 검사하는 전용 화면과 문제용·정답용·해설용 논리 틀을 연결합니다.
∀x(P(x) → Q(x))∃x(P(x) ∧ R(x, a))R(a, b)a = b직접 입력하기
전제와 결론의 구조를 확인하세요
기호forall / exists / ~ / & / | / -> / <-> 도 입력할 수 있습니다.
전제
2개1
표준식∀x(P(x) → Q(x))
변수닫힌 식 · 속박 x
2
표준식P(a)
변수닫힌 식
결론
구조 분석표준식Q(a)
변수닫힌 식
현재 판정 원칙
증명을 찾으면 “도출됨”, 전제는 참이고 결론은 거짓인 반모형을 찾으면 “도출되지 않음”으로 확정합니다. 둘 다 찾지 못하면 미확정으로 남깁니다.
구조 분석 완료
논증 전체의 논리 언어
없음
a
속박: x
표준형
∀x(P(x) → Q(x))P(a)
∴
Q(a)구문 구조(AST) 보기
{
"premises": [
{
"type": "forall",
"variable": "x",
"body": {
"type": "group",
"start": 2,
"end": 16,
"expression": {
"type": "implies",
"left": {
"type": "predicate",
"name": "P",
"args": [
{
"type": "term-variable",
"name": "x",
"start": 5,
"end": 6
}
],
"start": 3,
"end": 7
},
"right": {
"type": "predicate",
"name": "Q",
"args": [
{
"type": "term-variable",
"name": "x",
"start": 13,
"end": 14
}
],
"start": 11,
"end": 15
},
"start": 3,
"end": 15
}
},
"start": 0,
"end": 16
},
{
"type": "predicate",
"name": "P",
"args": [
{
"type": "constant",
"name": "a",
"start": 2,
"end": 3
}
],
"start": 0,
"end": 4
}
],
"conclusion": {
"type": "predicate",
"name": "Q",
"args": [
{
"type": "constant",
"name": "a",
"start": 2,
"end": 3
}
],
"start": 0,
"end": 4
}
}현재 지원
동일성 추론 + 관계 성질 공리 인식 + 유한 관계 검사 + 논리 틀 전송
입력 규칙
술어는 대문자, 개체상항·함수는 소문자, 변수는 x·y·z·u·v·w 계열을 사용합니다.
관계 전용 검사