Merge branch 'remove-gmlmip'
This drops the rule implementation for GML and PML, because they wererelying on GMLMIP which complicated the build process and didn't workcompletely. See Issue 19.
GML and PML are still implemented as functors but currently disabled.To re-instantiate them, an OCaml implementation is needed.
Add vim modeline to all OCaml files
Fix deferral tracking for new CoalitionLogic code
Merge remote-tracking branch 'origin/master' into flatmu
Add deferral tracking for Identity
Add deferral tracking for Fusion
Add deferral tracking for Choice
Add deferral tracking to CoalitionLogic
Add Monotone neighbourhood logic
Fix bug in FL calculation and refocusing after states
Make real empty set for deferral (not including True)
Actually use refocused deferral in modal step
Make KD a deferral-tracking Logic
Make reasoner nodes include deferrals
This makes the identifying information be of type bset*bset instead ofbset and adds tracking of deferrals for propositional reasoning and --in case of K -- for modal reasoning
CL: create enough rule 2 applications
The previous optimization in the rule 2 applications of coalition logicleft out some rule applications. Now, do enough but still do notgenerate unnecessarily many rule applications.
Fix CL for diamond formula sets with all agents
For the case of two (or more) diamond formulas who all mention the fullagent list, no rule was created, because the former CL algorithm onlycreated rules for proper subsets of the agent list. This adds the...
Removed Negation Normal Form of Choice as Choice is Self-Dual
Added Identity Functor and Skeleton for Default Implication
Implement constant functor
Implement functor parameters for Const
Implement the REAL box of PML
Change AtMostProbable to LessProbableThan
The actual box of PML (in GMLMIP) is: less probable than. The Diamondis: At least Probable than.
So now you have ¬[p] C = <p> C.
Add ocaml part of PML rule application
Make Or-step in And-Or-rules lazy
Use lazylists to remove redudancy
Generalize ruleEnumeration by introducing lazylist
Introduce a new generic data type lazylist, e.g. used for lazy ruleenumerations.
Remove Disjunctive ruleEnumerations
Propagation of satisfiability and unsatisfiability does not coverdisjunctions and I don't get how propagation works, so I won't touch ityet. So this reverts the only partially implemented DisjunctiveruleEnumerations,
Introduce junctions (Disjunction, Conjunction)
Add some debug output (in comments)
Only use addBSNoChk for simple bitsets
Insert a formula into a bitset without checking for a contradiction. Theformer addBS performed a contradiction-check using MiscSolver.arrayNegwhich is a array of size 0 due to not being initialized.
For some reasons this bug only could be triggered when building with...
Separate cool into library and coalg frontend