Hi!

We don't have additional documentation on util/boolean other than
what's already in the file.

All util models (except util/ordering, which says so near the top) are just regular models,
so util/boolean should be just the semantics you get if you wrote it in your own model.
Do you have a question about something in util/boolean?

Thanks Felix,

I simply was investigating the suitability of Alloy for teaching purposes. I was asked to look into the possibility of using Alloy to help undergraduate students learn about basics of simple logic.
For example:

Where A,B,C are booleans
Trying to find the value of   ( A & ! A)
A & B = B & A
A II (B & C) = True
...

Although these examples are trivial, but the question is: are basic logic proofs native to Alloy?

--Waël Hassan

Hi: For your students, you can perhaps put the following into
a library module:

   module logic
   one sig True, False { }
   one sig A, B, C, D, E, F, G { value: (True+False) }
   pred a { A.value = True }
   pred b { B.value = True }
   pred c { C.value = True }
   pred d { D.value = True }
   pred e { E.value = True }
   pred f { F.value = True }
   pred g { G.value = True }

Then you can easily play with different logic formulas like this:

   module someExample
   open logic

   // This should be true
   check {  ((a=>b) && (b=>c)) => (a=>c)  }

   // This should be false
   check {  (a && b) <=> (!a && !b)  }

   // This would show a scenario where a implies b, but b does not imply a
   run {  (a=>b) && !(b=>a)  }

Is it at all possible to add more documentation on util/boolean?

Regards,
Barry

----------
Online Petition -=InK=-

Hi Barry: I can attempt to summarize it here:

1) It declares a signature called "Bool" with exactly two atoms "True" and "False"
2) "isTrue" takes a Bool atom, and is satisfied if the atom is "True"
3) "isFalse" takes a Bool atom, and is satisfied if the atom is "False"
4) "Not" takes a Bool atom, and returns the opposite Bool atom
5) "And" takes two Bool atoms, and returns "True" if both are "True"
6) "Or" takes two Bool atoms, and returns "True" if at least one is "True"
7) Likewise for "Xor", "Nand", and "Nor"

I should re-iterate that there is no special semantics involved with util/boolean...

Another minor point: the predicates and functions are all declared
to receive exactly one Bool.  For example, "Not" is defined like so:
        fun Not [b: Bool] : Bool { Bool - b }
But parameter declaration's multiplicity and type are not enforced in Alloy4.
So there's nothing preventing you from passing 0 atom, 2 atoms,
or even non Bool atoms into the function, in which case the function
won't behave as desired. (For example, if you pass the empty set
into Not, you will get back the set containing both True and False atoms!)

Sincerely,
Felix Chang
Alloy4 Developer