Title - 
	Formal semantics

Description - 
	Much of the language of the framework specification talks as if WS-Policy is a logic (e.g., reason about, logical construct, etc.) and yet the semantics are specified informally, and in no concentrated place. Furthermore, certain aspects of the semantics seem unspecified (e.g., the precise meaning of exactlyOne; first order exclusive disjunction, that + some sort of close world assumption, etc.).

Justification -  
	Clarity and completeness of a specification are always critical. Formalization does not *always* help clarity, at least for a wide audience, but WS-Policy is simple enough that the semantics should be reasonably accessible to anyone who understands truth tables.

	Secondly, if the semantics are as I believe (roughly propositional logic or a very simple description logic) then we gain access to the wealth of tools and algorithms available for these logics. SAT solvers and DL reasoners are highly optimized and used in all sorts of industrial settings.

	Thirdly, various sorts of analysis become easier if we have a clear semantics. On this page:
		<http://www.mindswap.org/2005/services-policies/>
are some papers and presentations showing how to discover policy containment, equivalence, disjointness, and incoherence.

	Furthermore, certain behaviors of the operators are specified individually (e.g., commutativity, etc.) that would follow from a normal semantics for the operators (e.g., logical and is commutative, etc.) I think this would simplify the spec.

Target - 
	framework

Proposal - 
	Let's consider normal form only for the moment.

	I will do it only propositionally at the moment.

	Policy assertions correspond to propositional variables, aka, atomic sentences. There are an infinite number of them.

		<all>P1...Pj</all> is true just in case for i = 1 to j, Pi is true.
		<exactlyOne>A1...Ak</exactlyOne> is true just in case for some i=1 to k, Ai is true and for an m != i, Am is false.

	(Now, when we introduce a policy subject, the propositional letters become one place predicates, but that is easily handled.)

	Clearly this isn't a lot of text, though there are additional details. I just wanted to give a flavor.

	For example, it's easy to show that <all> is communtative, and associative (the truth conditions are independent of order or grouping)