1% This file is part of the Attempto Parsing Engine (APE).
    2% Copyright 2008-2013, Kaarel Kaljurand <kaljurand@gmail.com>.
    3%
    4% The Attempto Parsing Engine (APE) is free software: you can redistribute it and/or modify it
    5% under the terms of the GNU Lesser General Public License as published by the Free Software
    6% Foundation, either version 3 of the License, or (at your option) any later version.
    7%
    8% The Attempto Parsing Engine (APE) is distributed in the hope that it will be useful, but WITHOUT
    9% ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR
   10% PURPOSE. See the GNU Lesser General Public License for more details.
   11%
   12% You should have received a copy of the GNU Lesser General Public License along with the Attempto
   13% Parsing Engine (APE). If not, see http://www.gnu.org/licenses/.
   14
   15
   16:- module(simplify_axiom, [
   17		simplify_axiom/2
   18	]).

Maps the given axiom to a syntactically simpler form

The given axiom is mapped to a syntactically simpler form in order to achieve better compatibility with OWL tools and OWL fragments (which are defined based on syntax). In most cases the axiom is preserved as it is, we only target the following forms:

ObjectPropertyDomain
ObjectPropertyRange
DisjointClasses
@author Kaarel Kaljurand @version 2013-04-07 @license LGPLv3

*/

 simplify_axiom(+Axiom:term, -SimplerAxiom:term) is det
Note: rule order is important
Arguments:
Axiom- is an OWL axiom
SimplerAxiom- is the same axiom possibly in a simpler form
   48% object property assertion
   49simplify_axiom(
   50	'ClassAssertion'('ObjectSomeValuesFrom'(OPE, 'ObjectOneOf'([I2])), I1),
   51	'ObjectPropertyAssertion'(OPE, I1, I2)
   52	) :- !.
   53
   54% data property assertion
   55simplify_axiom(
   56	'ClassAssertion'('DataHasValue'(DPE, Data), I1),
   57	'DataPropertyAssertion'(DPE, I1, Data)
   58	) :- !.
   59
   60% same individual
   61simplify_axiom(
   62	'ClassAssertion'('ObjectOneOf'([I2]), I1),
   63	'SameIndividual'([I1, I2])
   64	) :- !.
   65
   66% disjoint classes
   67simplify_axiom(
   68	'SubClassOf'(CE1, 'ObjectComplementOf'(CE2)),
   69	'DisjointClasses'([CE1, CE2])
   70	) :- !.
   71
   72% range
   73simplify_axiom(
   74	'SubClassOf'('ObjectIntersectionOf'([owl:'Thing', 'ObjectSomeValuesFrom'('ObjectInverseOf'(OPE), owl:'Thing')]), CE),
   75	'ObjectPropertyRange'(OPE, CE)
   76	) :- !.
   77
   78simplify_axiom(
   79	'SubClassOf'('ObjectSomeValuesFrom'('ObjectInverseOf'(OPE), owl:'Thing'), CE),
   80	'ObjectPropertyRange'(OPE, CE)
   81	) :- !.
   82
   83% domain
   84simplify_axiom(
   85	'SubClassOf'('ObjectIntersectionOf'([owl:'Thing', 'ObjectSomeValuesFrom'(OPE, owl:'Thing')]), CE),
   86	'ObjectPropertyDomain'(OPE, CE)
   87	) :- !.
   88
   89simplify_axiom(
   90	'SubClassOf'('ObjectSomeValuesFrom'(OPE, owl:'Thing'), CE),
   91	'ObjectPropertyDomain'(OPE, CE)
   92	) :- !.
   93
   94% Converts OWL 2 property axioms into a semantically equivalent yet
   95% syntactically simplified form, so that the resulting axiom is more
   96% backwards compatible with OWL 1. E.g. in case a property chain stands
   97% for a transitivity then we represent it with the TransitiveObjectProperty-axiom.
   98simplify_axiom(
   99	'SubObjectPropertyOf'('ObjectPropertyChain'(['ObjectInverseOf'(R)]), 'ObjectInverseOf'(S)),
  100	'SubObjectPropertyOf'(R, S)
  101	) :- !.
  102
  103simplify_axiom(
  104	'SubObjectPropertyOf'('ObjectPropertyChain'(['ObjectInverseOf'(R)]), S),
  105	'SubObjectPropertyOf'(R, 'ObjectInverseOf'(S))
  106	) :- !.
  107
  108simplify_axiom(
  109	'SubObjectPropertyOf'('ObjectPropertyChain'([R]), S),
  110	'SubObjectPropertyOf'(R, S)
  111	) :- !.
  112
  113simplify_axiom(
  114	'SubObjectPropertyOf'('ObjectPropertyChain'([R, R]), R),
  115	'TransitiveObjectProperty'(R)
  116	) :- !.
  117
  118
  119% no change
  120simplify_axiom(Axiom, Axiom)