Back to help contents.
The purpose of the Definite Clause Deduction Applet is to visually demonstrate
various deduction algorithms, from the SLD resolution used by Prolog to the
user manually unifying clauses. The Deduction applet accepts knowledge
bases in CILog format, and gives functions for solving a query in that
knowledge base. It also has options to view proof trees.
The File Menu has options to create graphs, load files, and save files, as
well as quitting the program.
Create New Knowledge Base - clears the currently loaded knowledge base. All
changes will be lost.
Load Sample Knowledge Base - allows the user to load from a selection of
Load From File - allows the user to load the knowledge base from an
Save Knowledge Base - allows the user to save the knowledge base as a *.pl
Load From URL - allows the user to load a file over the Internet by typing in
Print - Prints the canvas as displayed in Solve mode.
Quit - Kills the applet.
The Edit Menu allows the user to view a text representation of the knowledge
base and the proof tree.
Undo - undoes previous operation.
Redo - reverse the undo operation.
View CILog Code - displays the CILog code for the knowledge base.
View Proof Tree Text Representation - displays the text representation of the current
View XML Representation - displays the XML representation of the knowledge
The View Menu allows the user to modify the appearance of the applet
and to change what information is presented on the proof tree.
Font Size - changes the font size of the canvas display.
Line Width - changes the line thickness of the canvas display.
Autoscale - rearranges the displayed proof tree so that they fit optimally in the viewable area of the canvas. It should
be noted that when there are a lot of nodes to be displayed, the view area will be cluttered.
Pan - moves the graph around the canvas manually. This is particularly
useful when the graph has exceeded the bounds of the scrollbars. This allows
the user to drag the graph into view. To pan the canvas, depress the Pan
radio button and click and hold the right mouse button. Now drag the mouse
in the direction you want the graph to move.
Zoom - increases the view area of the canvas. To zoom, depress the zoom
radio button (this is on by default) and click and hold the right mouse
button. Now drag the mouse up to zoom in, or drag the mouse down to zoom
Reset Labels - edge labels (which contain unification information) can
be moved separately from the edge it is associated with. Resetting edge labels
snaps labels back to their associated edges.
Enable Anti-Aliasing - enable or
Show Message Panel - hides/displays the text area at the bottom of the canvas
and the knowledge base display at the bottom of the window if it is
Show Button Text - hides/displays the text labels on the toolbar buttons.
Show Buttons - hides/displays the toolbar buttons.
- Show Knowledge Base - opens an extra text area at the bottom of the window.
This area displays the current knowledge base (similar to the view in Create
Show Only Deduction's Structure - hides/displays all edge and node labels. By
default, the edge and node labels are displayed.
Edge Label Details
No Details - no edge labels are displayed. This means that no
unifier information is presented. Note that the Show
All Unifiers option does not do anything if there are
no edge details to display.
Placeholders - displays placeholder variables in place of
unification mappings. This shows where mappings have
occurred, but no other information is displayed.
Show All Unifiers - displays full unification information. This is the default.
Node Label Details
Numbers - labels the nodes by numbering them in the order that they
Atoms - shows the atoms that are (or need to be) unified for that
step of the proof tree. This is the default.
Yes Clauses - displays the full syntax of the clauses represented
by the nodes.
The Deduction Options menu allows the user to modify the behaviour of
the algorithms used to solve for a query.
- Auto Step Speed - sets the speed at which the Auto Search option unifies clauses.
Prune Irrelevant Clauses - prevents a deduction algorithm from choosing
a clause that does not work towards the unification.
Do Occurs Check - checks to see if a variable in a clause occurs in the clause that
it is being substituted into. Removing the occurs check increases efficiency
but soundness is lost.
Search Options - pops up a dialog that allows the user to modify some search
Stop Searching When An Answer is Found - causes the search
algorithm to stop once one answer is found. The default is Yes.
Max number of Search steps - defines an upper bound on the number
of steps the search algorithm does. The default is 50.
Search Tree Depth Bound - defines an upper bound on the depth
of the proof tree. The default is 50.
Atom Selection Heuristic - determines what atom the search algorithm
picks to unify if there is a choice.
First Atom - the first atom the algorithm encounters in the
order that they are defined in the knowledge base. This
is the default.
Random Atom - the algorithm picks the atom randomly.
Atom with the fewest variables - the algorithm picks the atom
with the fewest variables.
Atom with the fewest matching rules - the algorithm picks
the atom with the fewest matching rules.
Deduction Algorithms - This menu allows the user to pick what search algorithm to use.
Depth First - also known as SLD resolution. This algorithm
searches one path to its completion before trying an alternative
Breadth First - This algorithm unifies nodes in the order of their depth.
It will unify nodes of depth 0 before depth 1, depth 1 before depth 2,
and so on.
Best First - This algorithm unifies nodes that have the fewest goals to be unified.
Heuristic Depth First - This algorithm uses the same heuristic as Best First
but goes down subtrees before considering other paths. This is similar to
SLD resolution but with a heuristic function.
User Defined - allows the user to unify nodes manually.
Legend for Nodes/Edges - Opens a dialog with a legend for describing what the graph shapes/colours mean.
Opens this web page, which provides general help on the Decision Tree Learning applet.
Tutorials - Opens up the Tutorial web page. Tutorials walk through how to use the applet.
About CIspace -
Provides brief information about the CIspace project.
About this Applet -
Identifies the applet version and names of developers.
There are two ways to create a problem in the Definite Clause Deduction
Load an existing Knowledge Base - Select one of the options from the
File Menu to load an existing knowledge. After Loading an existing Knowledge
Base, edits can be made in the text area (where the canvas is).
Create a knowledge base manually - Create Mode provides a text area to input the knowledge base. Note
that the information has to be entered in CILog format.
Solve Mode graphically represents the construction of the proof tree, and allows the user to
step through the unification process, as well as inspect each step of the process.
Create New Query - pops up a dialog that allows the user to create a query for the knowledge base.
The dialog allows the user to select a predicate and input terms to query, or
(if the user is so inclined) provides a text box where the user can enter their query.
Fine Step - performs a partial step of the search/unification algorithm. Disabled if
User Defined algorithm is enabled.
- Step - performs one step of the search/unification algorithm.
Auto Search - runs the search/unification algorithm until a solution is found. Disabled if Manual Unification is enabled.
- Stop Search - Stops Auto Search if it is running.
Reset Query - clears the proof tree once a query is in the process of being solved. The problem
is reset to just the base queries.
Select Node - allows the user to move single nodes around by clicking and dragging nodes.
Inspect Node - allows the user to pull up information on how the node was derived by clicking on a node.
Move Subtree - allows the user to move a node and all of the nodes below it by clicking and dragging a node.
View Proof Deduction - when this radio button is depressed, clicking on a node pops up a frame that shows the proof
tree for the node.
Back to help contents.