2.2 Refinements

By simply translating some of the theory about first order logic and its semantics into Prolog, it was easy to implemement a model checker that can already do a lot of nice things. Yet it has its problems, and they will force us to invest some more thought. Let's see what happens if the input differs in various ways from what we've anticipated.



Aljoscha Burchardt, Stephan Walter, Alexander Koller, Michael Kohlhase, Patrick Blackburn and Johan Bos
Version 1.2.5 (20030212)