Advanced Lua

If you haven't read the Lua and formulas page, it is strongly recommended to do so first.

In addition to the creation of theories, and subsequently testing provability and satisfiability, the Lua interface provides a set of additional capabilities, which will be addressed in this page.

Formula substitution

It is possible to create a formula template in Lua, and subsequently substitute parts of it with the desired values. To do this, create a formula using oops.Formula(formula). In this formula, it is possible to define variables using uppercase characters (A-Z). If no variables are defined, the return value of these will act exactly the same as if you typed it in directly as an argument to one of the theory methods.

Once a template formula is made, calling the substitute(formulaSubstitutions, agentSubsitutions), will substitite the given forumas and agents (in the format of {Variable1 = Value1[,  Variable2 = Value2]}, etc) and will return the new formula.

An example of this:

f = oops.Formula("#_I A"):substitute({A = "a"}, {I = "1"})

This will create a formula "#_I A" with the variables I and A, and subsequently substitutes these by replacing the formula A with a and the agent I with 1, resulting in the formula #_1 a.

Changing prover

Using a simple Lua function it is possible to change the current prover to another one at any time. To do so, just call oops.setProver(name), with the name of the new axiom system to use (i.e. oops.setProver("S5")). If desired it is possible to obtain a list of available provers using oops.getProvers(), this will return an array with all available provers.

An example of a way to display all provers in the console is shown below:

provers = oops.getProvers()

for k,v in pairs(provers) do
     print(v)
end

Attaching visualizers

It is sometimes more interesting to see why a formula can or cannot be proven, instead of just getting true or false as a response. Therefore, it is possible to attach visualizers to OOPS.

There are currently three visualizers available:

• Tableau visualizer, which shows the final tableau that was generated by OOPS.
• Tableau solving observer, which shows the solving steps (in the console) that were taking to generate the final tableau.
• Kripke model visualizer, which shows a kripke model of a counter example. (NOTE: Since this shows a counter example, provable formulas will not show a model)

The tableau visualizer can be added very easily, simply add the following line in the editor, before any proving takes place: oops.attachTableauVisualizer(). Once this is done, any call to provable, satisfiable or consistent will bring up a new window showing the tableau that was generated.

Similarly, tableau solving observers can be added in the same fashion, simply call oops.attachTableauObserver() and all tableau steps will be shown in the console.

Finally, adding kripke model visualization requires two steps, first the constructor must be attached, which is done by oops.attachModelConstructor(), and after using provable, satisfiable or consistent, the constructed model can be visualized by calling oops.showModel()

One important thing to remember is that these visualizers are attached to the current prover. Therefore, if the prover is changed (using oops.setProver), the visualizers will need to be attached again.