help colog1.9
coherent logic prover

[page modified 2 July 2011 ]

Download the executable Java archive colog.jar .

Version 1.9 implements relevancy for case reasoning.
See the QEDF technote for details.

Red notes signal found bugs not fixed in this version.

This page resides at JohnRFisher.NET.

Running Colog

The user can double-click on the jar icon to start the GUI version,
if applicable for user's system. The GUI version is generally similar to GeologUI,
but rule interactions are more limited. 

$ java -jar colog.jar help
--------------------------------------------------------------------------------
colog1.9, 9 March 2011                                                       
  > java -jar colog.jar help                                        % this help 
  > java -jar colog.jar                                        % launch the GUI 
  > java -jar colog.jar file=f [depth=d width=w complexity=c log=b]   % comline 
       where                                                                    
          f is either a theory file or folder of same                           
          and defaults are ...                                                  
             d = 300                                                            
             w = 1000                                                            
             c = -1 (OFF)                                                       
             b = false                                                          
--------------------------------------------------------------------------------

QEDF search

Colog implements QEDF search for coherent logic.
See the QEDF technote (new §1.1 on relevance).
At this time, Colog only queues existential rules and complex functional rules,
and does not implement a strategy for breaking functional rule cycles (as described in the technote).

A queueing strategy decides which rules of a theory to put into the queue.
As an alternative to strategies built into the prover, one can employ the following mechanism.
If one includes an initial directive rule in a geolog theory of the form

do => queue(ri1,ri2,...).
where rij ≥ 1, then the loader will put only the specific rules rij into the queue.
Such a do rule must appear as the initial (0th) rule in the source file,
but Colog will not include this particular rule in Colog's rulebase.
To force an empty queue, employ the queue nothing rule 
   do => queue(0).
This adhoc queueing mechanism allows experiments regarding the effectiveness of queueing strategies.

Box search

Colog implements box search which is explained in a Box search technote.
Not all mathematical lattices are distributive.
Here is a beautiful picture of an automated verification of this fact (box search finds 2 counter models).

Fore/aft analysis of FOL inputs

Colog (GUI version only at present) implements fore-and-aft analysis for FOL inputs.
FOL theory file inputs must have .fol extension (sam as GeologUI).
One can convert FOL theories to coherent logic theories using the GUI version.
The GeologUI page describes FOL inputs (but considers a different translation to coherent logic).
Fore-and-aft analysis atempts to preserve formal implications in wffs.
See the Fore-and-Aft technote.

Note added 18 June 2010: The fore translation of either an
existential wff, or negated universal wff, can yield errors.
(The codes in sam.fol.WFF.java, lines 628-638 and 757-767 are incorrect.)
This problem does not affect geolog inputs.

Domain guarding

Colog has a domain guarding utility: 

$ java -cp Colog.jar Guard <file> <domname>
where domname is the name of the domain predicate used for the geolog theory in file.
The converted file with domain guards is written with .gd suffix.
See the domain guarding technote.

Note added 5 May 2010: found bug in code. Guard does not correctly analyze constants.
Needs fix.

Multicore experiments

In the spring of 2009, and on a visit to UiB in October 2009, a multicore version of Colog was developed and tested.
Here is a report describing some of the preliminary outcomes.

Skolem Machine Theory

Three papers about Skolem Machine Theory attempt to describe a machine model for computing with coherent logic.
The references in these papers are also helpful. Copies of these papers are available on request.

* John Fisher and Marc Bezem, Skolem Machines, Fundamenta Informaticae, Machines, Computation and Universality, 91 (1) 2009, pp. 79-103.

* John Fisher and Marc Bezem, Skolem Machines and Geometric Logic. In C.B. Jones, Z. Liu and J. Woodcock, Proc. ICTAC 2007 The 4th International Colloquium on Theoretical Aspects of Computing, Macao SAR, China, September 26-28, 2007. Springer LNCS vol. 4711, pp. 201-215.

* John Fisher and Marc Bezem, Query Completeness of Skolem Machine Computations. In J. Durand-Los`e and M. Margenstern, editors, Proc. Machines, Computations and Universality 07, Universite d`Orleans - LIFO, Orleans, France September 10-14, 2007. Springer LNCS vol. 4664, pp. 182-192.

Sources

colog1.9.zip

Unzip the colog archive and the structure is 

colog1.9/  
   about          {short notes on this version/changes}
   colog.java     {main class}
   org            {antlr runtime}
   LICENSE        {relevant to version}
   makeall        {recompile script}
   makedoc        {Javadoc script}
   makejar        {make jar script} 
   colog1.9.jar   {what makeall or makejar makes}
   sam/           {aka skolem abstract machine}
      fol/        {FOL to geolog}
         antlr    {ANTLR Fol grammar, etc.}
      gui/        {logic visualizer GUI}
      infer/      {inference engine guts}
      lang/       {geolog language classes}
         antlr/   {ANTLR Geolog grammar, etc.}
      util/       {fast small stacks, queues, etc.}
   ...            {perhaps other experimental stuff?}
I use JavaEditor and ANTLRworks for development.
I usually keep classes with sources. The makeall script
needs a classpath param: For example, If I download
colog1.9.zip and unzip it inside of /skolem/java/
then the classpath parameter to use for makeall is ... 
  > source makeall /skolem/java/colog1.9

Possible Student Projects

1. Design and implement dynamic rule indexing for colog, 
   also called "just-in-time-rule-indexing" (JITI), which restricts 
   the applicable rule choices based upon the current branch facts.
2. Adapt a colog prover for use with Google App Engine (GAE).
3. Adapt a colog prover for use with Amazon Web Services (AWS).
4. Design and implement extensions to geolog for built-ins: arithmetic, 
   lists, etc.
5. Design and implement extensions to geolog for using modules or packages, 
   supporting unique name spaces.
6. Design translators from N3 logic into extended geolog (using #4, #5).
7. Implement QEDF for a Prolog coherent logic prover.
Please direct questions to
cloudmail.gif

√W3C