001/** 002 * Copyright (C) 2007 - 2016, Jens Lehmann 003 * 004 * This file is part of DL-Learner. 005 * 006 * DL-Learner is free software; you can redistribute it and/or modify 007 * it under the terms of the GNU General Public License as published by 008 * the Free Software Foundation; either version 3 of the License, or 009 * (at your option) any later version. 010 * 011 * DL-Learner is distributed in the hope that it will be useful, 012 * but WITHOUT ANY WARRANTY; without even the implied warranty of 013 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 014 * GNU General Public License for more details. 015 * 016 * You should have received a copy of the GNU General Public License 017 * along with this program. If not, see <http://www.gnu.org/licenses/>. 018 */ 019package org.dllearner.core.owl; 020 021import java.util.ArrayList; 022import java.util.HashSet; 023import java.util.List; 024import java.util.Set; 025 026import org.semanticweb.owlapi.model.OWLAnnotationAssertionAxiom; 027import org.semanticweb.owlapi.model.OWLAnnotationPropertyDomainAxiom; 028import org.semanticweb.owlapi.model.OWLAnnotationPropertyRangeAxiom; 029import org.semanticweb.owlapi.model.OWLAsymmetricObjectPropertyAxiom; 030import org.semanticweb.owlapi.model.OWLAxiom; 031import org.semanticweb.owlapi.model.OWLAxiomVisitorEx; 032import org.semanticweb.owlapi.model.OWLClass; 033import org.semanticweb.owlapi.model.OWLClassAssertionAxiom; 034import org.semanticweb.owlapi.model.OWLClassExpression; 035import org.semanticweb.owlapi.model.OWLClassExpressionVisitorEx; 036import org.semanticweb.owlapi.model.OWLDataAllValuesFrom; 037import org.semanticweb.owlapi.model.OWLDataComplementOf; 038import org.semanticweb.owlapi.model.OWLDataExactCardinality; 039import org.semanticweb.owlapi.model.OWLDataFactory; 040import org.semanticweb.owlapi.model.OWLDataHasValue; 041import org.semanticweb.owlapi.model.OWLDataIntersectionOf; 042import org.semanticweb.owlapi.model.OWLDataMaxCardinality; 043import org.semanticweb.owlapi.model.OWLDataMinCardinality; 044import org.semanticweb.owlapi.model.OWLDataOneOf; 045import org.semanticweb.owlapi.model.OWLDataPropertyAssertionAxiom; 046import org.semanticweb.owlapi.model.OWLDataPropertyDomainAxiom; 047import org.semanticweb.owlapi.model.OWLDataPropertyRangeAxiom; 048import org.semanticweb.owlapi.model.OWLDataRange; 049import org.semanticweb.owlapi.model.OWLDataSomeValuesFrom; 050import org.semanticweb.owlapi.model.OWLDataUnionOf; 051import org.semanticweb.owlapi.model.OWLDataVisitorEx; 052import org.semanticweb.owlapi.model.OWLDatatype; 053import org.semanticweb.owlapi.model.OWLDatatypeDefinitionAxiom; 054import org.semanticweb.owlapi.model.OWLDatatypeRestriction; 055import org.semanticweb.owlapi.model.OWLDeclarationAxiom; 056import org.semanticweb.owlapi.model.OWLDifferentIndividualsAxiom; 057import org.semanticweb.owlapi.model.OWLDisjointClassesAxiom; 058import org.semanticweb.owlapi.model.OWLDisjointDataPropertiesAxiom; 059import org.semanticweb.owlapi.model.OWLDisjointObjectPropertiesAxiom; 060import org.semanticweb.owlapi.model.OWLDisjointUnionAxiom; 061import org.semanticweb.owlapi.model.OWLEquivalentClassesAxiom; 062import org.semanticweb.owlapi.model.OWLEquivalentDataPropertiesAxiom; 063import org.semanticweb.owlapi.model.OWLEquivalentObjectPropertiesAxiom; 064import org.semanticweb.owlapi.model.OWLFacetRestriction; 065import org.semanticweb.owlapi.model.OWLFunctionalDataPropertyAxiom; 066import org.semanticweb.owlapi.model.OWLFunctionalObjectPropertyAxiom; 067import org.semanticweb.owlapi.model.OWLHasKeyAxiom; 068import org.semanticweb.owlapi.model.OWLInverseFunctionalObjectPropertyAxiom; 069import org.semanticweb.owlapi.model.OWLInverseObjectPropertiesAxiom; 070import org.semanticweb.owlapi.model.OWLIrreflexiveObjectPropertyAxiom; 071import org.semanticweb.owlapi.model.OWLLiteral; 072import org.semanticweb.owlapi.model.OWLNegativeDataPropertyAssertionAxiom; 073import org.semanticweb.owlapi.model.OWLNegativeObjectPropertyAssertionAxiom; 074import org.semanticweb.owlapi.model.OWLObjectAllValuesFrom; 075import org.semanticweb.owlapi.model.OWLObjectComplementOf; 076import org.semanticweb.owlapi.model.OWLObjectExactCardinality; 077import org.semanticweb.owlapi.model.OWLObjectHasSelf; 078import org.semanticweb.owlapi.model.OWLObjectHasValue; 079import org.semanticweb.owlapi.model.OWLObjectIntersectionOf; 080import org.semanticweb.owlapi.model.OWLObjectMaxCardinality; 081import org.semanticweb.owlapi.model.OWLObjectMinCardinality; 082import org.semanticweb.owlapi.model.OWLObjectOneOf; 083import org.semanticweb.owlapi.model.OWLObjectPropertyAssertionAxiom; 084import org.semanticweb.owlapi.model.OWLObjectPropertyDomainAxiom; 085import org.semanticweb.owlapi.model.OWLObjectPropertyRangeAxiom; 086import org.semanticweb.owlapi.model.OWLObjectSomeValuesFrom; 087import org.semanticweb.owlapi.model.OWLObjectUnionOf; 088import org.semanticweb.owlapi.model.OWLReflexiveObjectPropertyAxiom; 089import org.semanticweb.owlapi.model.OWLSameIndividualAxiom; 090import org.semanticweb.owlapi.model.OWLSubAnnotationPropertyOfAxiom; 091import org.semanticweb.owlapi.model.OWLSubClassOfAxiom; 092import org.semanticweb.owlapi.model.OWLSubDataPropertyOfAxiom; 093import org.semanticweb.owlapi.model.OWLSubObjectPropertyOfAxiom; 094import org.semanticweb.owlapi.model.OWLSubPropertyChainOfAxiom; 095import org.semanticweb.owlapi.model.OWLSymmetricObjectPropertyAxiom; 096import org.semanticweb.owlapi.model.OWLTransitiveObjectPropertyAxiom; 097import org.semanticweb.owlapi.model.SWRLRule; 098 099/** 100 * 101 * A modified version of the NNF computation contained in the OWL API. The 102 * main difference is in the usage of DL-Learner version of intersection and 103 * union which allow for redundant usage of sub expression, e.g. (A and A) 104 * 105 * @author Lorenz Buehmann 106 * @author Matthew Horridge, The University Of Manchester, Information Management 107 * Group, Date: 06-Jun-2008 108 */ 109public class NNF implements OWLClassExpressionVisitorEx<OWLClassExpression>, 110 OWLDataVisitorEx<OWLDataRange>, OWLAxiomVisitorEx<OWLAxiom> { 111 112 private boolean negated; 113 private final OWLDataFactory dataFactory; 114 115 /** 116 * @param dataFactory 117 * datafactory to use 118 */ 119 public NNF(OWLDataFactory dataFactory) { 120 this.dataFactory = dataFactory; 121 } 122 123 /** reset the negation. */ 124 public void reset() { 125 negated = false; 126 } 127 128 private OWLClassExpression getNegation(OWLClassExpression classExpression) { 129 return dataFactory.getOWLObjectComplementOf(classExpression); 130 } 131 132 @Override 133 public OWLClassExpression visit(OWLClass desc) { 134 if (negated) { 135 if (desc.isOWLNothing()) { 136 return dataFactory.getOWLThing(); 137 } else if (desc.isOWLThing()) { 138 return dataFactory.getOWLNothing(); 139 } else { 140 return getNegation(desc); 141 } 142 } else { 143 return desc; 144 } 145 } 146 147 @Override 148 public OWLClassExpression visit(OWLObjectIntersectionOf desc) { 149 List<OWLClassExpression> ops = new ArrayList<>(); 150 for (OWLClassExpression op : desc.getOperandsAsList()) { 151 ops.add(op.accept(this)); 152 } 153 if (negated) { 154 return new OWLObjectUnionOfImplExt(ops); 155 } else { 156 return new OWLObjectIntersectionOfImplExt(ops); 157 } 158 } 159 160 @Override 161 public OWLClassExpression visit(OWLObjectUnionOf desc) { 162 List<OWLClassExpression> ops = new ArrayList<>(); 163 for (OWLClassExpression op : desc.getOperandsAsList()) { 164 ops.add(op.accept(this)); 165 } 166 if (negated) { 167 // Flip to an intersection 168 return new OWLObjectIntersectionOfImplExt(ops); 169 } else { 170 return new OWLObjectUnionOfImplExt(ops); 171 } 172 } 173 174 @Override 175 public OWLClassExpression visit(OWLObjectComplementOf desc) { 176 if (negated) { 177 // Cancels out. 178 // Save and then restore. 179 boolean neg = negated; 180 negated = false; 181 OWLClassExpression negDesc = desc.getOperand().accept(this); 182 negated = neg; 183 return negDesc; 184 } else { 185 // Save and then restore 186 boolean neg = negated; 187 negated = true; 188 OWLClassExpression negDesc = desc.getOperand().accept(this); 189 negated = neg; 190 return negDesc; 191 } 192 } 193 194 @Override 195 public OWLClassExpression visit(OWLObjectSomeValuesFrom desc) { 196 OWLClassExpression filler = desc.getFiller().accept(this); 197 if (negated) { 198 return dataFactory.getOWLObjectAllValuesFrom(desc.getProperty(), 199 filler); 200 } else { 201 return dataFactory.getOWLObjectSomeValuesFrom(desc.getProperty(), 202 filler); 203 } 204 } 205 206 @Override 207 public OWLClassExpression visit(OWLObjectAllValuesFrom desc) { 208 OWLClassExpression filler = desc.getFiller().accept(this); 209 if (negated) { 210 return dataFactory.getOWLObjectSomeValuesFrom(desc.getProperty(), 211 filler); 212 } else { 213 return dataFactory.getOWLObjectAllValuesFrom(desc.getProperty(), 214 filler); 215 } 216 } 217 218 @Override 219 public OWLClassExpression visit(OWLObjectHasValue desc) { 220 return desc.asSomeValuesFrom().accept(this); 221 } 222 223 @Override 224 public OWLClassExpression visit(OWLObjectMinCardinality desc) { 225 boolean neg = negated; 226 int card = desc.getCardinality(); 227 if (negated) { 228 card = desc.getCardinality() - 1; 229 if (card < 0) { 230 card = 0; 231 } 232 } 233 negated = false; 234 235 OWLClassExpression filler = desc.getFiller().accept(this); 236 237 OWLClassExpression nnf; 238 if (neg) { 239 nnf = dataFactory.getOWLObjectMaxCardinality(card, desc.getProperty(), filler); 240 } else { 241 nnf = dataFactory.getOWLObjectMinCardinality(card, desc.getProperty(), filler); 242 } 243 negated = neg; 244 return nnf; 245 } 246 247 @Override 248 public OWLClassExpression visit(OWLObjectExactCardinality ce) { 249 return dataFactory.getOWLObjectExactCardinality(ce.getCardinality(), ce.getProperty(), ce.getFiller().accept(this)); 250// return desc.asIntersectionOfMinMax().accept(this); 251 } 252 253 @Override 254 public OWLClassExpression visit(OWLObjectMaxCardinality desc) { 255 boolean neg = negated; 256 int card = desc.getCardinality(); 257 if (negated) { 258 card = desc.getCardinality() + 1; 259 } 260 negated = false; 261 OWLClassExpression filler = desc.getFiller().accept(this); 262 263 OWLClassExpression nnf; 264 if (neg) { 265 nnf = dataFactory.getOWLObjectMinCardinality(card, 266 desc.getProperty(), filler); 267 } else { 268 nnf = dataFactory.getOWLObjectMaxCardinality(card, 269 desc.getProperty(), filler); 270 } 271 negated = neg; 272 return nnf; 273 } 274 275 @Override 276 public OWLClassExpression visit(OWLObjectHasSelf desc) { 277 if (negated) { 278 return getNegation(desc); 279 } else { 280 return desc; 281 } 282 } 283 284 @Override 285 public OWLClassExpression visit(OWLObjectOneOf desc) { 286 if (desc.getIndividuals().size() == 1) { 287 if (negated) { 288 return getNegation(desc); 289 } else { 290 return desc; 291 } 292 } else { 293 return desc.asObjectUnionOf().accept(this); 294 } 295 } 296 297 @Override 298 public OWLClassExpression visit(OWLDataSomeValuesFrom desc) { 299 OWLDataRange filler = desc.getFiller().accept(this); 300 if (negated) { 301 return dataFactory.getOWLDataAllValuesFrom(desc.getProperty(), 302 filler); 303 } else { 304 return dataFactory.getOWLDataSomeValuesFrom(desc.getProperty(), 305 filler); 306 } 307 } 308 309 @Override 310 public OWLClassExpression visit(OWLDataAllValuesFrom desc) { 311 OWLDataRange filler = desc.getFiller().accept(this); 312 if (negated) { 313 return dataFactory.getOWLDataSomeValuesFrom(desc.getProperty(), 314 filler); 315 } else { 316 return dataFactory.getOWLDataAllValuesFrom(desc.getProperty(), 317 filler); 318 } 319 } 320 321 @Override 322 public OWLClassExpression visit(OWLDataHasValue desc) { 323 return desc.asSomeValuesFrom().accept(this); 324 } 325 326 @Override 327 public OWLClassExpression visit(OWLDataExactCardinality desc) { 328 return desc.asIntersectionOfMinMax().accept(this); 329 } 330 331 @Override 332 public OWLClassExpression visit(OWLDataMaxCardinality desc) { 333 boolean neg = negated; 334 int card = desc.getCardinality(); 335 if (negated) { 336 card = desc.getCardinality() + 1; 337 } 338 negated = false; 339 OWLDataRange filler = desc.getFiller().accept(this); 340 OWLClassExpression nnf; 341 if (neg) { 342 nnf = dataFactory.getOWLDataMinCardinality(card, 343 desc.getProperty(), filler); 344 } else { 345 nnf = dataFactory.getOWLDataMaxCardinality(card, 346 desc.getProperty(), filler); 347 } 348 negated = neg; 349 return nnf; 350 } 351 352 @Override 353 public OWLClassExpression visit(OWLDataMinCardinality desc) { 354 boolean neg = negated; 355 int card = desc.getCardinality(); 356 if (negated) { 357 card = desc.getCardinality() - 1; 358 if (card < 0) { 359 card = 0; 360 } 361 } 362 negated = false; 363 OWLDataRange filler = desc.getFiller().accept(this); 364 OWLClassExpression nnf; 365 if (neg) { 366 nnf = dataFactory.getOWLDataMaxCardinality(card, 367 desc.getProperty(), filler); 368 } else { 369 nnf = dataFactory.getOWLDataMinCardinality(card, 370 desc.getProperty(), filler); 371 } 372 negated = neg; 373 return nnf; 374 } 375 376 // ///////////////////////////////////////////////////////////////////////////////////////////////////////// 377 @Override 378 public OWLDataRange visit(OWLDatatype node) { 379 if (negated) { 380 return dataFactory.getOWLDataComplementOf(node); 381 } else { 382 return node; 383 } 384 } 385 386 @Override 387 public OWLDataRange visit(OWLDataComplementOf node) { 388 if (negated) { 389 return node.getDataRange(); 390 } else { 391 return node; 392 } 393 } 394 395 @Override 396 public OWLDataRange visit(OWLDataOneOf node) { 397 if (node.getValues().size() == 1) { 398 if (negated) { 399 return dataFactory.getOWLDataComplementOf(node); 400 } else { 401 return node; 402 } 403 } else { 404 // Encode as a data union of and return result 405 Set<OWLDataOneOf> oneOfs = new HashSet<>(); 406 for (OWLLiteral lit : node.getValues()) { 407 oneOfs.add(dataFactory.getOWLDataOneOf(lit)); 408 } 409 return dataFactory.getOWLDataUnionOf(oneOfs).accept(this); 410 } 411 } 412 413 @Override 414 public OWLDataRange visit(OWLDataIntersectionOf node) { 415 Set<OWLDataRange> ops = new HashSet<>(); 416 for (OWLDataRange op : node.getOperands()) { 417 ops.add(op.accept(this)); 418 } 419 if (negated) { 420 return dataFactory.getOWLDataUnionOf(ops); 421 } else { 422 return dataFactory.getOWLDataIntersectionOf(ops); 423 } 424 } 425 426 @Override 427 public OWLDataRange visit(OWLDataUnionOf node) { 428 Set<OWLDataRange> ops = new HashSet<>(); 429 for (OWLDataRange op : node.getOperands()) { 430 ops.add(op.accept(this)); 431 } 432 if (negated) { 433 // Flip to an intersection 434 return dataFactory.getOWLDataIntersectionOf(ops); 435 } else { 436 return dataFactory.getOWLDataUnionOf(ops); 437 } 438 } 439 440 @Override 441 public OWLAxiom visit(OWLHasKeyAxiom axiom) { 442 return null; 443 } 444 445 @Override 446 public OWLDataRange visit(OWLDatatypeRestriction node) { 447 if (negated) { 448 return dataFactory.getOWLDataComplementOf(node); 449 } else { 450 return node; 451 } 452 } 453 454 @Override 455 public OWLDataRange visit(OWLLiteral node) { 456 return null; 457 } 458 459 @Override 460 public OWLDataRange visit(OWLFacetRestriction node) { 461 return null; 462 } 463 464 // ////////////////////////////////////////////////////////////////////////////////////////////// 465 // 466 // Conversion of non-class expressions to NNF 467 // 468 // ///////////////////////////////////////////////////////////////////////////////////////////// 469 @Override 470 public OWLAxiom visit(OWLSubClassOfAxiom axiom) { 471 return dataFactory.getOWLSubClassOfAxiom( 472 axiom.getSubClass().accept(this), 473 axiom.getSuperClass().accept(this)); 474 } 475 476 @Override 477 public OWLAxiom visit(OWLNegativeObjectPropertyAssertionAxiom axiom) { 478 return axiom; 479 } 480 481 @Override 482 public OWLAxiom visit(OWLAsymmetricObjectPropertyAxiom axiom) { 483 return axiom; 484 } 485 486 @Override 487 public OWLAxiom visit(OWLReflexiveObjectPropertyAxiom axiom) { 488 return axiom; 489 } 490 491 @Override 492 public OWLAxiom visit(OWLDisjointClassesAxiom axiom) { 493 Set<OWLClassExpression> ops = new HashSet<>(); 494 for (OWLClassExpression op : axiom.getClassExpressions()) { 495 ops.add(op.accept(this)); 496 } 497 return dataFactory.getOWLDisjointClassesAxiom(ops); 498 } 499 500 @Override 501 public OWLAxiom visit(OWLDataPropertyDomainAxiom axiom) { 502 return dataFactory.getOWLDataPropertyDomainAxiom(axiom.getProperty(), 503 axiom.getDomain().accept(this)); 504 } 505 506 @Override 507 public OWLAxiom visit(OWLObjectPropertyDomainAxiom axiom) { 508 return dataFactory.getOWLObjectPropertyDomainAxiom(axiom.getProperty(), 509 axiom.getDomain().accept(this)); 510 } 511 512 @Override 513 public OWLAxiom visit(OWLEquivalentObjectPropertiesAxiom axiom) { 514 return axiom; 515 } 516 517 @Override 518 public OWLAxiom visit(OWLNegativeDataPropertyAssertionAxiom axiom) { 519 return axiom; 520 } 521 522 @Override 523 public OWLAxiom visit(OWLDifferentIndividualsAxiom axiom) { 524 return axiom; 525 } 526 527 @Override 528 public OWLAxiom visit(OWLDisjointDataPropertiesAxiom axiom) { 529 return axiom; 530 } 531 532 @Override 533 public OWLAxiom visit(OWLDisjointObjectPropertiesAxiom axiom) { 534 return axiom; 535 } 536 537 @Override 538 public OWLAxiom visit(OWLObjectPropertyRangeAxiom axiom) { 539 return dataFactory.getOWLObjectPropertyRangeAxiom(axiom.getProperty(), 540 axiom.getRange().accept(this)); 541 } 542 543 @Override 544 public OWLAxiom visit(OWLObjectPropertyAssertionAxiom axiom) { 545 return axiom; 546 } 547 548 @Override 549 public OWLAxiom visit(OWLFunctionalObjectPropertyAxiom axiom) { 550 return axiom; 551 } 552 553 @Override 554 public OWLAxiom visit(OWLSubObjectPropertyOfAxiom axiom) { 555 return axiom; 556 } 557 558 @Override 559 public OWLAxiom visit(OWLDisjointUnionAxiom axiom) { 560 Set<OWLClassExpression> descs = new HashSet<>(); 561 for (OWLClassExpression op : axiom.getClassExpressions()) { 562 descs.add(op.accept(this)); 563 } 564 return dataFactory.getOWLDisjointUnionAxiom(axiom.getOWLClass(), descs); 565 } 566 567 @Override 568 public OWLAxiom visit(OWLDeclarationAxiom axiom) { 569 return axiom; 570 } 571 572 @Override 573 public OWLAxiom visit(OWLAnnotationAssertionAxiom axiom) { 574 return axiom; 575 } 576 577 @Override 578 public OWLAxiom visit(OWLSymmetricObjectPropertyAxiom axiom) { 579 return axiom; 580 } 581 582 @Override 583 public OWLAxiom visit(OWLDataPropertyRangeAxiom axiom) { 584 return dataFactory.getOWLDataPropertyRangeAxiom(axiom.getProperty(), 585 axiom.getRange().accept(this)); 586 } 587 588 @Override 589 public OWLAxiom visit(OWLFunctionalDataPropertyAxiom axiom) { 590 return axiom; 591 } 592 593 @Override 594 public OWLAxiom visit(OWLEquivalentDataPropertiesAxiom axiom) { 595 return axiom; 596 } 597 598 @Override 599 public OWLAxiom visit(OWLClassAssertionAxiom axiom) { 600 if (axiom.getClassExpression().isAnonymous()) { 601 return dataFactory.getOWLClassAssertionAxiom(axiom 602 .getClassExpression().accept(this), axiom.getIndividual()); 603 } else { 604 return axiom; 605 } 606 } 607 608 @Override 609 public OWLAxiom visit(OWLEquivalentClassesAxiom axiom) { 610 Set<OWLClassExpression> ops = new HashSet<>(); 611 for (OWLClassExpression op : axiom.getClassExpressions()) { 612 ops.add(op.accept(this)); 613 } 614 return dataFactory.getOWLEquivalentClassesAxiom(ops); 615 } 616 617 @Override 618 public OWLAxiom visit(OWLDataPropertyAssertionAxiom axiom) { 619 return axiom; 620 } 621 622 @Override 623 public OWLAxiom visit(OWLTransitiveObjectPropertyAxiom axiom) { 624 return axiom; 625 } 626 627 @Override 628 public OWLAxiom visit(OWLIrreflexiveObjectPropertyAxiom axiom) { 629 return axiom; 630 } 631 632 @Override 633 public OWLAxiom visit(OWLSubDataPropertyOfAxiom axiom) { 634 return axiom; 635 } 636 637 @Override 638 public OWLAxiom visit(OWLInverseFunctionalObjectPropertyAxiom axiom) { 639 return axiom; 640 } 641 642 @Override 643 public OWLAxiom visit(OWLSameIndividualAxiom axiom) { 644 return axiom; 645 } 646 647 @Override 648 public OWLAxiom visit(OWLSubPropertyChainOfAxiom axiom) { 649 return axiom; 650 } 651 652 @Override 653 public OWLAxiom visit(OWLInverseObjectPropertiesAxiom axiom) { 654 return axiom; 655 } 656 657 @Override 658 public OWLAxiom visit(SWRLRule rule) { 659 return rule; 660 } 661 662 @Override 663 public OWLAxiom visit(OWLAnnotationPropertyDomainAxiom axiom) { 664 return axiom; 665 } 666 667 @Override 668 public OWLAxiom visit(OWLAnnotationPropertyRangeAxiom axiom) { 669 return axiom; 670 } 671 672 @Override 673 public OWLAxiom visit(OWLSubAnnotationPropertyOfAxiom axiom) { 674 return axiom; 675 } 676 677 @Override 678 public OWLAxiom visit(OWLDatatypeDefinitionAxiom axiom) { 679 return axiom; 680 } 681}