@misc{59, author = {Gavin Rens and Tommie Meyer and G. Lakemeyer}, title = {A Sound, Complete and Terminating Decision Procedure for SLAOP}, abstract = {SLAOP is the Speci cation Logic of Actions and Observations with Probability. In this report, we provide the syntax and semantics of SLAOP and then provide a decision procedure for checking validity of sentences. The decision procedure is a tableau method which appeals to solving systems of equations. The tableau rules eliminate propositional connectives, then, for all open branches of the tableau tree, systems of equations are generated and checked for feasibility. We prove that the procedure is sound and complete.}, year = {2013}, }