% Description Logic
% updated June 28, July 04, 2001, by Thom Fruehwirth
% Terminological Reasoning (similar to KL-ONE or feature trees)
% Ph. Hanschke, DFKI Kaiserslautern, and Th. Fruehwirth
% 920120-920217-920413-920608ff-931210, LMU 980312

%% 20050124 adopted for exercises (Marc)

:- use_module( library(chr)).

% SYNTAX

% Basic operators
% T-box
:- op(1200,xfx,isa).					% concept definition
% concept terms
:- op(950,xfx,'::').					% A-Box membership and role-filler assertion
:- op(940,xfy,or).						% disjunction
:- op(930,xfy,and).					% conjunction
:- op(700,xfx,is).						% used in restricitions 
:- op(690,fy, nota).					% complement 		
:- op(650,fx, some).					% exists-in restriction
:- op(650,fx, every).				% value restriction

:- dynamic (isa)/2.

% TYPES
role_assertion((I,J)::R):- individual(I),individual(J), role(R).
membership_assertion(I::T):- individual(I), concept_term(T).

concept_definition((C isa T)):- concept(C), concept_term(T).

concept_term(S):- concept(S).
concept_term(S or T):- concept_term(S), concept_term(T).
concept_term(S and T):- concept_term(S), concept_term(T).
concept_term(nota S):- concept_term(S).
concept_term(some R is S):- role(R), concept_term(S).
concept_term(every R is S):- role(R), concept_term(S).

individual(I):- var(I) ; atomic(I).

role(R):- var(R) ; atomic(R).

concept(C):- var(C) ; atomic(C).

% CONSISTENCY CHECK
% A-box as constraint goals
% T-box asserted (concept definitions by isa- and sub-rules)

:- chr_constraint (::)/2, labeling/0.

% primitive clash
  I::nota Q, I::Q <=> false.		

% remove duplicates (both concepts and roles)
  I::C \ I::C <=> true.

% top
  I::top <=> true.

% complement nota/1

% nota-top
  I::nota top <=> false.

% nota-or
  I::nota (S or T) <=> I::(nota S and nota T).

% nota-and
  I::nota (S and T) <=> I::(nota S or nota T).

% nota-nota
  I::nota nota S <=> I::S.

% nota-every 
  I::nota (every R is S) <=> I::some R is nota S.

% nota-some 
  I::nota (some R is S) <=> I::every R is nota S.

% conjunction
  I::S and T <=> I::S, I::T.

% exists-in restriction
  I::some R is S <=> role(R) | (I,J)::R, J::S.	% generate witness

% value restriction
  I::every R is S, (I,J)::R ==> J::S.

% disjunction (is delayed as choice)
labeling, (I::S or T) # Id <=>
	(I::S ; I::T),
	labeling
    pragma passive(Id).

% T-box unfolding using concept definition
% if you use cyclic concepts (recursion), replace rules below by propagation rules
  I::C <=> (C isa T) | I::T.
  I::nota C <=> (C isa T) | I::nota T.