Release Notes: Formal proofs can be checked. The first successfully checked QEDEQ module is "sample/qedeq_sample3.xml". Another new plugin can find simple propositional calculus proofs. You can test that with "sample/qedeq_sample4.xml", which contains propositions without formal proofs. Also added was "doc/math/qedeq_propositional_v1.xml", which contains new axioms for propositional calculus. Propositions with formal proofs will be added to develop the complete propositional calculus. Definitions are now direct equivalences or identity relations, thus definition formulas can be referenced in formal proofs directly.
Release Notes: This release concentrates on stabilizing the processing structure, increasing the test coverage, and bugfixes. It reworks "Process / View Processes": now all modules it tries to work on within a process are listed. "Details" shows more useful information. There is an XSD change: the element BIBLIOGRAPHY is allowed to have no ITEM sub elements.
Release Notes: The icon for QEDEQ module status display now has different colors to represent different stages. Errors and warnings are visualized by decorator icons. Modules which are in progress are represented by animated icons. The clover and findbugs tools were updated. Process synchronization and process control were reorganized. This work is not finished yet, but nearly all module status changes are now caused by plugins. The process view shows more detail, and the chances for user interrupts were increased.
Release Notes: The context menu of text area fields include now "find": one can search for strings. The initial window size for text viewing was optimized; now the window should fit the screen more likely. Various test classes and tests were added. The test coverage percentage is now at 78.6%. A positive side effect was the discovery of some minor bugs, which were directly fixed. A few formal proofs were added to qedeq_formal_logic_v1.xml.
Release Notes: There is now a parser that can read a propositional calculus proof written in ASCII text format and transform it into a QEDEQ XML NODE element. This helps speed up proof integration. It can be accessed via GUI menu entry "Tools / Proof Text to QEDEQ". A derivation rule now also has a version, and the combination of name and version must be unique. A "brief" parameter was introduced for the LaTeX and UTF-8 plugin to produce summary documents. More propositions with formal proofs are included.
Release Notes: This release introduced a new proof method: conditional proof. Based on the deduction theorem, you can make an assumption and draw conclusions from it. It shows the unfolding of formal logic from axioms and inference rules to propositions of propositional calculus with formal proofs within qedeq_formal_logic_v1. The new proof method is also integrated in the proof checker. In the log output pane, messages are now better structured and more readable.