## cool / src / lib / ALCFormula.mli @ de84f40d

History | View | Annotate | Download (3.3 KB)

1 | 4fd28192 | Thorsten Wißmann | exception ALCException of string |
---|---|---|---|

2 | |||

3 | type formula = |
||

4 | | TRUE |
||

5 | | FALSE |
||

6 | | AP of string |
||

7 | | NOT of formula |
||

8 | | EX of string * bool * formula |
||

9 | | AX of string * bool * formula |
||

10 | | MIN of int * string * bool * formula |
||

11 | | MAX of int * string * bool * formula |
||

12 | | EQU of formula * formula |
||

13 | | IMP of formula * formula |
||

14 | | OR of formula * formula |
||

15 | | AND of formula * formula |
||

16 | |||

17 | type definition = |
||

18 | | PRIMITIVE of string * formula |
||

19 | | NECANDSUFF of string * formula |
||

20 | |||

21 | val numberOfTypes : int |
||

22 | val getTypeFormula : formula -> int |
||

23 | val generateCompare : int list -> (formula -> formula -> int) |
||

24 | val aRanking : int list |
||

25 | |||

26 | val exportFormula : formula -> string |
||

27 | val exportQuery : formula list -> formula list -> definition list -> string |
||

28 | val importFormula : string -> formula |
||

29 | val importQuery : string -> (formula list) * (formula list) * definition list |
||

30 | val sizeFormula : formula -> int |
||

31 | |||

32 | val substFormula : (string * formula) list -> formula -> formula |
||

33 | |||

34 | val nnfNeg : formula -> formula |
||

35 | val nnf : formula -> formula |
||

36 | |||

37 | val containsInverse : formula -> bool |
||

38 | |||

39 | val simplifyFormula : formula -> formula |
||

40 | |||

41 | val dest_ap : formula -> string |
||

42 | val dest_not : formula -> formula |
||

43 | val dest_ex : formula -> string * bool * formula |
||

44 | val dest_ax : formula -> string * bool * formula |
||

45 | val dest_min : formula -> int * string * bool * formula |
||

46 | val dest_max : formula -> int * string * bool * formula |
||

47 | val dest_equ : formula -> formula * formula |
||

48 | val dest_imp : formula -> formula * formula |
||

49 | val dest_or : formula -> formula * formula |
||

50 | val dest_and : formula -> formula * formula |
||

51 | |||

52 | val is_true : formula -> bool |
||

53 | val is_false : formula -> bool |
||

54 | val is_ap : formula -> bool |
||

55 | val is_not : formula -> bool |
||

56 | val is_ex : formula -> bool |
||

57 | val is_ax : formula -> bool |
||

58 | val is_min : formula -> bool |
||

59 | val is_max : formula -> bool |
||

60 | val is_equ : formula -> bool |
||

61 | val is_imp : formula -> bool |
||

62 | val is_or : formula -> bool |
||

63 | val is_and : formula -> bool |
||

64 | |||

65 | val const_true : formula |
||

66 | val const_false : formula |
||

67 | val const_ap : string -> formula |
||

68 | val const_not : formula -> formula |
||

69 | val const_ex : string -> bool -> formula -> formula |
||

70 | val const_ax : string -> bool -> formula -> formula |
||

71 | val const_min : int -> string -> bool -> formula -> formula |
||

72 | val const_max : int -> string -> bool -> formula -> formula |
||

73 | val const_equ : formula -> formula -> formula |
||

74 | val const_imp : formula -> formula -> formula |
||

75 | val const_or : formula -> formula -> formula |
||

76 | val const_and : formula -> formula -> formula |
||

77 | |||

78 | val detClosure : (formula -> formula -> int) -> formula -> formula list |
||

79 | |||

80 | type hcFormula = (hcFormula_node, formula) HashConsing.hash_consed |
||

81 | and hcFormula_node = |
||

82 | | HCTRUE |
||

83 | | HCFALSE |
||

84 | | HCAP of string |
||

85 | | HCNOT of string |
||

86 | | HCEX of string * bool * hcFormula |
||

87 | | HCAX of string * bool * hcFormula |
||

88 | | HCOR of hcFormula * hcFormula |
||

89 | | HCAND of hcFormula * hcFormula |
||

90 | |||

91 | module HcFormula : (HashConsing.S with type nde = hcFormula_node and type fml = formula) |
||

92 | |||

93 | module HcFHt : (Hashtbl.S with type key = hcFormula) |
||

94 | |||

95 | val hc_formula : HcFormula.t -> formula -> hcFormula |
||

96 | val detClosureHc : HcFormula.t -> hcFormula -> hcFormula list |
||

97 | |||

98 | val exportFormulaAlcTableau : formula -> string |
||

99 | val createFactTBox : string -> formula list -> formula list -> definition list -> unit |
||

100 | val createWill : string -> formula -> unit |
||

101 | val createOWL : string -> formula list -> formula list -> definition list -> unit |
||

102 | val importTancs2000 : string -> (formula list) * (formula list) * definition list |