Instructional Software for Logic and Source Code
5/24/2015
Welcome.
[As of summer 2012 we started to drop the use of Java and Java applets and instead transitioned to Javascript systems (this was principally to allow the software to run on tablets such as the iPad). The conversion is complete now.]
Most of the software is linked to directly from the Main Index to Instructional Software. [Additionally, sub-sections are being added to give more detail.]
Here are some shortcut links:-
Javascript Widgets
The Javascript implementations should run on any web browser on any computer directly and without any security concerns. They can run in a variety of configurations (with different menus, different menu items, different logical systems, etc.). Which configuration a running instance uses depends on how they are launched, specifically the web page, and preferences that the User (or Instructor or Author of the web page) chooses. The examples shown here are mostly running Introduction and Elimination rules (Gentzen sequent calculus adapted to a friendly presentation).
Example of Proof Widget
Example of Tree Widget
Example of Semantics Widget
Example of Symbolization Widget
Example of Modal Trees Widget
Example of Modal Truth Tables Widget
Example of an Examination Widget [not available yet]
Example of Reading a Counter Example from a Tree Widget
Example of Lambda Widget
Example of Endorse-Deny Widget [not available yet]
Java Applications
The Java applications can run in a variety of configurations (with different menus, different menu items, different logical systems, etc.). Which configuration a running instance uses depends on how they are launched, and preferences that the User (or Instructor) chooses. The examples shown here are mostly running Introduction and Elimination rules (Gentzen sequent calculus adapted to a friendly presentation).
[The main differences between the web page widgets and the stand alone applications are that the applications can save, or open, finished or half finished work, they can print better than the mere printing of a web page, and they are more sophisticated. If you wish to run an application, it will first download to your machine, check its own integrity, ask you if you wish to accept the digital signature that it carries, then it will launch.]
Examples of Applications (the Documentation will help you here)
Deriver.jar, double click on this after it has been downloaded. Your machine will probably ask you about all sorts of security matters (you'll have to make your own choices on that, but the application is digitally signed by SoftOption). On the first run it will run with default preferences; make desired changes to the preferences (under the Help Menu); save them; then, on subsequent launches, it will run to your preferences.
Example Propositional Exercises
Example Predicate Exercises
Easy Deriver [Full configuration] This can take 60 seconds to download. [2013 update. This uses what is called a '.jnlp' file to both launch JavaWebStart and configure what is launched to be what the User has requested. But, using jnlp files as launchers in web browsers has become very difficult. There are security concerns, and there are commercial interests trying to kill these kinds of uses of Java. It is probably prudent now for us to pass on trying to make a success of this. There are other ways, which we will explore. As a related example, many video conferencing systems use jnlp, and many are broken now.]
Java Applets (not favored these days)
The Java applets can run in a variety of configurations (with different menus, different menu items, different logical systems, etc.). Which configuration a running instance uses depends on how they are launched, and preferences that the User (or Instructor) chooses. The examples shown here are mostly running Introduction and Elimination rules (Gentzen sequent calculus adapted to a friendly presentation).
Examples of Applets (not favored these days)
[Applets can take 30 seconds to launch on recent Apple Macintoshes, but they launch in perhaps 10 seconds on most other machines]
Example of Proof Applet
Example of Tree Applet
Example of Semantics Applet
Example of Symbolization Applet
Example of Modal Trees Applet
Example of Modal Truth Tables Applet
Example of Reading a Counter Example from a Tree
Example of Examination Applet
Example of Lambda Applet
Example of Endorse-Deny Applet
Source Code
It is the intention to 'open source' most, if not all, the source code used here. This will take some time to do, maybe a year or two.
The Parsers Source
https://github.com/mfricke1947/ParserPublic.git
These are the parsers used for propositional and predicate logic on http://softoption.us . There are, possibly, four parsers. There are hand-written recursive descent parsers for the basic propositional and predicate logic, and for lambda calculus. Then there are two automatically generated parsers CCParser and CCParserTwo also for logic. All the actual parsers in use for the logic in the instructional software, and subclassed parsers all use CCParser or CCParserTwo. They can parse pretty well all the standard versions of logic (versions corresponding to all the standard textbooks). There is a single internal form, and the variations are translated into it when being read and parsed, then the formulas are written back in the desired flavor or style.
The Proof Widget Source
https://github.com/mfricke1947/ProofsPublic.git
Software for instruction in logic (as used on http://softoption.us ). This is the source code for the Proof Widget, which is some javascript for displaying proofs in propositional logic, predicate logic, first-order theories, set theory, and lambda calculus. The Widget illustrates intelligent editing of derivations, tactics, and compiling derivations (best-path theorem proving). The code is written in Java and the project hosted and developed in the Eclipse IDE, with GIT and the Google Web Toolkit (GWT) plug-in. The GWT plug-in can run the project in Super Dev mode for development. Then it compiles the Java to Javascript, which can be embedded in Web Pages (or ePubs, iBooks etc.). Various 'switches' in those Web Pages allow the Proof Widget to be configured to run the desired systems. Sample Web pages are included.
- Example of the Proof Widget
- The Proof Panel
- Intelligent Editing
- Tactics for System I
- Using Tactics [Generic]
- Frické, M [2012] 'Best-path theorem proving: compiling derivations', Chapter in Rationis Defensor: Essays in Honour of Colin Cheyne. Springer, 2012, ISBN-10: 9400739826, pp. 255- 275. pdf of Draft