Instructional Software for Logic and Source Code

1/27/2020

Welcome.

Most of the software is explained in detail in the sub-chapters below.

If you are interested just in a brief look, here are some shortcut links:-

Javascript Widgets (produced primarily from Java Code)

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 Reductions Widget
Example of Endorse-Deny Widget [not available yet]
Example of  Combinatory Logic Verbose Parse and Combinatory Logic Reductions

Javascript Widgets (produced primarily from Haskell Code)

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.

Example of Lambda Verbose Parse Widget 
Example of Lambda One-step Redex Widget 
Example of Normal Order and Applicative Order Reductions in Parallel Widget 

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 (compiled 2015 tested and runs 1/19/20). 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. For example, (9/27/2019) "Blackboard Collaborate Web Conferencing utilizes the Java Network Launching Protocol (JNLP) to launch a web conferencing session". This is Web Conferencing for Online Teaching. We will assume that in the case of Blackboard, they will have it working perfectly— but, take home, using jnlp is not easy.]