t0참
참인 명제: P
통합 논리 계산실
논리 체계 선택
논리식 편집실열기
논리식·증명·관계도 자유 작성
한국어 · 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단계 · 비교·안전 변환21단계 · LTLf 오토마톤 전이 그래프
시간논리 계산실
LTLf 오토마톤의 잔여식 상태와 진리배정 전이를 실제 그래프로 시각화합니다.
자동 판정 결과에서 q0·q1… 잔여식 상태, 상태 사이의 진리배정 전이, 거짓 종착 ⊥, 반례 종료 상태를 그래프로 확인하고 논리 틀에도 같은 도식을 사용합니다.
X P다음 시점에서 PF P현재부터 끝까지 언젠가 PG P현재부터 끝까지 항상 PP U QQ가 올 때까지 P가 유지
예제
기호next / eventually / always / until / ~ / & / | / -> / <-> 입력도 지원합니다.
시간논리식
표준식G(P → F Q)
시간 깊이2명제문자P, Q
유한 시간흐름
LTLf 계산 결과
G(P → F Q)
t1참
참인 명제: Q
t2참
참인 명제: P
t3참
참인 명제: Q
| 식 | t0 | t1 | t2 | t3 |
|---|---|---|---|---|
G(P → F Q) | T | T | T | T |
X마지막 상태에서는 거짓F현재를 포함한 미래에 한 번이라도 참G현재를 포함한 남은 모든 상태에서 참U오른쪽 식의 실제 미래 증인이 필요
현재 계산은 유한 시간흐름 LTLf 의미론을 사용합니다. X는 마지막 상태에서 X가 거짓인 의미, U는 Q가 실제로 나타나야 하는 U 의미로 해석합니다.
20단계 · LTLf 오토마톤 판정
자동 타당성·반례 판정
진행 오토마톤으로 모든 유한 시간흐름을 상태공간으로 압축해 검사하고, 한계에 걸리면 기존 제한된 길이의 반례 탐색으로 보조합니다.
X · 다음
마지막 상태에는 다음 상태가 없으므로 X P는 거짓입니다.
F · 언젠가
현재 시점부터 시간흐름 끝까지 한 번이라도 참이면 참입니다.
G · 항상
현재 시점부터 시간흐름 끝까지 모든 상태에서 참이어야 합니다.
U · ~할 때까지
오른쪽 식이 실제로 나타나고, 그 전까지 왼쪽 식이 계속 참이어야 합니다.