colog colog https://skolemmachines.org/index.htmlfor background information about Skolem Machines and the various versions of the colog (coherent logic) prover.
• A colog theory can be loaded by dragging a link (representing File or URL) to the colog theory pane.• The "Open .." Theory menuitems can open theories using File or URL dialogs. Cmd-R reloads a theory.
• The R key (or => on toolbar) reruns a search and the C key (or clear on toolbar) clears the tree pane (and also the aux pane).
• The tree tabbed pane displays the search results as a colog tree.
• The console tabbed pane is useful to view theory load errors or search statistics.
• Tree view scale can be increased (P key) or decreased (M key) or forced to fit pane (S key), or use original scale (O key). The Options menu has three tools for view control of trees: tree scale, see selected and move split. The view tools require practice for effective use.
• The aux menu can generate proofs, models, theory analysis report or LaTeX picture code which is directed to the aux tabbed pane.
• Select an inference node in the tree display and the corresponding colog rule is highlighted in the theory panel; this selection also shows the relevant rule instance in the lower status label and in the aux pane. Conversely, clear node selection in the tree pane (by clicking on background) and then select an inference rule in the theory pane: This causes all inference nodes corresponding to the selected rule to be red-boxed in the tree pane.
• The toolbar has a complexity control tool: toggle the cut switch; (red color when switched ON) and adjust the selector to limit the production of new complex facts. (E.g., if cut is ON and say the selector is 3, then no rule will fire if it would introduce a fact into the tree which contains function nesting greater than 3.) The cut tool snips complex facts from the tree.
• Search can be forced to fit inside a box: depth x width. In search of a proof, one may need to enlarge the box. Click on on depth/width display on the toolbar or use B key to elicit dialog for setting box dimensions. The box mechanism can be employed to trap counter-model branches (even if initial branches are unbounded).
• From the Theory menu one can spawn a new colog processes. A spawned process can be killed using the Kill dialog under the options menu of the parent colog window.
• If a theory has hints before rules:
// hints depth=d. width=w. cut=c.where d,w,c are integers (in any order) then colog will alter the settings on load. Any flat theory (no disjunctions) will be detected and automatically set width=1. Otherwise default values are used. (Note: hints override command line parameter values, so comment out hints if necessary.)• The FOL tool tabbed pane manages translation of FOL inputs to colog inputs. One can drop a FOL file link on the panel. The terse and fore toggle buttons control the translation methods to colog code, the 2colog button attempts to translate the FOL theory to colog and install it in the colog theory pane. The show button displays the colog translation in the aux panel.
> java -jar colog14I.jar help
--------------------------------------------------------------------
colog14I 10 October 2014
> java -jar colog14I.jar help % this help
> java -jar colog14I.jar % launch the GUI
> java -jar colog14I.jar file=f [depth=d width=w cut=c log=b]
> java -jar colog14I.jar url=u [depth=d width=w cut=c log=b]
% comline run, where
% f is either a colog theory file or folder
% u is a well-formed URL description of a colog theory file
% and defaults are ...
% d = 300
% w = 1000
% c = -1 (limit complexity OFF)
% b = false
http://www.SkolemMachines.ORG
--------------------------------------------------------------------
Difficult theories may require more Java resources, e.g.,
> java -Xms6g -Xmx6g -jar colog14I.jar file=test-cl/test-cl-1000.cl width=1 depth=5000runs the theory with 6 gigs of heap. So, to run the GUI with more heap, try ...
> java -Xms6g -Xmx6g -jar colog14I.jarOne gets messages if one asks for too much!