Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgLogics.ml @ de84f40d

History | View | Annotate | Download (17.7 KB)

# Date Author Comment
a25a6849 02/29/2016 10:37 AM Christoph Egger

Make KD a deferral-tracking Logic

16af388e 02/15/2016 04:57 PM Christoph Egger

Make reasoner nodes include deferrals

This makes the identifying information be of type bset*bset instead of
bset and adds tracking of deferrals for propositional reasoning and --
in case of K -- for modal reasoning

d58bba0f 02/05/2015 07:02 AM Dirk Pattinson

Removed Negation Normal Form of Choice as Choice is Self-Dual

19f5dad0 02/04/2015 05:02 AM Dirk Pattinson

Added Identity Functor and Skeleton for Default Implication

93cbaa2e 01/23/2015 08:07 AM Dirk Pattinson

Implement constant functor

5e0983fe 01/22/2015 08:23 PM Thorsten Wißmann

Implement functor parameters for Const

9bae2c4f 07/21/2014 01:49 PM Thorsten Wißmann

Implement the REAL box of PML

c855ba91 07/21/2014 11:34 AM Thorsten Wißmann

Change AtMostProbable to LessProbableThan

The actual box of PML (in GMLMIP) is: less probable than. The Diamond
is: At least Probable than.

So now you have ¬[p] C = <p> C.

eda515b6 07/21/2014 11:05 AM Thorsten Wißmann

Add ocaml part of PML rule application

672429b4 07/16/2014 12:08 PM Thorsten Wißmann

Make Or-step in And-Or-rules lazy

a9949a25 07/16/2014 12:08 PM Thorsten Wißmann

Use lazylists to remove redudancy

69243f7f 07/16/2014 12:08 PM Thorsten Wißmann

Generalize ruleEnumeration by introducing lazylist

Introduce a new generic data type lazylist, e.g. used for lazy rule
enumerations.

b36e57bc 07/16/2014 12:08 PM Thorsten Wißmann

Remove Disjunctive ruleEnumerations

Propagation of satisfiability and unsatisfiability does not cover
disjunctions and I don't get how propagation works, so I won't touch it
yet. So this reverts the only partially implemented Disjunctive
ruleEnumerations,

269d93e5 07/16/2014 12:08 PM Thorsten Wißmann

Introduce junctions (Disjunction, Conjunction)

77a804ab 05/15/2014 11:53 AM Thorsten Wißmann

Add some debug output (in comments)

b5352205 05/04/2014 12:06 PM Thorsten Wißmann

Only use addBSNoChk for simple bitsets

Insert a formula into a bitset without checking for a contradiction. The
former addBS performed a contradiction-check using MiscSolver.arrayNeg
which is a array of size 0 due to not being initialized.

For some reasons this bug only could be triggered when building with...

7c4d2eb4 04/23/2014 11:21 AM Thorsten Wißmann

Separate cool into library and coalg frontend