Add Monotone neighbourhood logic
Deallocate satsolver once core becomes `Open`
The satsolver is reatined and only updated with new clauses for everystate that is generated out of a core. Once the core becomes Open (asopposed to expandable), the solver is no longer needed.
This patch makes the solver a `Solver option` and gets it deallocated...
Make number of waves between propagation depend on #openCores
First implementation of propagateUnsat
Add header for function used in previous commit
Add function to determin size of Core / State set
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
Add basic graphviz export feature
Add deferral flags to core/state data structure
Add deferral accessor function
Add MuF / NuF datatypes to reasoner
Implement state listing for debugger
Implement lscores for debugger
Add basic debugging repl
Added Identity Functor and Skeleton for Default Implication
Implement functor parameters for Const
Implement raw syntax for constant functors
Change ConstF to TrueFalseF
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
Add formula constructors for PML
Implement more generic functor parsing/printing
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)
Separate cool into library and coalg frontend