What's new in ProofTools 0.6.2
Jun 21, 2020
- Bugfix: for some proofs, notably the simplest of premise P and conclusion P, the application aborted due to trying to free already-freed memory.
New in ProofTools 0.6.1 (Nov 19, 2019)
- New features:
- Bugfix: the (negated) biimplication rule had been copying branch data erroneously with the effect that nodes from one of the generated branches could be mistakenly used in rule applications on the other branch. This was exemplified by the invalid argument being assessed as valid: premise #1 Td↔(Oj∧Cj), premise #2 Te↔∀x(Ox→Cx), conclusion Td→Te. (This bug had been introduced in version 0.6).
New in ProofTools 0.6 (Nov 19, 2019)
- New features:
- Bugfix: disabled infinite branch detection, known to be using a defective algorithm which gives the wrong results in some cases, except for the straightforward detection of infinite branches due to applications of the modal extensibility rule, which was left in place.
- Added a progress window for when clicking "Show Proof". This includes a "Cancel" button which provides users with a means to escape infinite branches (trees) given that automated detection has been disabled.
- Added a numeric input box to allow specification of the number of rules to apply at a time when clicking the "Step" button, defaulting to one. (The progress window is not shown when stepping like this).
- Bugfix: fixed the "branching modal logic with necessity" bug, exemplified by ProofTools reporting to be NOT valid when it IS valid the argument with premise □(P∧Q) and conclusion □P∧□Q.
- Corrected a mistaken hint on the "T" tool button.
New in ProofTools 0.5 Beta (Oct 10, 2014)
- 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.
New in ProofTools 0.4.2 Beta (Jun 6, 2014)
- New features:
- Turned the "abbreviated tree" feature into an option (accessible via a checkbox), defaulting to off rather than mandatorily on as it had been.
- Implemented greater sophistication of handling of parentheses, including:
- Provided an interface option (a dropdown box) to (de)normalise parentheses, either universally across the tree, or from the current point onwards.
- Implemented the parsing, storing and reproducing of all parentheses including those subsequent to unary operators, to any level of nesting.
- Bugfix: individual constants/variables were being incorrectly parenthesised in identities under Tarski syntax.
- Bugfix: when applying a negated universal/existential quantifier rule, or a negated necessity/possibility rule, and the negation operator is switched inside to apply to a term involving a binary operator which wasn't yet parenthesised, parentheses weren't being generated to make it clear that the negation operator applied to the entire binary term rather than to just the first one.
- Split the settings toolbars into four, so that the minimum width of the app can be reduced to approximately 640 pixels - to support resolutions of 640x480.
- Added symbols for several common proposition/predicate/variable/constant names, so that the mouse can be used entirely for entry without needing to intersperse mouse clicks with keyboard entry.
- Added three new symbol replacements, /\ (forward slash, backslash) for conjunction, -| for negation, and -] for the existential quantifier.
- Bugfix: when "abbreviated tree" was enabled (which until now it had been mandatorily), sometimes duplicate identity nodes were not being detected.
- Bugfix: under the GTK2 widgetset, when the active premise/conclusion entry box cursor was at a location prior to the end of the text in the box, clicking a symbol button would insert the symbol in the wrong place (at the beginning or end of the text).
- Propagated font changes to secondary windows (the hotkey editor and test results windows).
New in ProofTools 0.4.1 Beta (Oct 10, 2013)
- Bugfix: the Substitutivity of Identicals rule was not being applied to identities themselves, such that the logical truth (a=b∧c=b)→a=c was not being evaluated as a logical truth.
- Bugfix: world numbers were sometimes displaying when they shouldn't have.
- Bugfix: the form was oversize on initial opening on OS X.
- Changed a symbol replacement: \/ (backslash, forward slash) is now replaced with the disjunction operator, ∨, rather than the universal quantifier, ∀.
New in ProofTools 0.4 Beta (Oct 10, 2013)
- Support for normal modal logics, including both basic, K, and those characterised by one or more of reflexivity, symmetry, transitivity and extendability, which includes support for S5. This implementation of modal logic has constant domain when quantified, and contingent identity.
- Support for identity (a=b) and negated identity (a≠b).
- Support for numbered predicate, proposition, variable and constant names.
- Support for symbol replacements whilst editing formulas (e.g. is replaced with ↔).
- Support for Tarski's world syntax via a checkbox (by request).
- Optimised rule generation/application such that potential applications of rules that would add only nodes that already exist on the branch are ignored.
- Optimised rule choice so that rules that would close the branch are chosen ahead of all others.
- A battery of tests accessible from the File menu.
- Bugfix: the width of the tree panel was sometimes greater than it needed to be for some trees when scrollbars were visible.
- OS X bugfix: the status icon wasn't changing colour.
- Parser error-detection bugfix: the parser failed to pick up a certain type of error in certain cases, that error being when a predicate was specified multiple times with a different number of variables (the actual conditions for the error were more specific than this). An example of a formula containing this type of error (w.r.t. the P predicate) that would fail to be detected by the parser is ∃x∃yPxy∧Qxy∧∃zPxyz∧Qxy.
New in ProofTools 0.3.2 Beta (Oct 10, 2013)
- First Mac release! Contains compatibility fixes for Mac OSX, x86 (Intel) platform only - otherwise is identical with the previous 0.3.1 beta release, hence no new files have been released for existing platforms.
- Note: this first release is not perfect - in particular, the validation status icon (the square at the left of the status bar bottom of application) never changes colour - you will need to rely on the messages in the status bar.