| Branch: | Revision:

cool / src / lib / CoAlgFormula.mli @ 946e8213

History | View | Annotate | Download (6.47 KB)

# Date Author Comment
946e8213 06/20/2017 07:41 PM Kristin Braun

translation from nominal to EG AF works for K

b6653b96 04/06/2017 05:57 PM Hans-Peter Deifel

Don't hardcode check for aconjunctive formulas

Previously, cool would simply raise an exception if the formula was
not aconjunctive. This was done to ease testing of the new reasoner

Now, the reasoner decides whether the formula is aconjunctive or not...

a57eb439 03/21/2017 09:12 PM Hans-Peter Deifel

Add vim modeline to all OCaml files

97d73a78 04/12/2016 02:54 PM Christoph Egger

Fix A ( φ U ψ ) and E ( φ U ψ ) translation

e30caa42 04/11/2016 12:13 AM Christoph Egger

Implement {A,E}( .. {R,B} ..) CTL formulas

5e7c8aa1 01/26/2016 04:29 PM Christoph Egger

Add function to verify if deferral is still mentioned in formula

cc07e93d 12/01/2015 04:43 PM Christoph Egger

Add function to substitute variables

1484d8cb 11/17/2015 03:54 PM Christoph Egger

Move verification of formula to separate step

d29d35f7 11/09/2015 02:43 PM Christoph Egger

Actually represent variable under μ/ν as string

so it's `MU of string * formula` again. The variable within the formula
is still represented as `VAR s`

87d5082f 11/09/2015 02:43 PM Christoph Egger

Add μ-constructors for hcFormula

CTL is assumed to be eliminated before the hash-consing step

b179a57f 10/30/2015 05:57 PM Christoph Egger

Add new datatypes for CTL

9a3b23cc 10/28/2015 05:10 PM Christoph Egger

Add New datatypes for μ-Calculus

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

c49eea11 01/22/2015 06:58 PM Thorsten Wißmann

Implement raw syntax for constant functors

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.

86b07be8 07/20/2014 11:05 AM Thorsten Wißmann

Add formula constructors for PML

e5422169 07/19/2014 06:36 PM Thorsten Wißmann

Add syntax for PML

ca99d0c6 05/06/2014 08:30 AM Thorsten Wißmann

Improve OWL -> CoAlg conversion

dbcce612 05/05/2014 01:16 PM Thorsten Wißmann

Implement fuzzy formula conversion to K or GML

0247525c 05/05/2014 12:02 PM Thorsten Wißmann

Add comments for CoAlgFormula.formula constructors

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

Separate cool into library and coalg frontend