help Colog1.7
coherent logic prover

[page modified 25 April 2010 ]

Download the executable Java archive Colog1.7.jar .

Version 1.7 uses smaller structures to hold facts in its search trees.
The tree pane for the GUI now supports dragging the tree into view.

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.

Command-line usage requires files containing geolog (not FOL) theories:

$ java -jar Colog1.7.jar help
--------------------------------------------------------------------------------
Colog1.7, 25 April 2010
  > java -jar Colog1.7.jar help                                    % this help 
  > java -jar Colog1.7.jar                                        % launch GUI 
  > java -jar Colog1.7.jar DESC DEPTH WIDTH COMPLEXITY           % comline run  
       where                                                                       
          DESC is folder of theory files or a single theory file                   
          DEPTH is max depth allowed for any branch                                
          WIDTH is the max number of branches                                     
          COMPLEXITY is max allowed nesting for functions, -1=OFF                 
  > java -jar Colog1.7.jar DESC DEPTH WIDTH          % comline run, short form  
       (COMPLEXITY off)                                                            
  > java -jar Colog1.7.jar DESC DEPTH              % comline run, shorter form 
       (WIDTH = 10,000 default and COMPLEXITY off)                                 
                                                                                    
  *See http://JohnRFisher.net/colog/ for more information                         
--------------------------------------------------------------------------------

QEDF search

Colog implements QEDF search for coherent logic.
See the QEDF technote.
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.

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.
(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 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.

Please direct questions to
cloudmail.gif

√W3C