## cool / src / lib / FuzzyALCABox.mli @ b75e5a66

History | View | Annotate | Download (1.92 KB)

1 |
(* |
---|---|

2 |
* vim: ts=2 sw=2 |

3 |
*) |

4 | |

5 |
exception CoAlgException of string |

6 | |

7 |
type concept = |

8 |
| TRUE |

9 |
| FALSE |

10 |
| AP of string |

11 |
| NOT of concept |

12 |
| OR of concept * concept |

13 |
| AND of concept * concept |

14 |
| EXISTS of int * concept |

15 |
| FORALL of int * concept |

16 | |

17 |
type asst = |

18 |
| ROLE of int * int * int |

19 |
| CONCEPT of int * concept |

20 |
type assertion = (asst list) * int * (asst list) |

21 | |

22 |
exception ConversionException of concept |

23 | |

24 |
(** Hash-consed formulae, which are in negation normal form, |

25 |
such that structural and physical equality coincide. |

26 |
*) |

27 |
type hcConcept = (hcConcept_node, concept) HashConsing.hash_consed |

28 |
and hcConcept_node = |

29 |
| HCTRUE |

30 |
| HCFALSE |

31 |
| HCAP of string |

32 |
| HCNOT of hcConcept |

33 |
| HCOR of hcConcept * hcConcept |

34 |
| HCAND of hcConcept * hcConcept |

35 |
| HCEXISTS of int * hcConcept |

36 |
| HCFORALL of int * hcConcept |

37 | |

38 |
module HcFormula : (HashConsing.S with type nde = hcConcept_node and type fml = concept) |

39 | |

40 |
type hcAsst = |

41 |
| HCROLE of int * int * int |

42 |
| HCCONCEPT of int * hcConcept |

43 | |

44 |
val toAsst : hcAsst -> asst |

45 |
val printAssertion : assertion -> string |

46 |
val toHcAsst : HcFormula.t -> asst -> hcAsst |

47 |
val hc_formula : HcFormula.t -> concept -> hcConcept |

48 |
val importQuery : string -> assertion list |

49 |
val replaceOrForall : assertion -> assertion |

50 |
val collapseNeg : assertion -> assertion |

51 |
(*val random_ABox : int -> int -> assertion*) |

52 |
val printConcept : concept -> string |

53 |
val print_fuzzyDL : concept -> string |

54 |
(* |

55 |
* Generates random concepts. |

56 |
* Parameters: Maximum operator nesting depth, |

57 |
* maximum number of operators, maximum number of atoms, |

58 |
* weights of each concept node as a list of weights, |

59 |
* e.g. [1 2 3 4] to give atomic assertions a weight |

60 |
* of 1/10, negations of 2/20, logical ands of 3/10 and |

61 |
* existential quantifiers of 4/10. If the weight of |

62 |
* atomic assertions is 0, the concept always has |

63 |
* maximum nesting depth. |

64 |
*) |

65 |
val random_concept : int -> int -> int -> int list -> concept |

66 |
val random_concept_opcount : int -> int -> int -> int list -> concept |