Project Description

The purpose of this project was to make a symantic tableaux solver for an S5 (for K) and KD45 (for B) KL system in PHP. (Page 89 of Epistemic Logic for AI and Computer Science) This means the basic KL logical formulas, enhanced with the S5 and KD45 axioms.
To do this, all axioms from these system have to be implemented of course. Additionally, all PHP code for "reading" logic had to be added. A valid question would of course be "why?", the answer is simple, because I could. Writing a tableaux solver gives one a really solid understanding of the principles involved, and because of that, I can recommend it to everyone. One of the main advantages of a "web based" solver is that it removes the need for any shell access to some remote server that has sufficient CPU power, with this, a simple web browser will suffice.

Design

The design makes rougly the following steps:

• Make the initial set of false formulas (The formula we are trying to find a counter model for)
• remove outer brackets from all true and false sets(if any)
• Determine the possible operators for all formulas (The one with the lowest priority)
• Try to find an operator among the sets that does not cause the tree to split
• If the previous fails, try to find an operator that does not create a new world
• If the previous fails, pick any operator that's left
• If that fails too, we are done, and have found a counter model
• If we did get an operator, we now try to apply it. While doing this, we also apply transitivity, D rule, and euclideanity.
• The resulting set is then checked for consistency, if it is inconsistent, we close this branch, when all branches close, the formula must be true

I would say one more thing about the process of making this program, Meeting the requirement for euclideanism, was one of the harder parts, since it required the model to be made in such a way that it allowed one to go up in the set of transitions again. (After all, the implication is that when for example K1a apprears in the "true" set, it must also have been there in any previously reachable worlds (<>A->[]<>A).

The solver can be found: here (password is "mas").

Future work

Possible suggestions for improvement include:

• Put the whole output in a database and let people provide an email when entering their formula, so the system can take as long as it takes, and mail the user a link to obtain the results when done.
• Graphs can be created, all the information is there, though how useful that is remains to be seen due to potentially very large trees.
• Add support for common knowledge, I believe this should not be extremely hard with the current architecture.
• Adding support for unicode logical operators. If there is demand for this feature, it would be exceptionally easy to implement by modifying the routine that currently looks for E and F.