The following paper introduced the idea of a Skolem Machine for computing coherent logic.John Fisher and Marc Bezem, Skolem Machines,The first link is to a copy of the paper with minor corrections. Note: colog machine code for a Skolem Machine was called geolog in this paper. The paper gives conceptual definitions of a Skolem Machine -- as a tape machine analagous to a Turing Machine and as a tree machine -- and shows that it has theoretical computational universality. The paper does not provide specific implementation design details (e.g. see SAM.pdf link below). Related ↬ papers ...
Fundamenta Informaticae, 91 (1) 2009, pp.79-103 ↬ SkolemMachines.pdf
The paper also has a ResearchGate page ↬ here
J. Barkley Rosser: "Of course Turing did it before us. Turing, of course, was awfully concerned with the correct way to do it. 'You do it on a machine, see.' "
A colog primer ↬ colog.pdf
Colog is a machine language for a Skolem machine.
Read the primer and use the GUI prover to run the primer's examples (examples/fisher/colog_primer/) ↳ examples.zip.
Latest Java implementation ↳ colog14I.jar (made with java version "15.0.1")
Download the jar, double-click on jar to start the colog proof browser GUI. Read the usage notes under the ??? tab of the proof browser.An old report (2009) describes the fore-and-aft, fol-to-colog translation idea: ↬ fol2cl.pdf. This version of translation is implemented by colog14I (FOL tool tab), and some earlier versions. Various bugs (or difficulties) persist, awaiting new developments.Sources: ↳ colog14I.zip (Unzip, See README file)
The colog and FOL parser-generators employed by the prover are implemented using ANTLR grammars.
Constructive Coherent Translation of Propositional Logic, using fore-and-aft Heyting templates ↬ prop2cl.pdf.
Implementation design report for the Skolem Abstract Machine ↬ SAM.pdfMore related refs and links ... (the 2023 note explains a colog14I bug)
This document outlines design ideas regarding SAM implementation, including the distributive (fair) choices algorithm §5.
#1 - Autolog MetaLogic .pdf .txt
#2 - Autolog Quantifier MetaLogic .pdf .txt
#3 - Autolog Type Metalogic .pdf .txt
#4 - Autolog Category Metalogic .pdf .txt
#5 - Autolog Set Type Metalogic .pdf .txt
The lecture notes describe autolog programs that we would like to compute, along with some suggestions regarding how they should be computed. The examples provide use cases for autolog system code development and testing. A problem is specified using an autolog program. The meaning of the program involves the inference trees that can be generated from the program by a Skolem Machine. The problem answers are specified by the goal rules of the autolog program and inference trees support answers.
about category ISOTYPES ‐ categories as type universes