Back to help contents.

Contents

Overview

Menu Help

Create Mode

Solve Mode

Overview

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.

Menu Help

File Menu

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

• Load From File - allows the user to load the knowledge base from an existing file.

• Save Knowledge Base - allows the user to save the knowledge base as a *.pl file.

• Load From URL - allows the user to load a file over the Internet by typing in a URL.

• Print - Prints the canvas as displayed in Solve mode.

• Quit - Kills the applet.

Edit Menu

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 proof tree.

• View XML Representation - displays the XML representation of the knowledge base.

View Menu

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/Zoom

  • 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 out.

• 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 disable anti-aliasing.

• 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 displayed.

• 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 mode).

• 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 are unified.

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

Deduction Options

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

  • 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 path.

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

Help Menu

• Legend for Nodes/Edges - Opens a dialog with a legend for describing what the graph shapes/colours mean.

• Help - 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.

Create Mode

There are two ways to create a problem in the Definite Clause Deduction Applet.

1. 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).

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

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.

Toolbar Buttons

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