Foda

http://www.csupomona.edu/~jrfisher/www/geolog/
Geolog and Skolem Machines
[last revised 30 August 2007]
|John Fisher |Marc Bezem |
|Computer Science Department |Department of Computer Science |
|California State Polytechnic University|University of Bergen |
|Pomona, California, USA |Bergen, Norway |
|jrfisher@csupomona.edu |bezem@ii.uib.no |

Geolog is a logic programming language for finitary geometric logic. These webnotes describe how touse a Geolog interpreter written in Prolog, called Geoprolog. These notes also provide examples showing how to prove some interesting mathematical theorems using Geoprolog. Another section (§8) discusses an interactive version of the software that connects a Prolog prover with a Java GUI.
The authors have developed machine models for describing Geolog computations. An interesting approachinvolves what we call Skolem Machines. A Skolem machine is another abstract model for computation. Skolem machines have Geolog theories as input instructions. Skolem machines have computational power generally equivalent to Turing Machines. Click on the link for §0 below to read a short article regarding some basic definitions of the Geolog language and Skolem machine operations. The references at theend of the article cite theoretical work. Skolem machines (as formulated by us) are named after the eminent Norwegian mathematician and logician Thoralf Skolem (1887-1963). Historically, the essential ideas behind Skolem Machines were "invented" by Thoralf Skolem about 87 years ago!!! See our notes in §0, which briefly explains this connection. A nice biography of T.Skolem is posted here.
If oneclicks on the "SM" links, a proof demonstration Java applet opens in a new window. The resulting interactive display simulates a Skolem machine computation, in tree form, for the corresponding theory. The interaction is NOT computing the tree: It is displaying the tree inferences generated by the iG program described in §8.
For example, click here: SM to see a sample Skolem machine computation forthe little theory described in the whitepaper of §0.
If you would like to make comments or ask questions about this website please email us (links above).
[pic]
[pic]
§...
§0. Technical Notes on the Geolog language and Skolem Machines (pdf)
§1. download some files
§2. start Prolog and load geoprolog.pl
§3. working with Geolog theories
§4. writing Geolog rules
§5. working with "runaway"theories
§6. Sample Geolog theories and proofs
6a- dpe Diamond Property in rewriting theory SM
6b- latt_assoc & latt_comm associativity and commutativity of the supremum operation in a lattice
6c- nl Newman's Lemma in rewriting theory
6d- p1p2 & p2p1 side conditions in Pappus' Theorem in plane geometry
6e- mb transitive relations property
6f- unf confluence of a rewrite relation impliesuniqueness of normal forms
6g- r3_5 Ramsey number COUNTERMODEL, 3-cliques on 5 points SM
§7. minimal case proofs
§8. interactive Geolog proof browser
[pic]
§1. download some files ...
Download the following files:
The Prolog source code file geoprolog.pl (~8KB).
The Java tree visualizer GeologTree.jar (~20KB).
The sample Geolog theory source file dpe.gl (~4KB), example for § 3.
The sampleGeolog theory source file inf.gl (~4KB), example for § 6.
Create a directory called "geolog" on your system and move these files into that directory, as shown in the following diagram.
[pic]
Additional files to download will be linked, as needed, in later sections.
_^_
[pic]
§2. start SWI-Prolog and load geoprolog...
Start SWI-Prolog from the "geolog" directory (created in step 1). On our...