README

OVERVIEW:

CB is an experimental reasoner for ontologies based on a new kind of
"consequence-based" reasoning procedure.

Currently CB supports a fragment of OWL-2 which corresponds to the DL 
Horn-SHIF. The theory behind CB is described in the paper:

[1] Y. Kazakov. Consequence-Driven Reasoning for Horn SHIQ Ontologies.
    In IJCAI, pages 2040-2045, July 11-17 2009.

CONTENTS:

  INSTALL               instructions for installation
  LICENSE               license and copyright notice
  Makefile              main Makefile
  README                this file
  bin                   reasoner executables
  examples              usage examples
  src                   program source files

COPYRIGHT:

All files in [src] are Copyright (c) 2009, 2010 Yevgeny Kazakov
<yevgeny.kazakov@comlab.ox.ac.uk> and Oxford University

INSTALLATION:

See the file INSTALL for installation instructions.

USAGE:

The binaries are located in the directory [/bin].
For the usage options type from this directory:

  ./cb --help     [on Linux & Mac]
  cb --help       [on Windows]

For usage examples see the directory [/examples]

REQUIREMENTS:

Currently CB can only read ontologies in OWL-2 functional-style syntax
and supports a subsets of the constructors corresponding to Horn-SHIF.
The reasoner will ignore any constructor or axiom type that it doesn't
support and issue a warning. Classes starting with unsupported
constructors will be treated as anonymous classes, which should not
result in any unsound inferences.

An SHIF ontology is Horn if:

  * It does not contain "ObjectUnionOf" positively, e.g., 
    within a class expressions C in the following axioms and their 
    synonyms:
      
      EquivalentClasses(C D)
      EquivalentClasses(D C)
      SubClassOf(D C)

  * It does not contain "ObjectComplementOf" and "ObjectAllValuesFrom" 
    negatively, e.g., within a class expressions C in the following 
    axioms and their synonyms:
 
      EquivalentClasses(C D)
      EquivalentClasses(D C)
      SubClassOf(C D)

The reasoner will issue a warning if the ontology is not Horn.
Please print ontology information to find out the reasons why 
ontology is not Horn:

  ./cb -i ontology.owl  [Linux & Mac]
    cb -i ontology.owl  [Windows]

For the description of OWL-2 functional-style syntax, see:
http://www.w3.org/TR/owl2-syntax/

OWL ontologies in other formats can be converted into OWL-2 functional
syntax using Protege version 4.1 or higher.

http://protege.stanford.edu/

To convert a file [ontology.owl], open it in Protege and save using
the menu:

  File > Save as... > OWL Functional Syntax.