I've just finished the first major part of my first step along the road to [real] implementation: I now have a working type for propositional calculus, a simple representation of a tableau branch, can saturate said branch (modulo the rules which branch) and generate a model (which is simply a list of literals at this point).
Next, I need to extend this tableau implementation to support branching and then complete the logic with correct rules for branching connectives (disjunction and implication). Once that is done, I'll rewrite my language parser and code generator so that I can actually generate this implementation of the propositional calculus from the definition.
Once that is done, I'll move on to the basic propositional modal logic: K. Getting K to work will require that I implement labels, relations and extend my language so that it can import and extend existing logics. Once that is done, I'll move onto a more complex modal logic (perhaps S4) before tackling intuitionistic logic (which uses two-part labels).
Subscribe to:
Post Comments (Atom)
3 comments:
If you have S4 working, then you can do intuitionistic logic for free... This is because you can faithfully embed intuitionistic logic into S4. The shallow reason for this is that there is a translation which does it, the deep reason has to do with algebra and topology.
The translation is quite simple.
The topology reason can almost be seen just from logic. Kripke proved the completeness of intuitionistic logic relative to partially ordered frames. One can also do it relative to complete Heyting algebras (this is the more common semantics). It is not terribly difficult to prove the two semantics equivalent. So, one can think of Int as partial orders and every partial order is also a preorder so...
Jon: the motivation for implementing the logics I mentioned is as a driver of my development. PC is the most basic logic I can think of, so I've taken it as my initial target. Once I've got that working, I'll aim for K, which will require labels and edges in the relation. After that, S4 will require support for the full [transitive] frame. Finally, the intuitionistic calculus I'm thinking of has weird labels: each formula has both a "proved or not proved" label and a "world" label.
All that matters from my point of view, is that they are not entirely useless, and require features that aren't too far beyond the system at each step along the road.
Fair enough. However, since the translation would be trivial to implement, it may be interesting to see which technique works better for Int. That is, proving it directly in Int (as you described) or translating into S4 and going from there. I think there is scope for some interesting experiments here.
Post a Comment