forked from aclai-lab/SoleLogics.jl
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathTODO
78 lines (59 loc) · 3.47 KB
/
TODO
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
########## MAIN TODOS ####################################################################################
Connectives:
☐ Change DiamondRelationalConnective and BoxRelationalConnective from singletons to structs wrapping a relation.
Interpretations:
☐ Create a SupportedInterpretation
☐ Algorithm to generate a truth table
Normalization:
☐ Add custom normalization rules to normalize
☐ Assuming boolean logic, "((¬q v p) ∧ ¬q)" could be simplified to "¬q"
Random:
☐ Generator for formulas with specific contraints:
✔ Fixed height formulas @done(23-12-06 12:04)
☐ CNF/DNF formulas
☐ UnSAT formulas
☐ Fuzzy formulas (algebra is an argument)
☐ Logger for offline formulas (in a log file, i can load and retrieve already generated formulas)
☐ Generator for complete collection of formulas generator (all possible combinations of formulas are considered)
☐ Add the following utility dispatches:
☐ rand(connectives, atom leaves array, algebra from which infer truth values)
☐ rand(connectives, atom leaves array, truth values with common supertype)
☐ rand(connectives, atom leaves array, true/false (use truth values as leaf or not. If true, default to boolean))
☐ sample(..., probability distribution)
✔ Write random models generation (see pluto-demo.jl and exploit Graphs.SimpleGraphs generation) @done(23-12-20 17:52)
☐ Expand the models generator, giving the possibility to use a generic SimpleGraphs method to shape a kripke frame
Readability:
☐ Add parameters to syntaxstring:
☐ parenthesize_unary_modals = false (force <G>phi becomes <G>(phi))
☐ parenthesize_operators
☐ meaningful names for relations: - IA_L -> After/Right - IA_A -> RightAfter
Tests:
☐ Increase code coverage
PAndQ:
☐ Recognize if a formula is satisfiable, is a contingency, a tautology or a contraddiction.
########## DONE ##########################################################################################
Documentation:
✔ In the documentation, show how to create a custom operator (maybe a Xor/⊻/⊕) starting from scratch. @done(23-12-06 12:05)
Normalization:
✔ Simplify code when possible, using dual/hasdual traits @done(23-12-06 12:05)
Random:
✔ Clean rand and sample dispatches
README:
✔ Check examples (see NOTE or pluto-demo.jl) @done(23-09-05 19:34)
✔ List of similar packages @done(23-09-05 19:30)
✔ Highlight SoleLogics use cases
Readability:
✔ Write check's docstring @done(23-09-05 19:33)
✔ Rename things to increase readability, using @deprecate in a deprecate.jl file. @done(23-12-06 12:05)
Tests:
✔ Fix SatsBase.sample errors @done(23-09-05 19:36)
✔ Add the following tests: @done(23-12-20 18:07)
✔ syntaxstring tests: get "◊¬p ∧ ¬q" from "(◊¬p) ∧ (¬q)" @done(23-12-20 18:06)
✔ syntaxstring tests: get "(q) → ((p) → (¬(q)))" from "q → p → ¬q" @done(23-12-20 18:07)
✔ (parseformula("p ∧ q ∧ r ∨ s ∧ t")) == @synexpr p ∧ q ∧ r ∨ s ∧ t @done(23-12-19 10:29)
Utilities:
✔ Differentiate Base.rand and StatsBase.sample (randformula should have a picker::Function argument, which can be rand or sample) @done(23-12-06 12:05)
✔ @atoms defaulted to String @done(23-09-12 15:48)
PAndQ:
✔ Write the algorithm that produces truth tables of propositional formulae @done(23-09-05 19:36)
✔ Macro to easily create atoms and parse expressions related to syntax (See PAndQ.jl) @done(23-09-05 19:36)