Definite Clause Deduction |
Home | News | Older Versions | Downloads | Supported Platforms | People | Report a bug! |
Overview
Menu Help
Create Mode
Solve Mode
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 and load files, as well as quitting the program. The application version of the applet can also save files.
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 pregenerated examples.
Open Location - allows the user to load a file over the Internet by typing in a URL.
Quit - Kills the applet.
The Edit Menu allows the user to view a text representation of the knowledge base and the proof tree.
View Prolog Code - displays the CILog code for the knowledge base.
View Text Representation - displays the text representation of the current proof tree.
The Graph Options 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.
Show Control Panel - hides/displays the left control panel. Default is ON.
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.
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 occured, but no other information is displayed.
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.
Show All Unifiers - hides/displays all unifiers. If this is set to ON, all variable to constant mappings are displayed on the nodes. If this is set to OFF, only variable to constant mappings that are derived by unification are displayed. Default is OFF.
The Deduction Options menu allows the user to modify the behaviour of the algorithms used to solve for a query.
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.
Other 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.
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.
SLD Resolution - also known as depth-first search. This algorithm searches one path to its completion before trying an alternative path.
Depth First - also known as SLD resolution.
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.
Manual Unification - allows the user to unify nodes manually.
Auto Search Speed - sets the speed at which the Auto Search option unifies clauses.
Create Mode provides a text area (where the canvas is) to input the knowledge base. Note that the information has to be presented 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.
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.
Unify Node - allows the user to manually unify nodes. This radio button is only available if Manual Unification is enabled.
Inspect Node - allows the user to pull up information on how the node was derived by clicking on a node.
Move Node - allows the user to move single nodes around by clicking and dragging nodes.
Move Subtree - allows the user to move a node and all of the nodes below it by clicking and dragging a node.
View Proof Tree - when this radio button is depressed, clicking on a node pops up a frame that shows the proof tree for the node.
Step - performs one step of the search/unification algorithm. Disabled if Manual Unification is enabled.
Fine Step - performs a partial step of the search/unification algorithm. Disabled if Manual Unification is enabled.
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 Edge 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.
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. A bounding box will appear to show the user the relative position of the drawn graph.
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. A bounding box will appear to show the user the relative size of the drawn graph.
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).