Home » Research » Research outputs » A Sound, Complete and Terminating Decision Procedure for SLAOP

A Sound, Complete and Terminating Decision Procedure for SLAOP

2013

  • Authors:
    Gavin Rens , Tommie Meyer , Lakemeyer, G.

    Publication date:
    2013

    Institution:

    Output type:
    Other

    Abstract:

    SLAOP is the Specication 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.