All releases tagged QEDEQ
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.
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: You can write formal proofs that use only the basic rules. These proofs can be seen in the text viewer and the generated LaTeX sources. They are still not checked for correctness. For an example see "sample\qedeq_sample3.xml". The reference syntax was slightly changed and extended to include proof line references. Under the hood, the kernel services were reorganized to fit better to the plugin structure. The text viewer now uses the "Monospaced" font, and more UTF-8 characters are now displayed correctly. Also, some more proofs were added to the mathematical content.
Release Notes: New real plugins: "Show module as UTF-8 text", "Create UTF-8", and "Model Tester". The first ones are self-explanatory. The last one allows testing the validity of formulas in different finite models. The "four element model" is the approved model. It contains the following four elements: {}, {{}}, {{}, {{}}}, and {{{}}}. Together with the usual "element of" relation, it can fulfill almost all formulas of the logic and set theory script. Quite a few typos were fixed. There is a new process window to watch over plugin processes. The GUI has some other additions and changes.
