## Inference Engine

26th January 2006 - By Paradochs

### Statement of Problem

The purpose of this assignment is to create a Horn clause solver. This solver must read in logical expressions, or rules, and then be able to determine if it is possible to prove a certain variable true or false. The structure of the input, rules maintenance, and proving algorithm is not specified. The significance of this problem is simple. Input can be related to percepts, and deductions can be related to actions. This program is a simple way of representing logical thinking in an AI machine. A simple conditional agent responds logically based on the rules the user/programmer inputs. Although limited, it can be very powerful if implemented correctly.

### Restrictions and limitations

The input for this program is assumed to be always correctly input by the user. The program checks for contradictions as the user enters new rules, and if the new rule is found to be contradictory it is ignored. This solver is more than a Horn clause solver. It can also solve most any clauses, by the inclusion of the Ã¢â‚¬Å“notÃ¢â‚¬Â case. For example, Ã¢â‚¬ËœaÃ¢â‚¬â„¢ is the same as not Ã¢â‚¬ËœAÃ¢â‚¬â„¢. The rules must still be inputted using the standard Horn clause format, with only one term on the right hand side and only AND operations and variables on the left. The program will check to see if the input is in a valid form. If there is an unknown character or more than one character after the implication symbol, it will return the problem and not add the rule. When the user inputs a character to prove the program can only output whether it is true, false, or maybe, but can not output how it got to that conclusion. The reason is in the next section. In some input situations, if a character is input where a number was expected, the program will exit without stating a reason.

### Explanation of Strategy

I used C++ for everything. I wrote a class Ã¢â‚¬Å“RuleÃ¢â‚¬Â to handle every clause given. It contains several constructors, a vector of chars for the left side, and a single character variable for the right side. I have two vectors of rules constantly maintained throughout the program. The main list is called rulesGiven. This is the list that the user can edit by adding new rules or removing existing ones. The other one is the inferred rules. The inferred list also contains all rules in the given list. Every time the user changes the given list, the program solves for everything that it can. When it solves that a variable is true it adds a truth rule for the character and a false rule for the conjugate variable in the inferred list. When the user inputs a character to prove, the program only has to search through the inferred list once and determine if it has proved it or not. If it hasnÃ¢â‚¬â„¢t proved it true or false, then it cannot be determined with the given information and will return Ã¢â‚¬ËœMaybeÃ¢â‚¬â„¢. This is why the path of proving can not be printed. The method of proving that I used was a backward solving algorithm. The program goes down every rule in the inferred list and when one matches the right side, it recursively calls the prove function for every character on the left side. Once a rule has completed and returned true, two things happen. The characters needed to prove the original character all have truth rules, and their conjugates all have false rules. This is the most complete and quickest way IÃ¢â‚¬â„¢ve found to implement the solver, and I have yet to find a set of rules that doesnÃ¢â‚¬â„¢t work correctly.

### Results and Analysis

I ran the program several times, trying to come up with different scenarios and different types of inferences. I tested the program many times, and have found no data that can not be processed correctly. The program does check for contradictions as the user inputs rules, so that filters out most of the types of problems that could arise when trying to prove something. Here are the simplified results of three test runs. Rules given are the rules that I input. Rules inferred are the rules the program created. Truths, falses, and maybes are the variables the program proved true, false or maybe, respectively. The program will return maybe for any variable it can not prove true or false, so if the user tries to prove a variable not given in any rule, it will always return maybe.

### Conclusions

My conclusions are simple. This program can take inputs of Horn clauses and, through deduction, prove anything and everything provable using those clauses. I am convinced that the program can handle any set of clauses, although I can not prove it as fact. I do not dismiss the possibility of there being an input set that produces erroneous results. The program is powerful and smart, with the ability to check for repetition of rules, use negated variables in proofs, and even has the ability to check for contradictions while inputting new rules. This is a very logical and robust program.

Future Research

This program could be built up to be much more powerful if a few modifications were made. First, the rule class would have to be changed to handle full expressions, without designating a left or a right. With the rule class changed, a user could input any logical expressions he needs, including ands, ors, nots, and other functions. Once this is done, a parse algorithm would have to be made to be able to determine the exact meaning of each rule. This would be the hardest part of the upgrade. The algorithm would have to detect what parts are expressions, operators, variables, truths, falses, and equivalences, and then use the rule accordingly. Another upgrade would be to let users define variables with more than one character. I will not try to explain how to implement it, because I do not know how to do it at this time. The last upgrade that I can think of is to let the user create functions. The user could define a function name, variables input, and what the function does. It would then return values of the unknown variable(s) such as in prolog. This is another part that is currently beyond me, but I hope to reach the skill level required soon.

### Instructions

Menu Appears.

- Input rules by choosing option 1.
- Use the format Ã¢â‚¬Å“AB>CÃ¢â‚¬Â for Ã¢â‚¬Å“A ^ B -> C Ã¢â‚¬Â and Ã¢â‚¬Å“AÃ¢â‚¬Â for Ã¢â‚¬Å“ true -> AÃ¢â‚¬Â
- Ã¢â‚¬Ëœ*Ã¢â‚¬â„¢ denotes a truth, Ã¢â‚¬Ëœ#Ã¢â‚¬â„¢ denotes a false. These can be used in inputs also.
- Ex: Ã¢â‚¬Å“*>AÃ¢â‚¬Â is equiv. to Ã¢â‚¬Å“#>aÃ¢â‚¬Â, and Ã¢â‚¬Å“#B>CÃ¢â‚¬Â can never be true.
- Loops input until you type 0 and press enter.
- Print the rules by choosing option 2.
- This prints both the given and the inferred lists of rules.
- Program returns to menu.
- Remove a given rule by choosing option 3.
- The given list of rules appears with the index of each rule on its left.
- Type the index of the rule you wish to remove and press enter.
- To exit without removing a rule, input 0.
- Program returns to menu.
- Prove a character by choosing option 4.
- Type the character you wish to prove and press enter.
- The computer will output whether it is true, false, or maybe.
- Program returns to menu.
- Program shuts down by choosing option 0.

### Files and C++ Code

This code has a few built in functions to time the sort and count the number of comparisons.

This code was written and compiled successfully in Visual Studio .NET.