MAS: Using Priest Modal Tableaux to Visualise Kripke Models
Chapter 5: Conclusions
M. Koonstra S2399385 / G. Schoenmacker s1550748 / Rijksuniversiteit Groningen
Overview of project
We have found that building a proving system is mainly a process of checking. With relative ease we've managed to build a Priest-based system for proving propositional formulae. In fact, this was so simple we were suspicious of the result. Thinking of test case after test case to assure ourselves, we finally found formulae containing a double negation were not expending well. This was the only issue however: in one afternoon we had a working propositional proving system. This dynamic remained visible throughout the project: thinking of rules and solutions was relatively easy: making sure we had thought of everything was difficult.
We've built this prover in stages. As a first step, we've made a propositional prover and tested it to satisfaction. After that, we've extended the system to include the box operator 
and the diamond operator 
for a single agent in system K. This was all according to Priest. After this worked, we expanded the system for multiple agents. This required a complete rewrite of our rule-system and our prover. At this point, we added a method to visualise a model using an external library. This method remained relatively stable throughout the remainder of the project. Because of the external library (which does the hard work of deciding where to place nodes and draw relations), this was doable. Next, we added support for system S5. Lastly, we added the systems KEC and S5EC. Again this required a rewrite because for E and C it is vital that the proving system has access to the number of agents, which was at the time not available to the prover.
We think the modular approach was very important, because it allowed us to test the system step by step and build on things we knew to work. The downside of this approach was the two complete rewrites we mentioned above: if we could have built the system in one go, this could have been avoided.
Problems in the current implementation
The largest problem as we see it, is the possible infinity in system KEC introduced due to the C operator working with the diamond operator. For example, the following formula will result in an unending run in KEC(1):
C M_1 pThe second improvement we would like to see is the reduction of produced models in several different ways. There are three changes we'd like to implement:
- Reduction of duplicate models.
- Reduction of duplicate worlds.
- Allowing premises to be added to a conclusion.
Duplicate models
Currently, the formula a & a (in any system) produces two counter models, which are in fact identical. This is a direct result of the Priest syntactic tableaux method, because the conjunction is expanded to two branches, each representing a counter model. This could be solved by comparing tree branches and is a relatively easy fix. We have decided to keep this behaviour to demonstrate the Priest method, without trying to hide some (perhaps unwanted) side effects.
Duplicate worlds
Currently, the formula ~M_1 a in K(EC) produces a counter model with two worlds, both of which satisfy a. We would like to see the prover realise that in fact it need not add another world, but just adding a relation to the current world in enough to disprove the formula. This is in fact an improvement we've discusses above, because this would (we think) solve the infinity problem.
Allowing premises
At this moment, we only allow a single formula to be entered. The prover then determines whether that formula is a tautology and shows models or counter models. A problem with this we have seen in the three wise men example: we would like to add some knowledge as a premise instead of including it in the formula to prove. Below is the formula we used to conclude that if a wise man sees two blue hats, he knows himself to be wearing a red one:
(C (((b1 & b2) > r3) & ((b2 & b3) > r1) & ((b1 & b3) > r2) & ((b1 & ~r1) | (~b1 & r1)) & ((b2 & ~r2) | (~b2 & r2)) & ((b3 & ~r3) | (~b3 & r3))) & #_1 (b2 & b3)) > #_1 r1In fact 64 out of the 65 counterexamples were useless to us, because they showed how our assumed knowledge might not be true. The counterexamples were logically valid, but still we would rather not see them. Priest's method allows a simple solution to this: simply add formulae as premises to the tree. Then lastly add the negation of the conclusion. This would eliminate tree branches which are in conflict with the premises automatically. The reason we have not implemented this is threefold: firstly we have tried to mimic OOPS-like performance in which the user enters a single formula to see whether it's a tautology or not. Secondly, when we realised this behaviour was present, we realised it was technically correct and showed a nice contraction in formal logic and our expectations. People would very likely not have said "well, the assumption people must have either a red or a blue hat is not valid". Lastly, we lacked the time needed to change our graphical user interface.
To correct this behaviour, we could have added a separate input field for premises and one for the conclusion. Our implementation is such that the reasoning system will accept this without problems, because it follows Priest's tableaux method. For the reasons states above, we have not done so. To demonstrate our program can deal with premises, we have supplied a command-line version which does exactly that.
Conclusions
Building an automatic prover for logic systems is relatively easy. Making sure it's correct is hard. The visualisation was not too difficult because of our usage of an external library. We have some open problems together with some good ideas on how to solve these. Lack of time is the primary reason for not applying those solutions. We think we've achieved the goal we set: to build a logic proof system based on Priest semantic tableaux and to visualise models generated by this.
Previous Chapter: Chapter 4 - Demonstration
Next Chapter: Chapter 6 - Bibliography
