10/5/2021
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.
English to Logic Source
https://github.com/mfricke1947/EnglishToLogic
Introduction This translates English into Propositional or Predicate Logic, primarily in the context of teaching logic in a college course. Running the code The code is written in Scheme, a LISP dialect. It was written to run on its own interpreter and so it uses only a subset of Scheme. There are different dialects of Scheme (for example, some have the empty list '() and others have the defined constant 'empty). This code will run on Racket (DrRacket). Download from https://racket-lang.org/ Use the 'Pretty Big' language option. [This may help you with Racket https://www.youtube.com/watch?v=oQD01ybB1z4 ]
The Deriver15 Application and Applet Source
https://github.com/mfricke1947/Deriver15Public
#Deriver15Public [Code compiles and runs with Eclipse 2019-09R (4.1.3.0) 1/31/2020] Software for instruction in logic (as used on https://softoption.us ). This is the full source code for Deriver15, which is java code for displaying proofs, intelligent editing of derivations, tactics, drawing derivation trees, drawing semantic interpretations, symbolization etc. This code is pretty much unchanged since 2012. In 2015 the license notices were added, hence Deriver15. The Java Build Path should have in it the source code and the JRE System Library, say Java SE 1.7 (although it won't be sensitive on that). It should also have JUnit 5 as a Library (as there is some JUnit test code). The code can then be run within Eclipse as a Java Application with the main TDeriverApplication -- us.softoption.editor The documentation on https://softoption.us would help here on what the application can do. Eclipse can export the application as a Runnable JAR file, say Deriver15.jar. It would be typical then to run this through Proguard, say 6.2.2 which will obfuscate and compress it (from about 3.6 meg to 1 meg). It is important here that the right configuration file be used for Proguard. Basically the consideration is that Java Beans are used to save to file, and this means that when windows and contents are re-created from file the names of the classes cannot have been obfuscated. Some sample Proguard configuration files are included. Proguard may produce hundreds of warnings but yet run through successfully. Then it would be usual to sign the compressed jar using jarsigner and Java key tool. It is possible to timestamp this. Deriver15 has various 'switches' in it controlled through its preferences. Sample logic instruction files are included. The Deriver15 jar/application can be automatically downloaded and launched using jnlp and Java Web Start. It also can configure itself when doing this. Some sample files are included. The source code for twenty or more applets is included. These used to be embedded in web pages so as to have Deriver functionality without having to have the application installed or downloaded. The applet code used to be obfuscated, compressed, and signed. This technology is dead. [Most of the applets have been rewritten as javascript widgets, and that code is available elsewhere.] However, you can still run the applets in Eclipse. The applets have 'applet' in their name somewhere. For example, us.softoption.gameApplets has as one of its source files GamesQuiz.java If you select that file and 'Run As Java Applet' Eclipse will do exactly that for you (and similarly for the other applets).
The Combinatory Logic Widget Source
https://github.com/mfricke1947/CombinatoryLogicPublic.git
Software for instruction in logic (as used on http://softoption.us ). This is the source code for the Combinatory Logic Widget, which is some javascript for displaying proofs in combinatory logic. The Widget illustrates intelligent editing of derivations. The code is written in Java and the project hosted and developed in the Eclipse IDE Oxygen 3a), with GIT and the Google Web Toolkit (GWT 2.8.1) 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 Lambda Widget to be configured. Sample Web pages are included. [Code compiles and runs with Eclipse and GWT 5/7/2018]
The Lambda Widget Source
https://github.com/mfricke1947/LambdaPublic.git
Software for instruction in logic (as used on http://softoption.us ). This is the source code for the Lambda Widget, which is some javascript for displaying proofs in lambda calculus. The Widget illustrates intelligent editing of derivations, and tactics. The code is written in Java and the project hosted and developed in the Eclipse IDE (Oxygen 3a), with GIT and the Google Web Toolkit (GWT 2.8.1) 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 Lambda Widget to be configured. Sample Web pages are included.[Code compiles and runs with Eclipse and GWT 4/27/2018]
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
The Trees Widget Source
https://github.com/mfricke1947/TreesJSPublic.git
Software for instruction in logic (as used on http://softoption.us ). This is the source code for the Trees Widget, which is some javascript for displaying trees in propositional logic, predicate logic, first-order theories, modal logic, and set theory. The Widget illustrates extension and closing of tree. 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 Trees Widget to be configured to run the desired systems. Sample Web pages are included. For these, go to TreesJS/war/ and then use a web browser on Tutorial1.html etc.