10/31/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 Truth Table Widget [Truth, Satisfiable, Consistent, Invalid]
Example of Tree Widget
Example of Semantics Widget
Example of Symbolization Widget
Example of Modal Trees Widget
Example of Modal Truth Table 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
Example of Intuitionistic Propositional Logic
Example of Epistemic Logic Widget
Example of Tarski's World Widget
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
Example of Normal Order Reductions in Simply Typed Lambda Calculus Widget
Example of Simply Typed Lambda Calculus Constraints for Type Inference 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)
Deriver20Signed.jar (compiled 2015 tested and runs 10/30/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.
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.]
DRAFT Java (Java applets and downloadable Java applications)
Downloadable Java Applications
The Deriver application program, and the applets, run on the 'Java Virtual Machine' or 'Java Runtime Environment' on the host computer (your home computer). But if your Java Runtime Environment is out of date, especially way out of date, that offers an invitation to erratic behaviour. Windows and Macintosh machines, and probably others, automatically update their JREs. But you can refuse that update (and maybe some Users do not understanding what a Java Runtime Environment is).
But if your version of Deriver is doing something odd, like not displaying the symbols properly, check that your JRE is up to date. Check
Java Tester and maybe Install Java (thank you, Michael Horowitz, for these)
Java Technology Help or
JRE Installation Instructions
mozillaZine Knowledge Base: Java has a lot of good and useful information on running Java.
Continue to Checking your computer is configured correctly II . This one has real Java in it, so it could take 30 seconds to load or, if things are not working properly, it may remain blank.