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
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