COOL issueshttps://git8.cs.fau.de/software/cool/-/issues2021-04-30T05:35:18Zhttps://git8.cs.fau.de/software/cool/-/issues/5Split fuzzy reasoner from cool repository2021-04-30T05:35:18ZMerlinSplit fuzzy reasoner from cool repositoryThe branch `fuzzy` contains work on fuzzy reasoning by Dominik Paulus, which is unrelated to cool and should be split into a separate repository.The branch `fuzzy` contains work on fuzzy reasoning by Dominik Paulus, which is unrelated to cool and should be split into a separate repository.https://git8.cs.fau.de/software/cool/-/issues/13Decide on modules to be either public or private for proper docs2021-05-21T12:25:57ZSimon PruckerDecide on modules to be either public or private for proper docsRight now all modules are declared as private, as they are not explicitly declared public. When creating the documentation using dune build @doc, only modules declared as public will be linked in the according index file, so only decidi...Right now all modules are declared as private, as they are not explicitly declared public. When creating the documentation using dune build @doc, only modules declared as public will be linked in the according index file, so only deciding on public modules will make proper doc creation possible.https://git8.cs.fau.de/software/cool/-/issues/16Test coverage2021-05-25T12:26:41ZMerlinTest coverageGitlab has UI [support for test coverage](https://docs.gitlab.com/ee/user/project/merge_requests/test_coverage_visualization.html). Might it make sense to analyse unit test coverage to increase confidence when refactoring?
See https://g...Gitlab has UI [support for test coverage](https://docs.gitlab.com/ee/user/project/merge_requests/test_coverage_visualization.html). Might it make sense to analyse unit test coverage to increase confidence when refactoring?
See https://github.com/aantron/bisect_ppxhttps://git8.cs.fau.de/software/cool/-/issues/6Cool REPL2021-06-11T05:40:22ZMerlinCool REPLThe `repl` branch contains work by Thorsten Wißmann trying to implement a REPL for Cool. It is unclear whether that branch can be salvaged given all the changes that were meanwhile made however the idea of having a REPL for interactive l...The `repl` branch contains work by Thorsten Wißmann trying to implement a REPL for Cool. It is unclear whether that branch can be salvaged given all the changes that were meanwhile made however the idea of having a REPL for interactive logic exploration is still worthwhile.
See also Perl’s Term::Shell
http://search.cpan.org/~shlomif/Term-Shell-0.05/lib/Term/Shell.podhttps://git8.cs.fau.de/software/cool/-/issues/24Support common OWL queries2021-06-11T05:41:38ZMerlinSupport common OWL queries- [ ] classify — Classify the ontology and display the hierarchy
- [ ] consistency
- [ ] entail
- [ ] explain — Explains one or more inferences in a given ontology including
- [ ] ontology inconsistency
- [ ] concept subsumption
- [ ] i...- [ ] classify — Classify the ontology and display the hierarchy
- [ ] consistency
- [ ] entail
- [ ] explain — Explains one or more inferences in a given ontology including
- [ ] ontology inconsistency
- [ ] concept subsumption
- [ ] instance retrival
- [ ] realize — Compute and display the most specific instances for each class
- [ ] unsat — find unsatisfiable classes in the ontologyhttps://git8.cs.fau.de/software/cool/-/issues/11Introduce proper performance tests2021-06-11T13:02:21ZMerlinIntroduce proper performance testsCurrently our "performance tests" are `time` calls on stuff and the old benchmarks in the `benchmarks` folders.
It would be nice to have actual benchmarks using an actual benchmarking tool such as [hyperfine](https://github.com/sharkdp/h...Currently our "performance tests" are `time` calls on stuff and the old benchmarks in the `benchmarks` folders.
It would be nice to have actual benchmarks using an actual benchmarking tool such as [hyperfine](https://github.com/sharkdp/hyperfine) which are evaluated on MRs to see their performance impact.Simon PruckerSimon Pruckerhttps://git8.cs.fau.de/software/cool/-/issues/27Update and document examples2021-06-23T06:37:40ZMerlinUpdate and document exampleshttps://git8.cs.fau.de/software/cool/-/issues/29Document what functors are supported2021-07-06T11:11:05ZMerlinDocument what functors are supportedMake it trivial to look at the repository and see if e.g. $`F X := X^2`$ is supported currently or not.Make it trivial to look at the repository and see if e.g. $`F X := X^2`$ is supported currently or not.https://git8.cs.fau.de/software/cool/-/issues/31Specify version bounds for the dependencies in the dune-project2021-07-09T13:09:28ZMerlinSpecify version bounds for the dependencies in the dune-projecthttps://git8.cs.fau.de/software/cool/-/issues/23OWL Ontologies2021-07-13T11:25:30ZMerlinOWL OntologiesRead OWL Ontologies. Implementing support for ABoxesRead OWL Ontologies. Implementing support for ABoxeshttps://git8.cs.fau.de/software/cool/-/issues/33Refactor CoAlgReasoner into class2021-07-16T13:34:12ZMerlinRefactor CoAlgReasoner into class`CoAlgReasoner` implements multiple stateful solvers in one file. The concrete algorithm is selected by parameter `game_solver` when calling the `initReasoner` function.
It would be much cleaner to use the OCaml class mechanism (https:/...`CoAlgReasoner` implements multiple stateful solvers in one file. The concrete algorithm is selected by parameter `game_solver` when calling the `initReasoner` function.
It would be much cleaner to use the OCaml class mechanism (https://ocaml.org/manual/classes.html) here and have three subclasses of a generic solver virtual class. Then the different implementations would be neatly separated while still retaining a shared interface. Furthermore, this would force initialization and ease further extensions.https://git8.cs.fau.de/software/cool/-/issues/35Can our bitset implementation compete or should it be replaced?2021-07-20T05:40:16ZMerlinCan our bitset implementation compete or should it be replaced?Cool has its own bitset implementation which looks very performance-optimized full of references, lookup tables and mutable state. Can this be replaced by established bitset implementations or is it better and should maybe be extracted i...Cool has its own bitset implementation which looks very performance-optimized full of references, lookup tables and mutable state. Can this be replaced by established bitset implementations or is it better and should maybe be extracted into its own library?
See https://github.com/rleonid/bitset_shootouthttps://git8.cs.fau.de/software/cool/-/issues/36Remove DIY bitset filter implementation in tableau rules2021-07-20T12:33:31ZMerlinRemove DIY bitset filter implementation in tableau rulesCurrently, many old tableau rule implementations rolled their own filter implementation. this should be unified with the now-existent `filterBS` function to slim down the code and avoid duplication.Currently, many old tableau rule implementations rolled their own filter implementation. this should be unified with the now-existent `filterBS` function to slim down the code and avoid duplication.https://git8.cs.fau.de/software/cool/-/issues/38Implement formula generators for other logics2021-10-18T05:57:23ZMerlinImplement formula generators for other logicsCurrently, we only implement generators for a subset of our supported logics. It should be straightforward to implement the other logics.Currently, we only implement generators for a subset of our supported logics. It should be straightforward to implement the other logics.https://git8.cs.fau.de/software/cool/-/issues/40Are the ALC Modules still used?2021-11-05T13:26:17ZMerlinAre the ALC Modules still used?v4.0 - COOL with Modelcheckinghttps://git8.cs.fau.de/software/cool/-/issues/41Unified modality elimination2021-12-03T12:38:36ZMerlinUnified modality eliminationCurrently, there are a bunch of functions eliminating/encoding certain modalities into other modalities carrying the implicit expectation that these functions are called preprocessing for interpreting over a given functor.
It would hel...Currently, there are a bunch of functions eliminating/encoding certain modalities into other modalities carrying the implicit expectation that these functions are called preprocessing for interpreting over a given functor.
It would help extensibility and clarity if there was a single function representing the capabilities of all the functors handling all embeddings of one logic into another.
One possibility informally would be to have a function `functor -> formula -> formula` which tries to encode a given formula for a given functor or throws an exception clearly notifying the user that the given functor doesn't support the given connective.https://git8.cs.fau.de/software/cool/-/issues/28Unify random generators2021-12-09T09:13:56ZMerlinUnify random generatorsCurrently, there are two random formula generators that seem to do similar things and could probably be easily unified.Currently, there are two random formula generators that seem to do similar things and could probably be easily unified.v4.0 - COOL with Modelcheckinghttps://git8.cs.fau.de/software/cool/-/issues/43Fix formula shrinkers using simplification of tree representations for proper...2022-06-28T13:35:58ZSimon PruckerFix formula shrinkers using simplification of tree representations for property-based testsThe current implementation for shrinkers of formulae, where the formula is parsed into a tree, then the deepest connective is replaced and thus simplified, does not work within the poperty-based test environment that it was meant for, al...The current implementation for shrinkers of formulae, where the formula is parsed into a tree, then the deepest connective is replaced and thus simplified, does not work within the poperty-based test environment that it was meant for, although it works as iterator.https://git8.cs.fau.de/software/cool/-/issues/44Implement or remove PML2022-06-29T10:10:51ZSimon PruckerImplement or remove PMLPML is currently not implemented, but mentioned. As the implementation seems to be quite complicated, this could be topic for a thesis. Otherwise delete the references to PML in COOL.PML is currently not implemented, but mentioned. As the implementation seems to be quite complicated, this could be topic for a thesis. Otherwise delete the references to PML in COOL.https://git8.cs.fau.de/software/cool/-/issues/46Formula printer has its own precedence mechanism2022-09-05T12:32:12ZMerlinFormula printer has its own precedence mechanismThe formula printer has its own precedence mechanism independent of the formula parser to determine where braces should be placed. Given that those two things are completely independent of one another we might run into cases where the br...The formula printer has its own precedence mechanism independent of the formula parser to determine where braces should be placed. Given that those two things are completely independent of one another we might run into cases where the bracketing leads to mismatches.
Related to #37