Automatically exported from code.google.com/p/cb-reasoner
OCaml Java C Makefile
Switch branches/tags
Nothing to show
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
examples No commit message Mar 28, 2011
src
INSTALL * Now use camlp4 preprocessor (module lib/pa_typeext.ml) to generate … Dec 9, 2010
LICENCE
Makefile
README * Now use camlp4 preprocessor (module lib/pa_typeext.ml) to generate … Dec 9, 2010

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.