ProofTools Changelog

What's new in ProofTools 0.5 Beta

• Bugfix: sometimes, when starting the app, its main window's status bar was invisible until that window was resized.
• Added copy-to-clipboard support for both individual nodes (plain text) and the entire tree (as an image), accessible via a right-click context menu.
• Added counter-model popups, fully supporting propositional, predicate and modal logic in any combination, with a copy-to-clipboard feature accessible via a right-click context menu.
• Added support and a toggle box for the modal Euclidean accessibility relation ε, equivalent to toggling modal axiom 5.
• Added a new dropdown box for all basic/normal modal logic variants - selecting an item in the dropdown sets the appropriate toggles of reflexivity, symmetry, transitivity, extendability, Euclidean and S5. Items in the dropdown are prefixed by a number - equivalent modal logic variants share the same number. For completeness, all included modal logic variants parenthesised into their fifteen equivalent groups are: (K), (KB), (KD), (KT, KDT, T), (K4), (K5), (KBD), (KBT, KBDT), (KB4, KB5, KB45), (KD4), (KD5), (KT4, KDT4, S4), (KT5, KBD5, KBD4, KBT4, KBT5, KDT5, KT45, KBD45, KBT45, KDT45, KBDT4, KBDT5, KBDT45, S5), (K45) and (KD45).
• Decoupled the S5 toggle box from the other modal accessibility relation toggle boxes (toggling it on now untoggles the rest), because in actuality the S5 proof tree rules are distinct from the other modal accessibility relation proof tree rules.
• Added several new tests based around the normal modal axioms.
• Bugfix: sometimes, adding a premise to, or changing the conclusion of, an existing argument, or clearing and then rerunning a proof, gave the wrong result (different to the original run, if any), due to state data not being correctly cleared. e.g. toggling S5 on and then setting a premise of □P, and a conclusion of □□P∨∀xQx→Px∧x=a, then clicking "Show proof", (correctly) showed a "Valid argument" result, but then clicking "Clear proof" followed by "Show proof" (incorrectly) showed an "Invalid argument" result.
• Corrected the hints for constant/variable shortcut buttons.
• Bugfix: sometimes, randomly, the second branch of a disjunct which should have had a modal extensibility rule applied to it and then been labelled infinite was instead left open.