|CSCI P415/515||Fri Jan 6 15:18:04 EST 2012 [SDJ]|
Andy, Bob, Cindy, Dinah, Eve, Fred, and Gary live in the seven houses, numbered 1 through 7, on Maple Steet. Gary's address is 5 greater than Bob's. Bob's address is greater than Andy's. Dinah's address is less than Eve's, whose address is 2 less than Gary's. Cindy's address is less than either Dinah's or Fred's. Who lives where?
In the PVS formulation, the problem statement, together with some needed background knowledge, are expressed as axioms (assumptions). The solution is represented by a series of lemmas.