Connect OWL ontologies with CoAlgReasoner

src/lib/CoAlgReasoner.ml

@@ -9,6 +9,12 @@ module M = Minisat
 
 type sortTable = CoAlgMisc.sortTable
 
+type nomTable = string -> CoAlgFormula.sort option
+
+type assumptions = CoAlgFormula.sortedFormula list
+
+type input = sortTable * nomTable * assumptions * CoAlgFormula.sortedFormula
+
 
 (*****************************************************************************)
 (*                     Propagation of Satisfiability                         *)

src/lib/CoAlgReasoner.mli

@@ -5,6 +5,11 @@
 
 type sortTable = (CoAlgMisc.functors * int list) array
 
+type nomTable = string -> CoAlgFormula.sort option
+
+type assumptions = CoAlgFormula.sortedFormula list
+
+type input = sortTable * nomTable * assumptions * CoAlgFormula.sortedFormula
 
 val isSat : ?verbose:bool -> sortTable -> (string -> CoAlgFormula.sort option) ->
   CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool

src/owl/OWL.ml

@@ -2,6 +2,8 @@
 open CoolUtils
 module L = List
 module CoAlg = CoAlgFormula
+module R = CoAlgReasoner
+module CM = CoAlgMisc
 
 exception ConversionError of string
 
@@ -140,3 +142,21 @@ let coalg_global_assumption_of_owl (ax:axiom): CoAlgFormula.formula =
     | DISJOINTCLASSES l -> raise (ConversionError "not implemented yet")
     | DISJOINTUNION (c,l) -> raise (ConversionError "not implemented yet")
 
+let to_coalg (uri,axioms): R.sortTable * R.nomTable * R.assumptions =
+  let assumptions = L.map coalg_global_assumption_of_owl axioms in
+  (* make assumptions of type CoAlgFormula.formula *)
+  let (assumptions, fnctor) = (* ofcourse functor leads to "Error: pattern expected".. *)
+    try
+      (L.map CoAlg.convertToK assumptions, CM.MultiModalK)
+    with CoAlg.ConversionException ->
+      (L.map CoAlg.convertToGML assumptions, CM.GML)
+  in
+  let sorts = [| (fnctor, [0]) |] in
+  let nomTable name =
+    assert (CoAlgFormula.isNominal name);
+    Some 0
+  in
+  (* make assumptions "sorted" *)
+  let assumptions = L.map (fun f -> (0,f)) assumptions in
+  (sorts,nomTable,assumptions)
+

src/owl/OWL.mli

@@ -46,5 +46,9 @@ val string_of_ontology : ontology -> string
 val string_of_axiom : axiom -> string
 val string_of_class_exp : class_exp -> string
 
+(* try to convert some OWL ontology to coalg formulas *)
+(* first try to express it in pure K, then in GML *)
+val to_coalg : ontology -> CoAlgReasoner.sortTable * CoAlgReasoner.nomTable * CoAlgReasoner.assumptions
+
 val coalg_formula_of_owl : class_exp -> CoAlgFormula.formula
 val coalg_global_assumption_of_owl : axiom -> CoAlgFormula.formula

src/owl/cool-owl.ml

 open OWL
 open CoolUtils
 module OWLFP = OWLFunctionalParser
+module CF = CoAlgFormula
+module CR = CoAlgReasoner
 module L = List
 
+exception Exception of string
+
 let string_of_stdin (): string =
     let buf = ref "" in
     (try
@@ -33,6 +37,20 @@ let owlcat () =
     print_endline (OWLFP.string_of_tree (OWLFP.string_of_annotated id) t)
     *)
 
+let consistency () =
+    let content = string_of_stdin () in
+    (* ignore prefixes and assume that there is exactly one ontology *)
+    let (_, ontology) = match OWLFP.parse content with
+        | (u, o :: _) -> (u,o)
+        | (_, []) -> raise (Exception "File needs to contain at least one ontology")
+    in
+    let (sorts,nomTable,axioms) = OWL.to_coalg ontology in
+    let cons = CR.isSat sorts nomTable axioms (0,CF.TRUE) in
+    let cons = if cons then "yes" else "no" in
+    let (ontoname, _) = ontology in
+    Printf.printf "%s consistent: %s\n" ontoname cons
+
+
 let rec
     printUsage () =
         let p = Printf.printf in
@@ -47,6 +65,7 @@ and
     tmp_subcmds () =
         let s name func description = (name,func,description) in
         [ s "cat" owlcat "Reads a functional style OWL file from stdin and prints it"
+        ; s "consist" consistency "Checks the consistency of a OWL file from stdin"
         ; s "-h"    printUsage "Prints this help screen"
         ; s "help"  printUsage "Prints this help screen"
         ]