Session 2

! Session 2.md

1. Prisoners

prisoners

vocabulary V{
	type Person := {Jan, Piet, Rob, Dirk, Bob, Wouter}
	Prisoner: Person -> Bool
	Shortterm: Person -> Bool
	Longterm: Person -> Bool
	Sentence: Person -> Int
	VisitRight: Person -> Bool
	Prejudiced: Person -> Bool
	Likes: Person * Person -> Bool
}

theory T: V{
    {!x in Person: Shortterm(x) <- Prisoner(x) & Sentence(x) <6.
     !x in Person: Longterm(x)  <- Prisoner(x) & Sentence(x)>=60.
    }
    !x in Person: Shortterm(x) => VisitRight(x).
    !x in Person: Longterm(x) & (!y in Person: Shortterm(y) => ~ Likes(x,y)) => Prejudiced(x).
    !x,y in Person: Likes(y,x) => ~(Longterm(x) | Shortterm(x)).
    !x,y in Person: ~Longterm(y) & ~Shortterm(y) & ~Longterm(x) & ~Shortterm(x) => Likes(x,y).
    
    !x in Person, y in Int: Sentence(x)=y => Prisoner(x).

}

structure S:V{ 
	Sentence := {Jan->7, Piet->65, Rob->5, Dirk-> 7, Bob-> 30, Wouter-> 18}.
}


procedure main(){
	pretty_print(model_expand(T,S))
    
}