What's 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 10, 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 14, 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 14, 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.
- 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 14, 2013)
- 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.
New in ProofTools 0.3.1 Beta (Oct 14, 2013)
- Bugfix: fixed a bug that could cause invalid arguments to be assessed as valid: the same constant was sometimes used for multiple separate applications of the universal quantifier rule.
- Bug/build fix: fixed a bug of unknown origin in the prior release whereby clicking on symbol buttons in the Linux builds resulted in symbols being inserted at the beginning of the active text box rather than at the cursor.
New in ProofTools 0.3 Beta (Oct 14, 2013)
- Bugfix (a parsing bug): fixed a bug that was exemplified by ∀xCa∧Dx→Fax being incorrectly parsed as ((∀x)Ca∧Dx)→Fax instead of (∀x)(Ca∧Dx→Fax). This was due to unary operators (including quantifiers) being bound to the first binary operator that follows, rather than to the lowest precedence binary operator that follows within the scope of the unary operator.
- Overhauled the drawing code majorly for speed and efficiency, replacing TLabel components with direct drawing to the canvas.
- Bugfix: fixed a bug that had been causing two problems: trees being bigger than they needed to be, and the wrong secondary node (the one from which the constant was taken) being highlighted when mousing over a node generated by a universal quantifier rule application.
- Bugfix: (mostly) solved a problem where scrollbars would appear or disappear when they ought not to during resizing of the main window.
New in ProofTools 0.2.2 Beta (Oct 14, 2013)
- Bugfix: only the first of multiple identical variables in a predicate was being replaced with a constant in a universal quantifier rule application.
- Bugfix: certain expressions, such as (∀x)(Fx)∨¬(∃x)(¬(Fx)), were being incorrectly parsed.
- A re-fix of the parse error message "fixed" in 0.2.1 beta.
- Bugfix: after hovering the mouse pointer over a node and then changing the tree's background colour using the background colour dialogue button, the node's background colour was not updating from its old colour until the mouse pointer was again hovered over it.
New in ProofTools 0.2.1 Beta (Oct 14, 2013)
- Bugfix: unclosed branches were randomly falsely being labelled infinite.
- Minor correction: fixed a faulty parse error message.
- The validation status messages for when only a conclusion is set have been adjusted to indicate that rather than being an (in)valid argument it is or is not a logical truth.
New in ProofTools 0.2.0 Beta (Oct 14, 2013)
- Support for predicate logic including detection of infinite loops on a branch. There is no support yet for nested functions although this is planned for down the road.
- Holding the mouse pointer over a node now highlights the node/s it was generated from, and displays in the status bar the rule that was used to generate it.
- Operator precedence and tolerance of missing pairs of parentheses.
- Customisable hotkeys.
- The ability to draw a tree based on premises only and without setting a conclusion.
- Enhancements to the status bar including separation of messages from the status of the validation, and colourisation of the status of the validation.