Geolog User Interface

The demonstration software described on this page is an experimental logic and algebra prover (or model builder) based on finitary geometric (a.k.a. coherent) logic. The GUI mediates dynamic interaction between the user and a Skolem machine (see references) which computes a coherent logic theory, using depth-first search. The indexed section on manual control describes the depth-first inference regimen for GeologUI in a more precise fashion.

The primary advantage of this software is the helpful opportunity it provides to visualize and interact with proofs. The software described on this page is only updated when specific errors are found. More recent theory and implementation is described elsewhere -- see the indexed section other links.

Building coherent logic provers is a very complicate engineering task requiring seemingly endless experimentation. The GeologUI software provides various working tools that are useful to investigate the problem of automating coherent logic proofs. To this end, four heuristics are presented here (, *, ∃, ∨). These heuristics provide interesting ways to limit the extent of search. Various experiments are offered which illustrate how to use the heuristics.

The following screen snapshot image is linked to the portable GeologUI Java application. Download the jar file and then either double-click the jar icon to run it, or else use the command

   > java -jar GeologUI.jar

Index ↓ [The panels] [Loading a theory] [Manual control] [Focus] [Tree scale] [Inference nodes] [Proof button] [Run button] [Clear button] [Yielding controls] [*Complexity controls] [∃Limit eigenvariables] [∨Limit splits] [Geolog inputs] [FOL inputs] [FOL options] [command line] [Geolog Experiments] [theory papers about Skolem machines] [other links]

The panels

Loading a geolog or a FOL theory

On many systems (e.g., Windows, Mac, Gnome) the user can drag and drop a file containing a theory onto the theory panel.

There is also a utility for converting TPTP format files to FOL format files in the File menu. It writes the converted file using the ".fol" extension, and the resulting file can be loaded explained in the previous paragraph.
⇑

Manual inference control

undo infer:

To undo the last rule application hit the <= button on the toolbar, or use the u key on the keyboard.

block rule instance:

Applicable rule instances are selected in a top-of-tree-down fashion. The first applicable rule -- shown as selected in the theory panel -- will match literals in the conjunctive antecedent of the rule using its factors from left-to-right. To block the application of the selected rule instance hit the x button on the toolbar, or use the b key on the keyboard. Backtracking control of rule instances occurs using right-most literals of the antecedent of the rule (right-to-left for a rule) and then proceeds to the next rule when no more instances of the current rule can be matched. Repeatly hitting x will cycle through all applicable rule instances from top-to-bottom, and then cycle back to top again.

next rule:

To block all remaining applicable instances of the current rule, hit the X button on the toolbar, or use the n key on the keyboard. The same effect could be achieved by repeated using the x button until all remaining instances of the current rule are avoided.

infer:

To accepted the selected applicable rule and to extend the proof tree using this applicable rule in the tree window, hit the => button on the toolbar, or use the i key on the keyboard. If there is no applicable rule (indicated by no rule being selected), then try hitting the <= button.

Focus

Tree scale (p key, m key, s key, o key)

Inference nodes

Proof button

Run button (r key)

Clear button (c key)

The following controls suppress manual inference control

Yielding controls

Complexity controls

Limit-Skolem-constants controls

Limit-splitting-rules-per-branch controls

Geolog format inputs

A geolog rule has the general form

A₁, A₂, .. , A_m => C₁ | C₁ | .. | C_.

If n=1 then there is a single consequent for the rule, and the rule is said to be definite. Otherwise the rule is a splitting rule that requires a case distinction (case of C₁ or case of C₂ or .. case of C_n).

The separate cases (disjuncts) C_j must have a conjunctive form

B₁, B₂,.., B_h

As an example, consider the geolog rule

s(X,Y) => e(X,Y) | dom(Z),r(X,Z),s(Z,Y) .

(∀ X)(∀ Y)[s(X,Y) → e(X,Y) ∨ (∃ Z)(dom(Z) ∧ r(X,Z) ∧ s(Z,Y))]

axiom:fol:equal_or_r_s:
![X,Y]:(s(X,Y) => (e(X,Y) | ?[Z]:(dom(Z) & r(X,Z) & s(Z,Y) ) ) ).

Now we come to special cases of rule forms, the true antecedent and the goal or false consequents. Rules of the form

true => C₁ | C₂ | .. | C_n.

A₁, A₂, .. , A_m => goal

A₁, A₂, .. , A_m => false

A geolog theory is a finite sequence of geolog rules. A theory may have any number of factuals and any number of goal or false rules.

The GeologUI system recognizes the abstract syntax just described for geolog rules and imposes the following restrictions for concrete syntax. With the exception of the special predicates and operators listed below, all other predicate names, functions, individual constants, and variable names are the responsibility of the geolog programmer.

The GeologUI system assumes that only variables start with caps (like Prolog). Predicates and function symbols appearing in GeologUI inputs can be framed in single quotes, such as 'Function'('A',X), in which case the quoted caps will not be read as variables, but the unquoted one (X) will..

The following tables display the special predicate, and operator symbols that the GeologUI system recognizes.

Here are some sample geolog rules, showing usage:

    X < Y, Y < Z = X < Z.                             % transitivity for predicate < 

    dom(X), dom(Y), dom(Z) => (X*Y)*Z) = (X*(Y*Z)).   % associativity for operator *

    dom(X) => (X *`X) = 1.                            % unary operator ` 
   
    dom(X) => (X * inv(X)) = 0.                       % 'inv(-)' is user operator

    X < Y => f(X) < f(Y).                             % f is monotonic wrt predicate <
    

Note that built-in binary infix operator expressions MUST occur parenthesized. The built-in binary infix predicates do not have to occur in surrounding parens.

NO fixed meaning is attached to any of the built-in symbolic predicates or operators.
⇑

FOL format inputs

role:mode:annotation: wff.

Only the 'conjecture' role is significant at present. All other role values are treated as if the wff is an axiom.

The 'cnf' and 'coherent' modes are significant. All other mode values assume that the wff is a closed first-order formula.

Universal quantification

![X,Y]: (p(X,Y) | q(Y)).

?[X]:(p(X) & q(X)).

When a ".fol" file is opened, it is parsed first and intermediate FOL formulas are generated, and then the FOL formulas are converted to geolog rules. The FOL formulas and the geolog conversion are displayed in a separate window (which can be minimized or dismissed).

The following table shows illustrative FOL-to-geolog conversions for the logical connectors and quantifiers. The second column shows the translation for axiom:fol:_:wff and the third column shows the translation for conjecture:fol:_:wff.

FOL-to-geolog Tableaux

wff	axiom:fol:_:	conjecture:fol:_:
(a & b)	/*1*/ a, -a => false. /*2*/ b, -b => false. /*3*/ true => '+{(a & b)}'. /*4*/ '+{(a & b)}' => a, b.	/*1*/ a, -a => false. /*2*/ b, -b => false. /*3*/ true => '-{(a & b)}'. /*4*/ '-{(a & b)}' => -a | -b.
(a | b)	/*1*/ a, -a => false. /*2*/ b, -b => false. /*3*/ true => '+{(a | b)}'. /*4*/ '+{(a | b)}' => a | b.	/*1*/ a, -a => false. /*2*/ b, -b => false. /*3*/ true => '-{(a | b)}'. /*4*/ '-{(a | b)}' => -a, -b.
~a	/*1*/ a, -a => false. /*2*/ true => '+{~a}'. /*3*/ '+{~a}' => -a.	/*1*/ a, -a => false. /*2*/ true => '-{~a}'. /*3*/ '-{~a}' => a.
(a <=> b)	/*1*/ a, -a => false. /*2*/ b, -b => false. /*3*/ true => '+{(a <=> b)}'. /*4*/ '+{(a <=> b)}' => '+{((a & b) | (~a & ~b))}'. /*5*/ '+{((a & b) | (~a & ~b))}' => '+{(a & b)}' | '+{(~a & ~b)}'. /*6*/ '+{(a & b)}' => a, b. /*7*/ '+{(~a & ~b)}' => '+{~a}', '+{~b}'. /*8*/ '+{~a}' => -a. /*9*/ '+{~b}' => -b.	/*1*/ a, -a => false. /*2*/ b, -b => false. /*3*/ true => '-{(a <=> b)}'. /*4*/ '-{(a <=> b)}' => '+{((a & ~b) | (~a & b))}'. /*5*/ '+{((a & ~b) | (~a & b))}' => '+{(a & ~b)}' | '+{(~a & b)}'. /*6*/ '+{(a & ~b)}' => a, '+{~b}'. /*7*/ '+{~b}' => -b. /*8*/ '+{(~a & b)}' => '+{~a}', b. /*9*/ '+{~a}' => -a.
![X]:p(X)	/*1*/ p(X0), -p(X0) => false. /*2*/ true => '+{![X]:p(X)}'. /*3*/ '+{![X]:p(X)}', 'exists'(X) => p(X).	/*1*/ p(X0), -p(X0) => false. /*2*/ true => '-{![X]:p(X)}'. /*3*/ '-{![X]:p(X)}' => '+{?[X]:~p(X)}'. /*4*/ '+{?[X]:~p(X)}' => 'exists'(X), '+{~p(X)}'(X). /*5*/ '+{~p(X)}'(X) => -p(X).
?[Y]:p(Y)	/*1*/ p(X0), -p(X0) => false. /*2*/ true => '+{?[Y]:p(Y)}'. /*3*/ '+{?[Y]:p(Y)}' => 'exists'(Y), p(Y).	/*1*/ p(X0), -p(X0) => false. /*2*/ true => '-{?[Y]:p(Y)}'. /*3*/ '-{?[Y]:p(Y)}' => '+{![Y]:~p(Y)}'. /*4*/ '+{![Y]:~p(Y)}', 'exists'(Y) => '+{~p(Y)}'(Y). /*5*/ '+{~p(Y)}'(Y) => -p(Y).

Given the sequence of fol formulas (from the file), the set of formulas is converted to a geolog theory. The geolog rules can then build geolog trees using the operations of a Skolem machine. In many ways the resulting geolog trees will resemble an analytic tableaux built from the original logical formulas, but the Skolem machine operations are quite different from tableaux operations in essential ways.

FOL formulas having mode 'cnf' do not have quantifiers. When such a formula is converted it is first closed. If the role is 'conjecture' then the existential closure is computed, otherwise the universal closure is computed.

For example, the input formulas

   axiom:cnf:either_or:
   (p(X) | ~q(X)) .

   conjecture:cnf:q_holds:
   q(Z) .

   axiom:fol:either_or:
   ![X](p(X) | ~q(X)) .

   conjecture:fol:q_holds:
   ?[Z]:q(Z) .

FOL conversion options

At present there are three methods for converting FOL formulas to geolog rules. One method uses verbose tabulation (an adaptation of the method of analytic tableaux). It translates a FOL formula to geolog rules using a full set of disjunctive geolog rules corresponding to the original wff, as illustrated in the previous table. Another method is called terse tabulation. It is a small refinement of the verbose method which collapses some of rules regarding the original wff. The third method detects coherent wffs, and translates them directly to corresponding geolog rules. Each conversion method automatically generates domain closure rules for function symbols (and constants) and consistency rules for predicates. The conversion method is selected via the "options" menu.

If the mode of a particular FOL input is 'coherent', then the wff is checked to see is it has coherent form and is converted accordingly. To only convert designated coherent FOL inputs, use the terse method of conversion and designate coherent rules by mode. To convert all coherent FOL inputs to geolog directly, use the coherent conversion method.

A coherent wff has the form

U ( A => C).

A is either a lone predicate or a conjunction of predicates, such as a(X) or (a(X) & p(Y) & r).

C has the form EA or a disjunction of same, where E is a possibly empty sequence of existential quantifiers such as ?[X]:?[Y]: or ?[X,Y]:

Here are some sample coherent wffs:

   (a => ((b & c) | d))

   ![X,Y]:(p(X) => (?[Z]:q(Y,Z) | r(X,Y)))

((a & (b & c)) => (d | e)).

Here is a sample FOL theory

   axiom:fol:commutativity_of_*:
   ![X,Y]: *(X,Y) = *(Y,X).

   axiom:fol:left_inverse:
   *(`a,a)=1.

   axiom:coherent:equal_is_transitive:
   ![X,Y,Z]: ( (X = Y & Y = Z) => X= Z).

   conjecture:fol:right_inverse:
   *(a,`a)=1.

   X = Y, Y = Z => X= Z

The conversion of a coherent wff to a geolog rule supplies 'exists'(-) predicates for universally quantified variables which do not actually appear in the antecedent, and it also supplies 'exists'(-) predicates explicitly for the existential variables which occcur in any disjunct in the consequent. For example

axiom:coherent:quantifier_test:
![X,Y]:(p(X) => (?[Z]:q(Y,Z) | r(X,Y))).

p(X), 'exists'(Y) => 'exists'(Z), q(Y,Z) | r(X,Y).

Equality ('=') and inequality ('!=') are logical contraries. For example,

   axiom:fol:_:
   ~ a=b.

   true => 'exists'(a).
   true => 'exists'(b).
   X0=X1, X0!=X1 => false.
   true => a!=b.

Command-line running

> java -jar GeologUI.jar h
usage: java -jar GeologDF.jar h                  {this help}
usage: java -jar GeologDF.jar F L Y C SK SP      {w/o gui}
usage: java -jar GeologDF.jar                    {start gui}

Geolog Experiments

Skolem Machine Theory

♦ 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.
⇑

Other links

♥ The Geolog theory loaders were created using ANTLRWorks: http://www.antlr.org/

♠ The Colog prover.

Send inquiries about GeologUI or recent developments here ...