daTac 0.93: ########### * Use of the version 3.04 of Objective Caml. * Addition of some parameters (limit in depth for the application of simplification or paramodulation/superposition, Otter-like strategy for simplification) that may be useful for specific examples. * Some bugs fixed in the basic strategy and in the research of simplification steps. * Only two possible architectures: Linux and Solaris. Digital Unix is no more supported. daTac 0.92: ########### * Many improvements of small tasks, but with important gain in time. However, in some cases, daTac uses more memory. daTac 0.91: ########### * Translation to Objective Caml 3.0. * Creation of a manual in text format. * Addition of the possibility to add some constraints in the initial clauses. * Some small bugs fixed. daTac 0.9: ########## * Translation to Objective Caml 2.02. The main advantage is the possibility to get a Native Code executable file, that is 10 times faster than the Byte Code version. * Some minor improvements in the AC unification algorithm. daTac 0.74: ########### * Adaptation to the version 0.74 of Caml Light. * daTac is now available for Linux. * Addition of the possibility not to use the graphical inteface. * Several major improvements: ordering tests, normalisation, selection of inference steps, AC matching. * Addition of the possibility to ask for a check-up (full normalisation and display of statistics) of the deduced clauses every X generated clauses. * Addition of the Breadth-First and Otter-like strategies for selecting deduction steps. * Renaming of some options: optimised AC unification -> uncomplete AC unification linear completion -> breadth-first strategy * Several minor modifications in the graphical interface. daTac 0.7: ########## * Some bugs have been corrected. * Several functions have been rewritten for a better use of the memory. * Previous version of daTac used Steven Eker's algorithm for AC matching. For this new version, we wrote an efficient algorithm in Caml Light. * In the Parameters Menu, option Strategy, the ambiguous names Resolution and Completion have been renamed into Non-Complete and Complete, respectively. * The graphical interface has been adaptated to Tcl/Tk 8.0. The executable file of the interface (wish) is still in the bin directory, but all the libraries have been added in the lib directory. * In general, daTac 0.7 is much faster than the previous versions. What has been added: #################### * You can add some constraints to the initial clauses: unification constraints, ordering constraints,... * This is now possible to precise a precedence ordering with several minimal operators, provided that they are all equal in precedence. * At the end of an execution (or in a manual execution), this is now possible to save the obtained clauses in a new data file. * Some buttons "Store" have been added for the data windows. If this button is enable, this means some modifications have been done and have not been saved yet. * This is now possible to precise whether you want to use backward subsumption or not.