smcdel-1.3.0: Symbolic Model Checking for Dynamic Epistemic Logic
Quick Jump
Contents
Index
Index
!
SMCDEL.Internal.Help
!=
SMCDEL.Internal.Help
$$
SMCDEL.Symbolic.S5
aAnnounce
SMCDEL.Examples.RussianCards
Act
1 (Type/Class)
SMCDEL.Explicit.K
2 (Data Constructor)
SMCDEL.Explicit.K
Action
SMCDEL.Explicit.S5
ActionModel
SMCDEL.Explicit.K
ActionModelS5
SMCDEL.Explicit.S5
actionOne
SMCDEL.Examples
actionToEvent
1 (Function)
SMCDEL.Translations.S5
2 (Function)
SMCDEL.Translations.K
actionToEventMulti
SMCDEL.Translations.S5
actionToTransformerWithMap
SMCDEL.Translations.S5
actionTwo
SMCDEL.Examples
ActM
SMCDEL.Explicit.K
ActMS5
SMCDEL.Explicit.S5
after
1 (Function)
SMCDEL.Examples.GossipS5
2 (Function)
SMCDEL.Examples.GossipKw
Ag
1 (Data Constructor)
SMCDEL.Explicit.DEMO_S5
2 (Data Constructor)
SMCDEL.Language
AgAgent
SMCDEL.Language
ageKnsStart
SMCDEL.Examples.Cheryl
Agent
1 (Type/Class)
SMCDEL.Explicit.DEMO_S5
2 (Type/Class)
SMCDEL.Language
agentsInForm
SMCDEL.Language
agentsOf
SMCDEL.Language
aIs
SMCDEL.Examples.WhatSum
aKnowsBs
SMCDEL.Examples.RussianCards
aKnowsBsN
SMCDEL.Examples.RussianCards
alice
SMCDEL.Language
aliceBdd
SMCDEL.Examples.SimpleK
alicesActions
SMCDEL.Examples.RussianCards
allCardsGiven
SMCDEL.Examples.RussianCards
allCardsUnique
SMCDEL.Examples.RussianCards
allCasesUpTo
SMCDEL.Examples.RussianCards
alldiff
SMCDEL.Internal.Help
alleq
SMCDEL.Internal.Help
alleqWith
SMCDEL.Internal.Help
allExperts
1 (Function)
SMCDEL.Examples.GossipS5
2 (Function)
SMCDEL.Examples.GossipKw
allHandLists
SMCDEL.Examples.RussianCards
allHandListsN
SMCDEL.Examples.RussianCards
allsamebdd
1 (Function)
SMCDEL.Internal.TaggedBDD
2 (Function)
SMCDEL.Symbolic.Ki
3 (Function)
SMCDEL.Symbolic.K
allSatsWith
SMCDEL.Symbolic.S5_DD
allSequs
1 (Function)
SMCDEL.Examples.GossipS5
2 (Function)
SMCDEL.Examples.GossipKw
allStates
1 (Function)
SMCDEL.Examples.CherylDemo
2 (Function)
SMCDEL.Examples.Cheryl
annePutsMarbleInBox
SMCDEL.Examples.SallyAnne
Announce
SMCDEL.Language
announce
1 (Function)
SMCDEL.Explicit.S5
2 (Function)
SMCDEL.Symbolic.S5
3 (Function)
SMCDEL.Symbolic.S5_DD
4 (Function)
SMCDEL.Symbolic.Ki
5 (Function)
SMCDEL.Symbolic.K
6 (Function)
SMCDEL.Examples.DoorMat
announce'
SMCDEL.Examples.DoorMat
announceAction
1 (Function)
SMCDEL.Explicit.S5
2 (Function)
SMCDEL.Explicit.K
announceOnScn
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
AnnounceW
SMCDEL.Language
anydiff
SMCDEL.Internal.Help
anydiffWith
SMCDEL.Internal.Help
apply
SMCDEL.Internal.Help
applyPartial
SMCDEL.Internal.Help
aProps
SMCDEL.Examples.WhatSum
asSeenBy
SMCDEL.Other.Planning
Assignment
SMCDEL.Explicit.S5
at
SMCDEL.Examples.LetterPassing
atP
SMCDEL.Examples.LetterPassing
bAnnounce
SMCDEL.Examples.RussianCards
Bdd
SMCDEL.Symbolic.S5_DD
bddEval
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
bddOf
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
3 (Function)
SMCDEL.Symbolic.Ki
4 (Function)
SMCDEL.Symbolic.K
bddprefix
1 (Function)
SMCDEL.Symbolic.Ki
2 (Function)
SMCDEL.Symbolic.K
bddReduce
1 (Function)
SMCDEL.Symbolic.Ki
2 (Function)
SMCDEL.Symbolic.K
bddsuffix
1 (Function)
SMCDEL.Symbolic.Ki
2 (Function)
SMCDEL.Symbolic.K
begintab
SMCDEL.Internal.TexDisplay
BelScene
1 (Type/Class)
SMCDEL.Symbolic.Ki
2 (Type/Class)
SMCDEL.Symbolic.K
BelStruct
1 (Type/Class)
SMCDEL.Symbolic.Ki
2 (Type/Class)
SMCDEL.Symbolic.K
BF
1 (Type/Class)
SMCDEL.Language
2 (Data Constructor)
SMCDEL.Language
bIs
SMCDEL.Examples.WhatSum
bisimClasses
SMCDEL.Explicit.S5
bisiminimize
SMCDEL.Explicit.S5
Bisimulation
SMCDEL.Explicit.S5
bitsOf
SMCDEL.Examples.Cheryl
bKnowsAs
SMCDEL.Examples.RussianCards
bKnowsAsN
SMCDEL.Examples.RussianCards
bl
SMCDEL.Internal.Help
BlS
1 (Data Constructor)
SMCDEL.Symbolic.Ki
2 (Data Constructor)
SMCDEL.Symbolic.K
blsToKripke
SMCDEL.Translations.K
bob
SMCDEL.Language
bobBdd
SMCDEL.Examples.SimpleK
bobsActions
SMCDEL.Examples.RussianCards
boolBddOf
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
boolEvalViaBdd
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
booloutof
SMCDEL.Translations.S5
booloutofForm
SMCDEL.Language
Bot
SMCDEL.Language
bot
SMCDEL.Symbolic.S5_DD
box
SMCDEL.Language
bProps
SMCDEL.Examples.WhatSum
broOne
SMCDEL.Examples.Cheryl
bTables
SMCDEL.Explicit.DEMO_S5
buildMC
SMCDEL.Examples.MuddyChildren
buildResult
SMCDEL.Examples.MuddyChildren
call
1 (Function)
SMCDEL.Examples.GossipS5
2 (Function)
SMCDEL.Examples.GossipKw
callTrf
1 (Function)
SMCDEL.Examples.GossipS5
2 (Function)
SMCDEL.Examples.GossipKw
cardIsAt
SMCDEL.Examples.Toynabi
carol
SMCDEL.Language
Check
SMCDEL.Other.Planning
checkBisim
1 (Function)
SMCDEL.Explicit.S5
2 (Function)
SMCDEL.Explicit.K
checkBisimClasses
SMCDEL.Explicit.S5
checkBisimPointed
1 (Function)
SMCDEL.Explicit.S5
2 (Function)
SMCDEL.Explicit.K
checkHandsFor
SMCDEL.Examples.RussianCards
checkPropu
SMCDEL.Symbolic.S5
checks
SMCDEL.Language
checkSet
SMCDEL.Examples.RussianCards
checkSetFor
SMCDEL.Examples.RussianCards
cheryl
SMCDEL.Examples.Cheryl
cherylIs
SMCDEL.Examples.CherylDemo
cherylsBirthday
SMCDEL.Examples.Cheryl
cIgnorant
SMCDEL.Examples.RussianCards
cIgnorantN
SMCDEL.Examples.RussianCards
cIs
SMCDEL.Examples.WhatSum
Ck
SMCDEL.Language
Ckw
SMCDEL.Language
Clean
SMCDEL.Other.MCTRIANGLE
cleanupObsLaw
SMCDEL.Symbolic.K
coinFlip
SMCDEL.Examples.CoinFlip
coinResult
SMCDEL.Examples.CoinFlip
coinStart
SMCDEL.Examples.CoinFlip
comknow
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
con
SMCDEL.Symbolic.S5_DD
Conj
1 (Data Constructor)
SMCDEL.Explicit.DEMO_S5
2 (Data Constructor)
SMCDEL.Language
3 (Data Constructor)
SMCDEL.Other.MCTRIANGLE
conSet
SMCDEL.Symbolic.S5_DD
convert
SMCDEL.Translations.Convert
Convertable
SMCDEL.Translations.Convert
CoopTask
1 (Type/Class)
SMCDEL.Other.Planning
2 (Data Constructor)
SMCDEL.Other.Planning
cp
1 (Function)
SMCDEL.Internal.TaggedBDD
2 (Function)
SMCDEL.Symbolic.Ki
3 (Function)
SMCDEL.Symbolic.K
cpBdd
1 (Function)
SMCDEL.Symbolic.Ki
2 (Function)
SMCDEL.Symbolic.K
cpMany
SMCDEL.Internal.TaggedBDD
cpP
1 (Function)
SMCDEL.Symbolic.Ki
2 (Function)
SMCDEL.Symbolic.K
cProps
SMCDEL.Examples.WhatSum
dayIs
SMCDEL.Examples.Cheryl
dcCheckForm
SMCDEL.Examples.DiningCrypto
dcScn1
SMCDEL.Examples.DiningCrypto
dcScn2
SMCDEL.Examples.DiningCrypto
dcScnInit
SMCDEL.Examples.DiningCrypto
dcValid
SMCDEL.Examples.DiningCrypto
defaultAgents
SMCDEL.Language
defaultVocabulary
SMCDEL.Language
DemoForm
SMCDEL.Explicit.DEMO_S5
DemoP
SMCDEL.Explicit.DEMO_S5
DemoPrp
SMCDEL.Explicit.DEMO_S5
DemoQ
SMCDEL.Explicit.DEMO_S5
DemoR
SMCDEL.Explicit.DEMO_S5
DemoS
SMCDEL.Explicit.DEMO_S5
descableRels
SMCDEL.Translations.S5
determinedVocabOf
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
3 (Function)
SMCDEL.Symbolic.K
Dia
SMCDEL.Language
diff
SMCDEL.Explicit.K
diffPointed
SMCDEL.Explicit.K
directed
SMCDEL.Internal.TexDisplay
dis
SMCDEL.Symbolic.S5_DD
Disj
1 (Data Constructor)
SMCDEL.Explicit.DEMO_S5
2 (Data Constructor)
SMCDEL.Language
disp
SMCDEL.Internal.TexDisplay
dispDot
SMCDEL.Internal.TexDisplay
disSet
SMCDEL.Symbolic.S5_DD
distinctVal
SMCDEL.Explicit.K
distRel
SMCDEL.Explicit.K
distribute
SMCDEL.Examples.RussianCards
distribute331
SMCDEL.Examples.RussianCards
dix
SMCDEL.Other.Planning
Dk
SMCDEL.Language
Dkw
SMCDEL.Language
dm
SMCDEL.Examples.DoorMat
dmCoop
SMCDEL.Examples.DoorMat
dmCoop2
SMCDEL.Examples.DoorMat
dmGoal
SMCDEL.Examples.DoorMat
dmPlan2
SMCDEL.Examples.DoorMat
dmResult
SMCDEL.Examples.DoorMat
dmResultBob
SMCDEL.Examples.DoorMat
dmResultBobKripke
SMCDEL.Examples.DoorMat
dmResultKripke
SMCDEL.Examples.DoorMat
dmStart
SMCDEL.Examples.DoorMat
dmTask
SMCDEL.Examples.DoorMat
Do
SMCDEL.Other.Planning
doCall
1 (Function)
SMCDEL.Examples.GossipS5
2 (Function)
SMCDEL.Examples.GossipKw
doCalls
SMCDEL.Examples.GossipKw
done
SMCDEL.Examples.Toynabi
dont
SMCDEL.Explicit.DEMO_S5
dontChange
SMCDEL.Examples.RussianCards
dot2tex
SMCDEL.Internal.TexDisplay
dot2texDefaultArgs
SMCDEL.Internal.TexDisplay
Dubbel
1 (Type/Class)
SMCDEL.Internal.TaggedBDD
2 (Type/Class)
SMCDEL.Symbolic.Ki
3 (Type/Class)
SMCDEL.Symbolic.K
Dyn
SMCDEL.Language
DynamicOp
SMCDEL.Language
eGrAnLaw
SMCDEL.Examples
empty
SMCDEL.Examples.MuddyChildren
emptyRelBdd
1 (Function)
SMCDEL.Internal.TaggedBDD
2 (Function)
SMCDEL.Symbolic.Ki
3 (Function)
SMCDEL.Symbolic.K
endOf
SMCDEL.Examples.Prisoners
endtab
SMCDEL.Internal.TexDisplay
ensureDistinctVal
SMCDEL.Translations.K
EpistM
SMCDEL.Explicit.DEMO_S5
equ
SMCDEL.Symbolic.S5_DD
Equi
SMCDEL.Language
equivalentWith
SMCDEL.Translations.S5
equivExtraVocabOf
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
3 (Function)
SMCDEL.Symbolic.K
Erel
SMCDEL.Internal.Help
eval
1 (Function)
SMCDEL.Explicit.S5
2 (Function)
SMCDEL.Explicit.K
3 (Function)
SMCDEL.Other.MCTRIANGLE
4 (Function)
SMCDEL.Symbolic.S5
5 (Function)
SMCDEL.Symbolic.S5_DD
evaluateFun
SMCDEL.Symbolic.S5_DD
evalViaBdd
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
3 (Function)
SMCDEL.Symbolic.Ki
4 (Function)
SMCDEL.Symbolic.K
evalViaBddReduce
1 (Function)
SMCDEL.Symbolic.Ki
2 (Function)
SMCDEL.Symbolic.K
Event
1 (Type/Class)
SMCDEL.Symbolic.S5
2 (Type/Class)
SMCDEL.Symbolic.S5_DD
3 (Type/Class)
SMCDEL.Symbolic.Ki
4 (Type/Class)
SMCDEL.Symbolic.K
eventToAction
1 (Function)
SMCDEL.Translations.S5
2 (Function)
SMCDEL.Translations.K
eventToActionMulti
SMCDEL.Translations.S5
everyoneKnows
SMCDEL.Other.MCTRIANGLE
everyoneKnowsWhetherNSApaid
SMCDEL.Examples.DiningCrypto
exampleBelScn
SMCDEL.Examples.SimpleK
exampleBlTresult
SMCDEL.Examples.SimpleK
exampleEvent
1 (Function)
SMCDEL.Examples.SimpleK
2 (Function)
SMCDEL.Examples.SimpleS5
exampleGenActM
SMCDEL.Examples.SimpleK
exampleGrAnnEvent
SMCDEL.Examples
exampleGroupAnnounceAction
SMCDEL.Examples
exampleModel
SMCDEL.Examples.SimpleK
examplePaAction
SMCDEL.Examples
examplePointedActM
SMCDEL.Examples.SimpleK
examplePointedModel
SMCDEL.Examples.SimpleK
exampleResult
1 (Function)
SMCDEL.Examples.SimpleK
2 (Function)
SMCDEL.Examples.Toynabi
3 (Function)
SMCDEL.Examples.SimpleS5
exampleStart
1 (Function)
SMCDEL.Examples.SimpleK
2 (Function)
SMCDEL.Examples.SimpleS5
execute
SMCDEL.Other.Planning
Exists
SMCDEL.Language
existsSet
SMCDEL.Symbolic.S5_DD
expert
1 (Function)
SMCDEL.Examples.GossipS5
2 (Function)
SMCDEL.Examples.GossipKw
explain
1 (Function)
SMCDEL.Examples.Toynabi
2 (Function)
SMCDEL.Examples.LetterPassing
3 (Function)
SMCDEL.Examples.DoorMat
explainState
1 (Function)
SMCDEL.Examples.Cheryl
2 (Function)
SMCDEL.Examples.Toynabi
father
SMCDEL.Examples.MuddyChildren
fatherN
SMCDEL.Explicit.DEMO_S5
findPlan
SMCDEL.Other.Planning
findSequentialIcPlan
SMCDEL.Other.Planning
findSequentialIcPlanBFS
SMCDEL.Other.Planning
findStateMap
SMCDEL.Translations.S5
flipOverAndShowTo
SMCDEL.Examples.SimpleK
flipRandomAndShowTo
SMCDEL.Examples.CoinFlip
flipRelBdd
SMCDEL.Other.Planning
for
SMCDEL.Examples.LetterPassing
Forall
SMCDEL.Language
forallSet
SMCDEL.Symbolic.S5_DD
Form
SMCDEL.Language
formOf
1 (Function)
SMCDEL.Other.BDD2Form
2 (Function)
SMCDEL.Symbolic.S5_DD
forP
SMCDEL.Examples.LetterPassing
freshp
SMCDEL.Language
fusion
SMCDEL.Internal.Help
genDcCheckForm
SMCDEL.Examples.DiningCrypto
genDcEveryoneKnowsWhetherNSApaid
SMCDEL.Examples.DiningCrypto
genDcKnsInit
SMCDEL.Examples.DiningCrypto
genDcNobodyknowsWhoPaid
SMCDEL.Examples.DiningCrypto
genDcNotwopaid
SMCDEL.Examples.DiningCrypto
genDcReveal
SMCDEL.Examples.DiningCrypto
genDcSomeonepaid
SMCDEL.Examples.DiningCrypto
genDcValid
SMCDEL.Examples.DiningCrypto
generatedSubmodel
1 (Function)
SMCDEL.Explicit.S5
2 (Function)
SMCDEL.Explicit.K
generatedSubstructure
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
genGraphWith
SMCDEL.Symbolic.S5_DD
getActuals
SMCDEL.Internal.TexDisplay
getEdges
SMCDEL.Internal.TexDisplay
getNodes
SMCDEL.Internal.TexDisplay
gossipers
SMCDEL.Examples.GossipS5
gossipInit
1 (Function)
SMCDEL.Examples.GossipS5
2 (Function)
SMCDEL.Examples.GossipKw
Group
1 (Type/Class)
SMCDEL.Language
2 (Data Constructor)
SMCDEL.Language
groupAnnounceAction
SMCDEL.Examples
groupRel
SMCDEL.Explicit.K
groupSortWith
SMCDEL.Internal.Help
has
SMCDEL.Examples.GossipS5
HasAgents
SMCDEL.Language
hasCard
SMCDEL.Examples.RussianCards
hasHand
SMCDEL.Examples.RussianCards
HasPerspective
SMCDEL.Other.Planning
HasPrecondition
SMCDEL.Language
hasSof
SMCDEL.Examples.GossipS5
HasVocab
SMCDEL.Language
HasWorlds
SMCDEL.Explicit.S5
haveSameAgents
SMCDEL.Language
ICPlan
SMCDEL.Other.Planning
icSolves
SMCDEL.Other.Planning
IfThenElse
SMCDEL.Other.Planning
ifthenelse
SMCDEL.Symbolic.S5_DD
imp
SMCDEL.Symbolic.S5_DD
Impl
SMCDEL.Language
impl
SMCDEL.Explicit.DEMO_S5
inCall
SMCDEL.Examples.GossipKw
Info
SMCDEL.Explicit.DEMO_S5
initM
SMCDEL.Explicit.DEMO_S5
initN
SMCDEL.Explicit.DEMO_S5
inSecT
SMCDEL.Examples.GossipKw
intersection
SMCDEL.Internal.Help
is
SMCDEL.Examples.Cheryl
isBdd
SMCDEL.Examples.Cheryl
isLocalFor
SMCDEL.Other.Planning
isNowInterviewed
SMCDEL.Examples.Prisoners
IsPlan
SMCDEL.Other.Planning
isSuccess
SMCDEL.Examples.GossipS5
isTrue
1 (Function)
SMCDEL.Explicit.DEMO_S5
2 (Function)
SMCDEL.Language
isTrueAt
SMCDEL.Explicit.DEMO_S5
ite
SMCDEL.Language
K
SMCDEL.Language
Kind
SMCDEL.Other.MCTRIANGLE
Kn
SMCDEL.Explicit.DEMO_S5
kn
SMCDEL.Explicit.DEMO_S5
knowN
SMCDEL.Explicit.DEMO_S5
knows
SMCDEL.Examples.MuddyChildren
KnowScene
1 (Type/Class)
SMCDEL.Symbolic.S5
2 (Type/Class)
SMCDEL.Symbolic.S5_DD
KnowSelf
SMCDEL.Other.MCTRIANGLE
KnowStruct
1 (Type/Class)
SMCDEL.Symbolic.S5
2 (Type/Class)
SMCDEL.Symbolic.S5_DD
KnowTransformer
1 (Type/Class)
SMCDEL.Symbolic.S5
2 (Type/Class)
SMCDEL.Symbolic.S5_DD
KnS
1 (Data Constructor)
SMCDEL.Symbolic.S5
2 (Data Constructor)
SMCDEL.Symbolic.S5_DD
knsA
SMCDEL.Examples
knsB
SMCDEL.Examples
knsToKripke
SMCDEL.Translations.S5
knsToKripkeMulti
SMCDEL.Translations.S5
knsToKripkeWithG
SMCDEL.Translations.S5
KnTrf
1 (Data Constructor)
SMCDEL.Symbolic.S5
2 (Data Constructor)
SMCDEL.Symbolic.S5_DD
knWhich
SMCDEL.Examples.Cheryl
KripkeLike
SMCDEL.Internal.TexDisplay
KripkeModel
SMCDEL.Explicit.K
KripkeModelS5
SMCDEL.Explicit.S5
kripkeToBls
SMCDEL.Translations.K
kripkeToBlsUnsafe
SMCDEL.Translations.K
kripkeToKns
SMCDEL.Translations.S5
kripkeToKnsMulti
SMCDEL.Translations.S5
kripkeToKnsWithG
SMCDEL.Translations.S5
KrM
SMCDEL.Explicit.K
KrMS5
SMCDEL.Explicit.S5
kv
SMCDEL.Examples.Cheryl
Kw
SMCDEL.Language
Labelled
SMCDEL.Other.Planning
letter
SMCDEL.Examples.LetterPassing
letterGoal
SMCDEL.Examples.LetterPassing
letterLine
SMCDEL.Examples.LetterPassing
letterPass
SMCDEL.Examples.LetterPassing
letterStart
SMCDEL.Examples.LetterPassing
letterStartFor
SMCDEL.Examples.LetterPassing
lfp
SMCDEL.Internal.Help
light
SMCDEL.Examples.Prisoners
lightSeenByOne
SMCDEL.Examples.Prisoners
makeFalseShowTo
SMCDEL.Examples.SimpleS5
McFormula
SMCDEL.Other.MCTRIANGLE
McM
SMCDEL.Other.MCTRIANGLE
McModel
SMCDEL.Other.MCTRIANGLE
mcModel
SMCDEL.Other.MCTRIANGLE
mcUpdate
SMCDEL.Other.MCTRIANGLE
minimizedKNS
SMCDEL.Examples
minimizedModel
SMCDEL.Examples
Mo
SMCDEL.Explicit.DEMO_S5
modelA
SMCDEL.Examples
modelB
SMCDEL.Examples
monthIs
SMCDEL.Examples.Cheryl
mudBelScnInit
SMCDEL.Examples.MuddyChildren
Muddy
SMCDEL.Other.MCTRIANGLE
mudGenKrpInit
SMCDEL.Examples.MuddyChildren
mudKns2
SMCDEL.Examples.MuddyChildren
mudScn0
SMCDEL.Examples.MuddyChildren
mudScn1
SMCDEL.Examples.MuddyChildren
mudScn2
SMCDEL.Examples.MuddyChildren
mudScnInit
SMCDEL.Examples.MuddyChildren
multiplier
SMCDEL.Internal.TaggedBDD
MultipointedActionModel
SMCDEL.Explicit.K
MultipointedActionModelS5
SMCDEL.Explicit.S5
MultipointedBelScene
1 (Type/Class)
SMCDEL.Symbolic.Ki
2 (Type/Class)
SMCDEL.Symbolic.K
MultipointedEvent
1 (Type/Class)
SMCDEL.Symbolic.S5
2 (Type/Class)
SMCDEL.Symbolic.S5_DD
3 (Type/Class)
SMCDEL.Symbolic.Ki
4 (Type/Class)
SMCDEL.Symbolic.K
MultipointedKnowScene
1 (Type/Class)
SMCDEL.Symbolic.S5
2 (Type/Class)
SMCDEL.Symbolic.S5_DD
MultipointedModel
SMCDEL.Explicit.K
MultipointedModelS5
SMCDEL.Explicit.S5
mv
1 (Function)
SMCDEL.Internal.TaggedBDD
2 (Function)
SMCDEL.Symbolic.Ki
3 (Function)
SMCDEL.Symbolic.K
mvBdd
1 (Function)
SMCDEL.Symbolic.Ki
2 (Function)
SMCDEL.Symbolic.K
mvP
1 (Function)
SMCDEL.Symbolic.Ki
2 (Function)
SMCDEL.Symbolic.K
myEvent
1 (Function)
SMCDEL.Examples.SimpleK
2 (Function)
SMCDEL.Examples.SimpleS5
myKNS
SMCDEL.Examples
myMudBelScnInit
SMCDEL.Examples.MuddyChildren
myMudGenKrpInit
SMCDEL.Examples.MuddyChildren
myMudScnInit
SMCDEL.Examples.MuddyChildren
myOtherEvent
SMCDEL.Examples.SimpleK
myPropu
SMCDEL.Examples
myResult
SMCDEL.Examples.SimpleS5
myStart
SMCDEL.Examples.SimpleS5
MyWorld
SMCDEL.Examples.CherylDemo
n
1 (Function)
SMCDEL.Examples.Prisoners
2 (Function)
SMCDEL.Examples.GossipKw
nCards
SMCDEL.Examples.RussianCards
nCardsGiven
SMCDEL.Examples.RussianCards
nCardsUnique
SMCDEL.Examples.RussianCards
Neg
1 (Data Constructor)
SMCDEL.Language
2 (Data Constructor)
SMCDEL.Other.MCTRIANGLE
neg
SMCDEL.Symbolic.S5_DD
newline
SMCDEL.Internal.TexDisplay
Ng
SMCDEL.Explicit.DEMO_S5
nmbr
SMCDEL.Examples.SumAndProduct
nobodyknows
1 (Function)
SMCDEL.Other.MCTRIANGLE
2 (Function)
SMCDEL.Examples.MuddyChildren
nobodyknowsWhoPaid
SMCDEL.Examples.DiningCrypto
noChange
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
3 (Function)
SMCDEL.Symbolic.K
nodeAts
SMCDEL.Internal.TexDisplay
noDoubles
SMCDEL.Examples.RussianCards
nonobsVocabOf
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
3 (Function)
SMCDEL.Symbolic.K
NotKnowSelf
SMCDEL.Other.MCTRIANGLE
notwopaid
SMCDEL.Examples.DiningCrypto
numberOfStates
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
obsFor
SMCDEL.Other.MCTRIANGLE
obsnobs
SMCDEL.Translations.S5
OfflinePlan
SMCDEL.Other.Planning
offlineSearch
SMCDEL.Other.Planning
oneOf
SMCDEL.Language
Optimizable
SMCDEL.Language
optimize
SMCDEL.Language
Owned
SMCDEL.Other.Planning
P
SMCDEL.Language
PA
SMCDEL.Explicit.DEMO_S5
pairs
SMCDEL.Examples.SumAndProduct
Partition
SMCDEL.Explicit.S5
PAW
SMCDEL.Explicit.DEMO_S5
pdfTo
SMCDEL.Internal.TexDisplay
pickHandsNoCrossing
SMCDEL.Examples.RussianCards
pIs
SMCDEL.Examples.SumAndProduct
Plan
SMCDEL.Other.Planning
play
SMCDEL.Examples.Toynabi
Pointed
SMCDEL.Language
PointedActionModel
SMCDEL.Explicit.K
PointedActionModelS5
SMCDEL.Explicit.S5
PointedModel
SMCDEL.Explicit.K
PointedModelS5
SMCDEL.Explicit.S5
posFor
SMCDEL.Other.MCTRIANGLE
posFrom
SMCDEL.Other.MCTRIANGLE
possibilities
SMCDEL.Examples.Cheryl
Possibility
SMCDEL.Examples.Cheryl
possibleHands
SMCDEL.Examples.RussianCards
possibleHandsN
SMCDEL.Examples.RussianCards
post
SMCDEL.Explicit.K
PostCondition
1 (Type/Class)
SMCDEL.Explicit.S5
2 (Type/Class)
SMCDEL.Explicit.K
powerList
SMCDEL.Explicit.DEMO_S5
powerset
SMCDEL.Internal.Help
pp
SMCDEL.Examples.SallyAnne
ppForm
SMCDEL.Language
ppFormWith
SMCDEL.Language
ppICPlan
SMCDEL.Other.Planning
pProps
SMCDEL.Examples.SumAndProduct
pre
SMCDEL.Explicit.K
preCheck
SMCDEL.Language
preOf
SMCDEL.Language
prisonAction
SMCDEL.Examples.Prisoners
prisonExpStart
SMCDEL.Examples.Prisoners
prisonExpStory
SMCDEL.Examples.Prisoners
prisonGoal
SMCDEL.Examples.Prisoners
prisonInterview
SMCDEL.Examples.Prisoners
prisonSymEvent
SMCDEL.Examples.Prisoners
prisonSymInterview
SMCDEL.Examples.Prisoners
prisonSymStart
SMCDEL.Examples.Prisoners
prisonSymStory
SMCDEL.Examples.Prisoners
problemKNS
SMCDEL.Examples.SimpleS5
problemPM
SMCDEL.Examples.SimpleS5
PropList
1 (Type/Class)
SMCDEL.Explicit.S5
2 (Data Constructor)
SMCDEL.Explicit.S5
propRel2bdd
SMCDEL.Symbolic.K
propsInForm
SMCDEL.Language
propsInForms
SMCDEL.Language
Propulation
SMCDEL.Symbolic.S5
Prp
1 (Data Constructor)
SMCDEL.Explicit.DEMO_S5
2 (Type/Class)
SMCDEL.Language
PrpF
SMCDEL.Language
PubAnnounce
SMCDEL.Language
pubAnnounceAction
SMCDEL.Examples
pubAnnounceStack
SMCDEL.Language
PubAnnounceW
SMCDEL.Language
pubAnnounceWhetherStack
SMCDEL.Language
publicAnnounce
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
publicMakeFalse
SMCDEL.Examples.SimpleS5
publicMakeFalseActM
SMCDEL.Examples.SimpleK
publicMakeFalseTrf
SMCDEL.Examples.SimpleK
Qf
SMCDEL.Other.MCTRIANGLE
qq
SMCDEL.Examples.SallyAnne
Quadrupel
SMCDEL.Internal.TaggedBDD
Quantifier
SMCDEL.Other.MCTRIANGLE
randomboolformWith
SMCDEL.Language
randomPartFor
SMCDEL.Explicit.S5
rcAllChecks
SMCDEL.Examples.RussianCards
rcCards
SMCDEL.Examples.RussianCards
rcCheck
SMCDEL.Examples.RussianCards
rcExplain
SMCDEL.Examples.RussianCards
rcGoal
SMCDEL.Examples.RussianCards
rcNumOf
SMCDEL.Examples.RussianCards
rcPlan
SMCDEL.Examples.RussianCards
rcPlayers
SMCDEL.Examples.RussianCards
rcProps
SMCDEL.Examples.RussianCards
rcSolutions
SMCDEL.Examples.RussianCards
rcSolutionsViaPlanning
SMCDEL.Examples.RussianCards
reaches
SMCDEL.Other.Planning
reachesOn
SMCDEL.Other.Planning
reduce
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
3 (Function)
SMCDEL.Symbolic.Ki
4 (Function)
SMCDEL.Symbolic.K
redundantModel
SMCDEL.Examples
rel
1 (Function)
SMCDEL.Explicit.DEMO_S5
2 (Function)
SMCDEL.Explicit.K
relabel
SMCDEL.Symbolic.S5_DD
relabelWith
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
RelBDD
1 (Type/Class)
SMCDEL.Symbolic.Ki
2 (Type/Class)
SMCDEL.Symbolic.K
relBddOfIn
SMCDEL.Symbolic.K
relOfIn
SMCDEL.Explicit.K
removeDoubleSpaces
SMCDEL.Internal.TexDisplay
replaceEquivExtra
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
3 (Function)
SMCDEL.Symbolic.K
replaceWithIn
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
3 (Function)
SMCDEL.Symbolic.K
replPsInF
SMCDEL.Language
replPsInP
SMCDEL.Language
restrict
1 (Function)
SMCDEL.Internal.Help
2 (Function)
SMCDEL.Symbolic.S5_DD
restrictSet
SMCDEL.Symbolic.S5_DD
reveal
SMCDEL.Examples.DiningCrypto
revealTransformer
SMCDEL.Examples.Cheryl
round1
SMCDEL.Examples.Cheryl
round2
SMCDEL.Examples.Cheryl
round3
SMCDEL.Examples.Cheryl
rtc
SMCDEL.Internal.Help
runAndWait
SMCDEL.Internal.TexDisplay
runIgnoreAndWait
SMCDEL.Internal.TexDisplay
rusBelScnfor
SMCDEL.Examples.RussianCards
RusCardProblem
SMCDEL.Examples.RussianCards
rusKNS
SMCDEL.Examples.RussianCards
rusSCN
SMCDEL.Examples.RussianCards
rusSCNfor
SMCDEL.Examples.RussianCards
safeHandLists
SMCDEL.Examples.RussianCards
safepost
1 (Function)
SMCDEL.Explicit.S5
2 (Function)
SMCDEL.Explicit.K
sallyComesBack
SMCDEL.Examples.SallyAnne
sallyFinal
SMCDEL.Examples.SallyAnne
sallyFinalCheck
SMCDEL.Examples.SallyAnne
sallyInit
SMCDEL.Examples.SallyAnne
sallyIntermediate1
SMCDEL.Examples.SallyAnne
sallyIntermediate2
SMCDEL.Examples.SallyAnne
sallyIntermediate3
SMCDEL.Examples.SallyAnne
sallyIntermediate4
SMCDEL.Examples.SallyAnne
sallyLeaves
SMCDEL.Examples.SallyAnne
sallyPutsMarbleInBasket
SMCDEL.Examples.SallyAnne
samplerel
SMCDEL.Symbolic.K
sanityCheck
SMCDEL.Internal.Sanity
sapAllProps
SMCDEL.Examples.SumAndProduct
sapExplainState
SMCDEL.Examples.SumAndProduct
sapForm1
SMCDEL.Examples.SumAndProduct
sapForm2
SMCDEL.Examples.SumAndProduct
sapForm3
SMCDEL.Examples.SumAndProduct
sapKnows
SMCDEL.Examples.SumAndProduct
sapKnStruct
SMCDEL.Examples.SumAndProduct
sapProtocol
SMCDEL.Examples.SumAndProduct
sapSolutions
SMCDEL.Examples.SumAndProduct
satCountWith
SMCDEL.Symbolic.S5_DD
Semantics
SMCDEL.Language
set
SMCDEL.Internal.Help
seteq
SMCDEL.Internal.Help
SF
SMCDEL.Language
shareknow
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
shiftPrepare
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
3 (Function)
SMCDEL.Symbolic.Ki
4 (Function)
SMCDEL.Symbolic.K
showme
SMCDEL.Other.MCTRIANGLE
showSet
SMCDEL.Language
shrinkform
SMCDEL.Language
SimplifiedForm
SMCDEL.Language
simplify
SMCDEL.Language
simStep
SMCDEL.Language
sIs
SMCDEL.Examples.SumAndProduct
size
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
sizeOf
SMCDEL.Symbolic.S5_DD
smartKripkeToKns
SMCDEL.Translations.S5
smartKripkeToKnsWithoutChecks
SMCDEL.Translations.S5
solveN
SMCDEL.Explicit.DEMO_S5
some
SMCDEL.Other.MCTRIANGLE
someonepaid
SMCDEL.Examples.DiningCrypto
sortL
SMCDEL.Explicit.DEMO_S5
sProps
SMCDEL.Examples.SumAndProduct
start
1 (Function)
SMCDEL.Examples.CherylDemo
2 (Function)
SMCDEL.Examples.Cheryl
State
1 (Type/Class)
SMCDEL.Other.MCTRIANGLE
2 (Type/Class)
SMCDEL.Symbolic.S5
3 (Type/Class)
SMCDEL.Symbolic.S5_DD
StateMap
SMCDEL.Translations.S5
statesOf
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
3 (Function)
SMCDEL.Symbolic.Ki
4 (Function)
SMCDEL.Symbolic.K
Status
SMCDEL.Explicit.K
StatusMap
SMCDEL.Explicit.K
step
SMCDEL.Other.MCTRIANGLE
step1
1 (Function)
SMCDEL.Examples.CherylDemo
2 (Function)
SMCDEL.Examples.Cheryl
step2
1 (Function)
SMCDEL.Examples.CherylDemo
2 (Function)
SMCDEL.Examples.Cheryl
step3
1 (Function)
SMCDEL.Examples.CherylDemo
2 (Function)
SMCDEL.Examples.Cheryl
step4
1 (Function)
SMCDEL.Examples.CherylDemo
2 (Function)
SMCDEL.Examples.Cheryl
step5
1 (Function)
SMCDEL.Examples.CherylDemo
2 (Function)
SMCDEL.Examples.Cheryl
Stop
SMCDEL.Other.Planning
Story
1 (Type/Class)
SMCDEL.Examples.Prisoners
2 (Data Constructor)
SMCDEL.Examples.Prisoners
sub
SMCDEL.Explicit.DEMO_S5
subformulas
SMCDEL.Language
subseteq
SMCDEL.Internal.Help
substit
1 (Function)
SMCDEL.Language
2 (Function)
SMCDEL.Symbolic.S5_DD
substitOutOf
SMCDEL.Language
substitSet
SMCDEL.Language
substitSimul
SMCDEL.Symbolic.S5_DD
succeeds
SMCDEL.Examples.GossipKw
svg
SMCDEL.Internal.TexDisplay
svgViaTex
SMCDEL.Internal.TexDisplay
TagBdd
1 (Type/Class)
SMCDEL.Symbolic.Ki
2 (Type/Class)
SMCDEL.Symbolic.K
tagBddEval
1 (Function)
SMCDEL.Internal.TaggedBDD
2 (Function)
SMCDEL.Symbolic.Ki
3 (Function)
SMCDEL.Symbolic.K
TagForBDDs
SMCDEL.Internal.TaggedBDD
Task
1 (Type/Class)
SMCDEL.Other.Planning
2 (Data Constructor)
SMCDEL.Other.Planning
tc
SMCDEL.Internal.Help
tell
SMCDEL.Examples.Toynabi
tex
SMCDEL.Internal.TexDisplay
TexAble
SMCDEL.Internal.TexDisplay
texBDD
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
texBddWith
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
texDocumentTo
SMCDEL.Internal.TexDisplay
texForm
SMCDEL.Language
texRelBDD
1 (Function)
SMCDEL.Symbolic.Ki
2 (Function)
SMCDEL.Symbolic.K
textDot
SMCDEL.Internal.TexDisplay
texTo
SMCDEL.Internal.TexDisplay
thirdEvent
SMCDEL.Examples.SimpleS5
thirdResult
SMCDEL.Examples.SimpleS5
thirstyCheck
SMCDEL.Examples.DrinkLogic
thirstyF
SMCDEL.Examples.DrinkLogic
thirstyScene
SMCDEL.Examples.DrinkLogic
thisCallProp
SMCDEL.Examples.GossipS5
thisPos
SMCDEL.Examples.Cheryl
toBeExchangedT
SMCDEL.Examples.GossipKw
toGraph
SMCDEL.Internal.TexDisplay
Top
1 (Data Constructor)
SMCDEL.Explicit.DEMO_S5
2 (Data Constructor)
SMCDEL.Language
top
SMCDEL.Symbolic.S5_DD
toPlay
SMCDEL.Examples.Toynabi
totalRelBdd
1 (Function)
SMCDEL.Internal.TaggedBDD
2 (Function)
SMCDEL.Symbolic.Ki
3 (Function)
SMCDEL.Symbolic.K
toynabi
SMCDEL.Examples.Toynabi
toynabiGoal
SMCDEL.Examples.Toynabi
toynabiStartFor
SMCDEL.Examples.Toynabi
toyPlan
SMCDEL.Examples.MuddyPlanning
Transformer
1 (Type/Class)
SMCDEL.Symbolic.Ki
2 (Type/Class)
SMCDEL.Symbolic.K
transformerToActionModelWithG
SMCDEL.Translations.S5
tResult
SMCDEL.Examples.SimpleK
tResult2
SMCDEL.Examples.SimpleK
Trf
1 (Data Constructor)
SMCDEL.Symbolic.Ki
2 (Data Constructor)
SMCDEL.Symbolic.K
trfPost
1 (Function)
SMCDEL.Symbolic.Ki
2 (Function)
SMCDEL.Symbolic.K
Tripel
SMCDEL.Internal.TaggedBDD
truthsInAt
SMCDEL.Explicit.K
tryTake
SMCDEL.Examples.DoorMat
tryTakeL
SMCDEL.Examples.DoorMat
tt
SMCDEL.Examples.SallyAnne
uncp
1 (Function)
SMCDEL.Symbolic.Ki
2 (Function)
SMCDEL.Symbolic.K
uniqueVals
SMCDEL.Translations.S5
unmv
1 (Function)
SMCDEL.Symbolic.Ki
2 (Function)
SMCDEL.Symbolic.K
unmvBdd
1 (Function)
SMCDEL.Internal.TaggedBDD
2 (Function)
SMCDEL.Symbolic.Ki
3 (Function)
SMCDEL.Symbolic.K
unmvcpP
1 (Function)
SMCDEL.Symbolic.Ki
2 (Function)
SMCDEL.Symbolic.K
unsafeUpdate
SMCDEL.Language
Update
SMCDEL.Language
update
SMCDEL.Language
updates
SMCDEL.Language
updateSequence
SMCDEL.Language
updPa
SMCDEL.Explicit.DEMO_S5
updPaW
SMCDEL.Explicit.DEMO_S5
updPc
SMCDEL.Explicit.DEMO_S5
updPi
SMCDEL.Explicit.DEMO_S5
updsPa
SMCDEL.Explicit.DEMO_S5
updsPaW
SMCDEL.Explicit.DEMO_S5
updsPc
SMCDEL.Explicit.DEMO_S5
valid
SMCDEL.Explicit.S5
validViaBdd
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
3 (Function)
SMCDEL.Symbolic.Ki
4 (Function)
SMCDEL.Symbolic.K
valueIn
SMCDEL.Examples.Cheryl
Var
SMCDEL.Examples.Cheryl
Variable
SMCDEL.Examples.Cheryl
ViaDot
1 (Type/Class)
SMCDEL.Internal.TexDisplay
2 (Data Constructor)
SMCDEL.Internal.TexDisplay
vocab
SMCDEL.Examples.Toynabi
vocabOf
SMCDEL.Language
wasInterviewed
SMCDEL.Examples.Prisoners
weKnowIt
SMCDEL.Examples.CherylDemo
whereViaBdd
1 (Function)
SMCDEL.Symbolic.S5
2 (Function)
SMCDEL.Symbolic.S5_DD
whoKnowsMeta
1 (Function)
SMCDEL.Examples.GossipS5
2 (Function)
SMCDEL.Examples.GossipKw
whoKnowsWhat
SMCDEL.Examples.GossipKw
willExchangeT
SMCDEL.Examples.GossipKw
withoutProps
1 (Function)
SMCDEL.Explicit.S5
2 (Function)
SMCDEL.Symbolic.S5
3 (Function)
SMCDEL.Symbolic.S5_DD
4 (Function)
SMCDEL.Symbolic.K
withoutWorld
1 (Function)
SMCDEL.Explicit.S5
2 (Function)
SMCDEL.Explicit.K
World
SMCDEL.Explicit.S5
worldsOf
SMCDEL.Explicit.S5
Wrap
1 (Data Constructor)
SMCDEL.Symbolic.S5
2 (Data Constructor)
SMCDEL.Symbolic.S5_DD
WrapBdd
1 (Type/Class)
SMCDEL.Symbolic.S5
2 (Type/Class)
SMCDEL.Symbolic.S5_DD
wsBound
SMCDEL.Examples.WhatSum
wsExplainState
SMCDEL.Examples.WhatSum
wsKnowSelfA
SMCDEL.Examples.WhatSum
wsKnowSelfB
SMCDEL.Examples.WhatSum
wsKnowSelfC
SMCDEL.Examples.WhatSum
wsKnStruct
SMCDEL.Examples.WhatSum
wsResult
SMCDEL.Examples.WhatSum
wsSolutions
SMCDEL.Examples.WhatSum
wsTriples
SMCDEL.Examples.WhatSum
xIs
SMCDEL.Examples.SumAndProduct
Xor
SMCDEL.Language
xorSet
SMCDEL.Symbolic.S5_DD
xProps
SMCDEL.Examples.SumAndProduct
xyAre
SMCDEL.Examples.SumAndProduct
yIs
SMCDEL.Examples.SumAndProduct
yProps
SMCDEL.Examples.SumAndProduct
|=
SMCDEL.Language