Herbrand 우주와 최소한의 herbrand 모델

나는 Herbrand universe, Herbrand Base and Herbrand Model of binary tree (prolog)에서 질문 한 내용을 읽었지만 주어진 질문과 약간 다른 질문이 있습니다. 확인과 같은 질문이 더 있습니다. 잘하면 혼란 스러울 것입니다. 의 Herbrand 우주에게Herbrand 우주와 최소한의 herbrand 모델

Up = {a, b, g(a), g(b), q(a, g(a)), q(a, g(b)), q(b, g(a)), q(b, g(b)), g(g(a)), g(g(b))...e.t.c}

Herbrand 기반 위의 프로그램에서

q(a, g(b)). 
q(b, g(b)). 
q(X, g(X)) :- q(X, g(g(g(X)))).

Bp = {q(s, t) | s, t E Up}

을

하자 P는 우리는 다음과 같은 사실과 규칙을 가지고 프로그램 등의 수

이제 내 질문에 대해 (용서 나는 나의 허 브란드 우주에서 요소로 q (a, g (a))를 포함 시켰지만, 실제로 그것은 q (a, g (b))를 나타낸다. 그것은 q (a, g (a))가 거기에 있다고 가정하지 않는다는 것을 의미합니까?
또한 Herbrand 모델이 Herbrand 기반의 하위 집합이기 때문에 어떻게 Herbrand 모델을 유도로 결정할 수 있습니까?

참고 : 나는 이것에 대한 많은 연구를 해왔으며, 일부 부분은 분명히 나에게 분명하다. 그러나 나는 아직도 커뮤니티에 대한 의견을 구하고 싶다. 고맙습니다.

출처

2014-01-27 Plaix

모델에 q(a,g(b)) 사실을 알리는 것으로부터 결론을 내릴 수 없습니다. 먼저 모델을 생성해야합니다.

모델을 확인하려면 사실 {q(a,g(b)), q(b,g(b))}으로 시작하고 규칙을 적용하여 확장하십시오. 그러나 귀하의 경우에는 위의 사실에 q(X,g(X)) :- q(X,g(g(g(X)))). 규칙의 오른쪽을 일치시킬 수있는 방법이 없습니다. 그러므로, 당신은 끝났습니다.

지금 우리의 집합을 확장하는 데 사용할 수있는 규칙

q(a,g(Y)) :- q(b,Y).

이 규칙을 상상한다. 사실, 인스턴스

q(a,g(g(b))) :- q(b,g(b)).

이 사용됩니다 q(b,g(b))가있는 경우, q(a,g(g(b)))을 체결. 오른쪽에서 왼쪽으로 규칙을 사용하고 있습니다. 그래서 우리는 얻습니다

{q(a,g(b)), q(b,g(b)), q(a,g(g(b)))}

고정 점에 도달.

이제 한 단계에서 생성 규칙 허용

q(X, g(g(g(X)))) :- q(X, g(X)).

(나는 더 이상 인스턴스화 규칙을 보여줄 것)를 제안 다른 예로서 취

{q(a,g(b)), q(b,g(b)), q(a,g(g(g(b)))), q(b, g(g(g(b))))}

을하지만이 아니다 결국, 규칙이 더 많은 것을 생산하기 위해 적용될 수 있기 때문에! 사실, 당신은 지금 무한한 모델을 가지고 있습니다!당신은 프롤로그에서 재귀 규칙을 이해하려고 할 때

 
{g(a,gⁿ⁺¹(b)), g(b, gⁿ⁺¹(b))}

이 오른쪽에서 왼쪽으로 읽기는 종종 많은 도움이 될 것입니다. 일반적으로 뒤틀림과 일반적인 통일을 고려해야하기 때문에 하향식 읽기 (왼쪽에서 오른쪽으로)는 종종 매우 어렵습니다.

출처

2014-01-27 20:26:52 false

설명해 주셔서 감사합니다. 나는 그것을 얻고 있다고 생각합니다. 예를 들어 규칙 q는 무엇입니까? (X, g (g (X))) : q (X, g (X)). 또한 Herbrand Universe가 맞습니까? – Plaix

@Plaix : Herbrand Universe는 모든 가능한 조합 일뿐입니다. – false

지금 알았어. 다시 감사합니다. – Plaix

귀하의 질문에 대해서는 "?를 Herbrand 모델은 Herbrand 기반의 부분 집합이기 때문에 또한, 내가 어떻게 유도에 의해 가장 Herbrand 모델을 결정합니까"

이

을

이

T_P(M) := { H S | S is ground substitution, (H :- B) in P and B S in M }

가장 적은 모델은 다음과 같습니다 :

inf(P) := intersect { M | M |= P }

것을하지 유의하시기 바랍니다 당신이 혼 조항의 설정 P, 명확한 프로그램이있는 경우

, 당신은 에게 프로그램 연산자를 정의 할 수 있습니다 명확한 프로그램의 모든 모델은 프로그램 운영자의 고정 점입니다. 예를 들어 완전한 herbrand 모델은 항상 이라는 프로그램입니다. 프로그램 P는 확실한 프로그램이 항상 일관성이 있음을 보여줍니다. 그러나 반드시 고정 점일 필요는 없습니다.

한편 프로그램 운영자의 각 고정 점은 확실한 프로그램의 모델입니다. 즉 당신이있는 경우 T_P (M) = M은, 다음 하나는 M 결론을 내릴 수 | = P. 그래서 좀 더 수학적 추론 (*) 하나가 가장 fixpoint도 이상 모델임을 발견 후 :

lfp(T_P) = inf(P)

그러나 우리는 계산의 종류에 따라 최소 모델을 결정할 수 있다고 말할 수 있도록 몇 가지 추가 고려 사항이 필요합니다. 즉 하나는 쉽게 혼 절은 자신의 몸에 한정사 FORALL하지 않기 때문에 프로그램 연산자, 즉 연속이다 체인의 무한한 조합을 유지하는 것이 관찰 :

그래서

union_i T_P(M_i) = T_P(union_i M_i)

이 다시 몇 가지 더 수학적 추론 후 (*) 하나는 우리가 반복을 통해 최소한의 고정 점을 계산할 수 있다는 것을 알게되고, 마녀는 단순한 유도를 위해 유도에 사용될 수 있습니다. 최소 모델의 모든 요소는 유한 깊이의 간단한 유도 있습니다

union_i T_P^i({}) = lpf(T_P)

안녕을

(*) 는 대부분의 경우이 책에 필요한 정확한 수학적 추론 에 대한 자세한 힌트를 찾을 수 있지만, 불행하게도 나는 기억하지 수있는 관련된 섹션 : 논리 프로그래밍, 존 와일리 로이드의
재단, 1984
http://www.amazon.de/Foundations-Programming-Computation-Artificial-Intelligence/dp/3642968287

출처

2014-02-02 17:55:37

Herbrand 우주와 최소한의 herbrand 모델

답변

관련 문제