begin_problem(Cheese_lovers_example).
list_of_descriptions.
  name({* Cheese lovers example *}).
  author({* Renate Schmidt *}).
  status(unsatisfiable).
  description({* A description logic example. *}).
end_of_list.

list_of_symbols.
functions[   
    (adam,0),  (bob,0),  (cauliflower,0),  (cheddar,0)
].
predicates[  
    (plant,0),        (Plant,1),       (cheese,0),        (Cheese,1),
    (food,0),         (Food,1),        (person,0),        (Person,1),
    (vegetarian,0),   (Vegetarian,1),  (cheese_lover,0),  (Cheese_lover,1),
    (eat,0),          (Eat,2),         (sibling_of,0),    (Sibling_of,2)
].
translpairs[ 
    (plant,Plant),            (cheese,Cheese),             (food,Food),
    (vegetarian,Vegetarian),  (cheese_lover,Cheese_lover), 
    (eat,Eat),                (sibling_of,Sibling_of)
].
end_of_list.

list_of_special_formulae(axioms, DL).

% TBox
concept_formula(                   % Plants and cheese are food
        implies( or( plant, cheese ), 
                 food ) ).
concept_formula(                   % Persons eat food
        implies( person, 
                 some( eat, food ) ) ).
concept_formula(                   % Vegetarians eat only plants
        implies( vegetarian, 
                 and( some( eat, plant ),
                      all(  eat, plant ) ) ) ).
concept_formula(                   % Cheese lovers eat every cheese
        implies( cheese_lover, 
                 not( some( not(eat), cheese ) ) ) ).
role_formula(                      % sibling_of is a symmetric relation
        implies( sibling_of, conv( sibling_of ) ) ).
formula( forall( [x,y,z],          % sibling_of is a transitive relation
        implies( and( Sibling_of(x,y), Sibling_of(y,z) ),
                 Sibling_of(x,z) ) ) ).

% ABox
formula( Person( adam ) ).
formula( Person( bob ) ).
formula( Sibling_of( adam, bob ) ).
formula( Plant(  cauliflower ) ).
formula( Cheese( cheddar ) ).
formula(      Eat( bob, cauliflower ) ).
formula( not( Eat( bob, cheddar ) ) ).

end_of_list.

list_of_special_formulae(conjectures, DL).

formula(  not( Cheese_lover( bob ) ) ).   % unsatisfiable
% formula( Vegetarian( bob ) ).           % satisfiable

end_of_list.

end_problem.