Lua basics
To simplify the usage of OOPS, Lua scripts are used as input, which are then parsed and executed. This Lua interface is build around the concept of a background theory, which is then used as a basis to prove a specific formula.
To create a new theory object, one calls the function oops.Theory(), which will return a new empty theory.
This theory can then be added upon using the add method of this theory, providing formulas to add(formula) to the theory. Once all background theory is added, one can test whether a formula can be proven by calling the provable(formula) method, specifying the formula to try to prove. This method returns true if it is provable, and false otherwise.
To illustrate, here is a simple example of a proof (for explanation of formula syntax, see below):
th = oops.Theory()
th:add("#_1 (a > ~b)")
th:add("#_1 (b > ~a)")
th:add("#_1 a")
print(th:provable("#_1 ~b"))
In this sample, Agent 1 is given the background knowledge that a → ¬b and b → ¬a. And is given the knowledge that a holds. Logically this implies that it knows that b does not hold. The result of the call to provable is, as expected, true. The print function is added to display this result in the console.
In addition to proving formulas, it is also possible to check if formulas are satisfiable, using the satisfiable(formula) method, which works similarly to the provable method. The difference between satisfiability and provability is the way these are handled by the underlying prover. Tableau provers can only test satisfiability of formulas: Whether there is any circumstance (or more accurately, whether there is any kripke model) in which the formula holds. Testing for satisfiability tests the following formula: T1 ∧ ... ∧ Tn ∧ F, where Ti is a formula added to the theory, and F is the formula being tested for satisfiability. When proving a formula however, the following is tested: ¬( (T1 ∧ ... ∧ Tn) → F). This in fact tests whether the opposite of the formula to prove is satisfiable. Since, if a formula is satisfiable, there is no counter example, this approach does just that: find a counter example. If successful, the formula is not provable, otherwise it is.
One last thing that can be done with theories is testing whether or not a theory is consistent. Since any formula can be added to the theory, it is possible to create a theory which itself is not consistent, which makes the results of provability or satisfiability tests unreliable. To test if a theory is consistent, use the consistent() method. This tests whether T1 ∧ ... ∧ Tn holds, and will return true if this is the case, and false otherwise.
Formula syntax
For formulas, OOPS follows the following syntax:
| OOPS symbol |
Logical Symbol |
Description |
| & |
∧ |
Conjunction |
| | |
∨ |
Disjunction |
| ~ |
¬ |
Negation |
| > |
→ |
Implication |
| = |
≡ |
Bi-implication (If and only if) |
| a-z |
a-z |
Propositions |
| A-Z |
N/A |
Variables. These can be used for subsitution (see below) |
| #_i φ |
□i φ |
Knowledge: Agent i knows φ(i must be a number). φ must be a proposition or set of propositions in parentheses. |
| %_i φ |
◊i φ |
Knowledge: Agent i considers it possible that φ. |
| # φ |
∀i∈A□i φ |
Shared knowledge: Every agent knows φ. |
| % φ |
∃i∈A□i φ |
Shared knowledge: There is an agent that knows φ. |
Note that some of these operators are only valid in certain axiom systems. For instance, when using the propositional axiom system, knowledge operators will not be available. Attempting to use these will result in an error, stating the formula failed to validate. This is to ensure unsupported operators are automatically rejected, instead of causing invalid results.
|
