PROP	P	T	true
		F	false
		Q	agent variables (which may not be T or F) begin with upper case
		~P	negation
		P & P	conjunction
		P | P	disjunction
		(P)	you can use brackets just as you'd expect
		P => P	implication
		[a,...]P	strong necessity
		[-a,...]P	strong complement necessity
		[[a,...]]P	weak necessity
		[[-a,...]]P	weak complement necessity
		<a,...>P	strong possibility
		<-a,...>P	strong complement possibility
		<<a,...>>P	weak possibility
		<<-a,...>>P	weak complement possibility
		[S]P	strong necessity using a set identifier S
		[-S]P	strong complement necessity using a set identifier S
		[[S]]P	weak necessity using a set identifier S
		[[-S]]P	weak complement necessity using a set identifier S
		<S>P	strong possibility using a set identifier S
		<-S>P	strong complement possibility using a set identifier S
		<<S>>P	weak possibility using a set identifier S
		<<-S>>P	weak complement possibility using a set identifier S
		min(X.P)	least fixpoint temporal formula
		max(X.P)	greatest fixpoint temporal formula
		V(Q,...)	parameterised agent

---

Edinburgh Concurrency Workbench (v7.1). Page generated: Sat Jul 17 22:16:15 BST 1999