Interactive Tests

The following things should be checked interactively for the next release 0.99. Furthermore the nightly builds should indicate no errors for all supported architectures.

Note: The example files are located in the Hets-lib repository which will be shortly migrated to github

• check if all nodes can be proven for:

hets -g -A Calculi/Space/RCCVerification.het

Only one node is heterogeneous and needs an Isabelle proof. Make sure that the generated file RCCVerification_RCC_FO_in_MetricSpace__T.thy in the current directory is properly merged with an existing proof file. For the node ExtRCCByRCC8Rels__E2 the box "include preceding proven theorem in next proof attempt" must be checked.

• check Edit, Proofs, Auto-DG-Prover followed by Undo works for

hets -g Basic/LinearAlgebra_II.casl

• check if the red node Nat with the goal dichotomy_TotalOrder (after Edit, Proofs, Auto-DG-Prover) can be proven automatically with Vampire for

hets -g Basic/RelationsAndOrders.casl

• "Check conservativity" of link from TestSuite/Conservative/Nat.casl which calls AProVE.jar and should result in "The link is mono".

• check owl parser within the Hets repository.

hets -g -i owl OWL2/tests/wine.rdf

• check owl conservativity checker on "Cons?" links. One link can be proven! You may always choose "Locality_BOTTOM_BOTTOM". Also check consistency using pellet und fact. Check "Concept graph" of "Taxonomy Graphs" of the four OWL nodes (that calls the pellet classifier).

hets -g Ontology/Examples/Family.het

• check OntoDMU.jar within the Hets repository.

hets -g DMU/test/Integrated.het

• check if "Reduce" works within the Hets repository. (see http://www.dfki.de/sks/hets/UserGuide.pdf under "Proofs with Hets" for installation)

hets -g -A CSL/TestData/reduceTest.het