Note: Analysis

###5.3 Unbound Universal Quantifiers

####5.3.1 Generator Axioms and Exploding Scopes

####5.3.2 Omitting the Generator Axiom

###Question

1. What about

   module analysis/paramSets [t]

2. every relational expression in Alloy has a value

###Feb 28 Class

####Universal existential quantifier

some $x_0, x_1 ... x_{n-1}$ | all $y_0, y_1 ... y_{m-1}$

Using the bound of n will be sufficient.

####The monadic fragment

constraints:

• pred calculus
• only unary relations(K)

Bound: $2^k$

Mar 5 Class

Syntax v.s. Semantics

See my written notes

Mar 7 Class

domain v.s. co-domain:(Universe: 1,2,3,4,5,6…)

• domain: 1 ,2 ,3 ,4 ,5 ,6…
• co-domain: 1, 4, 9, 16…

Instance:

• atoms
• functions
• relations

Propositional logic(boolean logic)

Mar 10 Class

Not symmetric

run 3 expect 1

What about the algorithm for Aluminum?