OWL Full이 결정 불가능한 이유를 다 둘러 보았습니다. 이해하기 쉬운 예제를 발견하지 못했습니다.왜 OWL Full은 결정 불가능합니까?
나는 그것이 "Entailment Closure"때문인 것으로 밝혀졌으며 OWL Full이 Properties이고 또한 동시에 Individual 인 클래스를 가질 수 있다고 설명하는 진술을 발견했습니다.
그러나 이러한 진술 간의 관계를 이해하지 못합니다.
OWL Full이 결정 불가능한 이유를 다 둘러 보았습니다. 이해하기 쉬운 예제를 발견하지 못했습니다.왜 OWL Full은 결정 불가능합니까?
나는 그것이 "Entailment Closure"때문인 것으로 밝혀졌으며 OWL Full이 Properties이고 또한 동시에 Individual 인 클래스를 가질 수 있다고 설명하는 진술을 발견했습니다.
그러나 이러한 진술 간의 관계를 이해하지 못합니다.
질문에 많은 의미가 있으며 대답하기 쉽지 않습니다. 또한 OWL-DL과 OWL-Full의 차이점은 수정되지 않았습니다. 처음에는 OWL에서 제한된 것이 나중에 허용되었으며, 가장 일반적인 경우는 punning입니다.
그러나 기본적으로는, 아이디어는 예 또는 전혀에 답하고 또는 에 "무한는"아직를 모르는 모르는 을 피할 수있는 추론을 쓸 수 있어야하는 것입니다. 이 30 분 lecture on Tableaux Algorithm와 어쩌면 몇 가지 다른 것들이 전과 후에 같은 코스에서 도움이 될 것입니다.
그런데 계산 동점 종결의 결정 불가능 성과 불가능 성은 the same thing이 아닙니다.
나를 위해 OWL 전체 결정 불가능 성을 이해하는 가장 쉬운 방법은 OWL 2 DL 글로벌 제한, 특히 간단한 역할 부분 인 https://www.w3.org/TR/owl2-syntax/#Global_Restrictions_on_Axioms_in_OWL_2_DL을 살펴 보는 것입니다. 이러한 제한이 제거 된 OWL 2 DL만으로는 결정할 수 없으므로이를 포함하는 OWL 2 Full이 결정됩니다.
이 슬라이드 http://www.cs.man.ac.uk/~horrocks/Slides/ijcai-slides.pdf에는 위의 제한 사항을 완화하면 (일부) 논리를 결정할 수없는 링크가 포함되어 있습니다.
OWL Full과 OWL DL의 수학적 생성자 집합이 동일하지만 OWL Full은 이러한 생성자의 사용에 대한 제한이 없습니다. OWL Full이 결정 불가능한 이유를 확인하기 위해 전이 속성 사용에 대한 제한이 없다고 생각하십시오.
다음은 OWL 2 Full이 결정 불가능한 이유를 이해하는 데 충분한 예제입니다. 이것은 Russel's paradox과 관련이 있습니다. 이 논리는 결정 불가능하지 않습니다
:IsInstanceOfItself a :IsIntanceOfItself .
이것은 또한 RDF/RDFS에서 가능하지만 :
는 OWL 전체에서는 인스턴스로 자신을 가진 클래스를 정의 할 수 있습니다. undecidability로 인도하는 것은 OWL 2 Full에서 역설적 인 클래스를 정의 할 수 있다는 사실입니다. 당신은 인스턴스로 자신이 클래스의 클래스 정의 할 수 있습니다 : 이:HaveThemselvesAsInstance
rdfs:subClassOf [
a owl:Restriction;
owl:onProperty rdf:type;
owl:hasSelf true
] .
그런 다음 클래스를 정의 할 수 있습니다 그 인스턴스로 자신이없는 :
:DoNotHaveThemselvesAsInstance
owl:equivalentClass [ owl:complementOf :HaveThemselvesAsInstance ] .
을 이제 우리가 질문을 할 수있다 :DoNotHaveThemselvesAsInstance
자체의 인스턴스? 그것이 사실이라고 가정 해보십시오. 그 다음 :
:DoNotHaveThemselvesAsInstance a :DoNotHaveThemselvesAsInstance .
가 참입니다.따라서 :DoNotHaveThemselvesAsInstance
은 rdf:type
속성과 자체 관계가없는 클래스에 있다는 정의를 준수합니다. 그래서 가정은 잘못되었습니다. 따라서 :DoNotHaveThemselvesAsInstance
은 그 자체가 rdf:type
인 클래스를 보완해야합니다. 따라서 인스턴스는 :DoNotHaveThemselvesAsInstance
이어야합니다. 따라서 위의 가정 된 관계가 유지되어야합니다. 초기 단계로 돌아갑니다. 결과적으로 위에 정의 된 클래스를 정의하는 온톨로지에 대한 모델은 존재할 수 없다. 따라서 클래스 자체가 인스턴스가 아닌 클래스는있을 수 없습니다. 아마도 모든 수업은 스스로를 인스턴스로 가지고있을 것입니다. 그러나 일부 클래스가 자신의 인스턴스가 아닌 온톨로지 모델이 있습니다. 그래서 ... OWL 2 Full은 정말 망했어?