Files

T

Antigravity Agent 504fd5fb42 [G1-Sync] Manual knowledge update

2026-05-10 22:08:15 +09:00

4.6 KiB

Raw Blame History

id, title, category, status, canonical_id, aliases, duplicate_of, source_trust_level, confidence_score, verification_status, tags, raw_sources, last_reinforced, github_commit, tech_stack

title

Logic

매 한 줄

"매 추론을 형식화한다". 명제·술어·양상·퍼지 논리는 truth-preserving 변환의 규칙이며, AI에서는 Prolog/ASP/SMT/Neuro-symbolic으로 LLM의 hallucination을 제약한다.

매 핵심

매 분류

Propositional: ∧ ∨ ¬ → ↔, 진리표.
First-order (predicate): ∀ ∃, 술어, 함수 — 표현력 ↑.
Higher-order: 술어 자체를 정량화.
Modal: □ ◇ (필연/가능) — 시간/지식/의무.
Fuzzy: [0,1] 진리값 — 모호성.
Linear / substructural: 자원 회계.
Probabilistic: Bayesian + 논리 (Markov logic, ProbLog).
Description Logic: OWL, ontology.

매 핵심 결과

Soundness/Completeness (Gödel): 1차 논리 완전.
Incompleteness (Gödel): 산술 포함 시 불완전.
Cut elimination (Gentzen): 증명 정규화.
Curry-Howard: 증명 = 프로그램, 명제 = 타입.
Resolution (Robinson): 자동 정리 증명 기반.

매 AI 응용

Prolog: 백트래킹 기반 논리 프로그래밍.
ASP (Answer Set Programming): clingo, 조합 탐색.
SAT/SMT (Z3): 검증, 합성.
Knowledge Graph + reasoner: SPARQL, OWL.
Neuro-symbolic: LLM + symbolic verifier (e.g., Lean/Z3 augmented).
LLM tool use: Claude가 SMT/Lean 호출해 hallucination 차단.

💻 패턴

Pattern 1 — Prolog 사실/규칙

parent(alice, bob).
parent(bob, carol).
ancestor(X, Y) :- parent(X, Y).
ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).
?- ancestor(alice, carol).  % true

Pattern 2 — Z3 (SMT)

from z3 import *
x, y = Ints('x y')
solve(x + y == 10, x - y == 4)  # x=7, y=3

Pattern 3 — ASP (clingo)

% N-queens
{queen(1..n, 1..n)}.
:- queen(R,C1), queen(R,C2), C1 != C2.
:- queen(R1,C), queen(R2,C), R1 != R2.
:- queen(R1,C1), queen(R2,C2), |R1-R2| == |C1-C2|, R1!=R2.

Pattern 4 — Fuzzy (scikit-fuzzy)

import skfuzzy as fuzz
warm = fuzz.trimf(x, [15, 22, 30])
cool = fuzz.trimf(x, [0, 10, 20])

Pattern 5 — Description Logic (OWL/Pellet)

:Person rdf:type owl:Class .
:hasParent rdf:type owl:ObjectProperty ;
           rdfs:domain :Person ; rdfs:range :Person .
:Mother rdfs:subClassOf [owl:intersectionOf (:Person :Female)] .

Pattern 6 — Lean 4 (proof assistant)

theorem add_comm (a b : Nat) : a + b = b + a := by
  induction a with
  | zero => simp
  | succ n ih => simp [Nat.succ_add, ih]

Pattern 7 — Neuro-symbolic with LLM

# LLM proposes plan → Z3 verifies constraints
plan = claude.generate(problem)
solver = Solver()
solver.add(constraints_from(plan))
if solver.check() == sat:
    return plan

매 결정 기준

문제	도구
결정 가능, 작은	Truth table / SAT (MiniSat, Glucose)
산술 포함	SMT (Z3, CVC5)
조합 탐색 / 일정	ASP (clingo)
KB + 추론	Prolog 또는 Datalog
Ontology / Web	OWL + reasoner
정리 증명	Lean, Coq, Isabelle
모호성	Fuzzy / probabilistic
LLM hallucination 검증	LLM + Z3/Lean 결합

기본값: 작으면 SAT, 산술이면 Z3, 검증이면 Lean.

🔗 Graph

부모: Mathematics, Reasoning
변형: Propositional-Logic, First-Order-Logic, Modal-Logic, Fuzzy-Logic
응용: Prolog, Answer-Set-Programming, SAT-Solver, SMT-Solver, Neuro-Symbolic-AI
Adjacent: Type-Theory, Curry-Howard, Knowledge-Graph, Theorem-Proving

🤖 LLM 활용

언제:

Z3/Prolog/ASP 인코딩 작성.
논리식 ↔ 자연어 번역.
증명 outline 초안.

언제 X:

정확한 정리 증명 (Lean/Coq 검증 필수).
Soundness 보장 주장 (도구로 확인).

❌ 안티패턴

LLM에 직접 SAT 풀리기 (불완전).
First-order에서 결정 가능성 가정.
Fuzzy logic을 확률과 혼동.
Closed-world (Prolog) ↔ open-world (OWL) 구분 무시.
Neuro-symbolic을 만능으로 (병목은 인코딩).

🧪 검증 / 중복

Verified. Z3 4.13, Lean 4, clingo 5 기준. 신뢰도 A.

🕓 Changelog

날짜	변경
2026-05-08	Phase 1
2026-05-10	Manual cleanup

4.6 KiB Raw Blame History Unescape Escape