Horn formula minimization
Tom Chang · RIT Scholar Works (Rochester Institute of Technology) · 2006
Horn formulas make up an important subclass of Boolean formulas that exhibits interesting and useful computational properties. They have been widely studied due to the fact that the satisfiability problem for Horn formulas is solvable in linear time. Also resulting from this, Horn formulas play an important role in the field of artificial intelligence. The minimization problem of Horn formulas is to reduce the size of a given Horn formula to find a shortest equivalent representation. Many knowledge bases in propositional expert systems are represented as Horn formulas. Therefore the minimization of Horn formulas can be used to reduce the size of these knowledge bases, thereby increasing the efficiency of queries. The goal of this project is to study the properties of Horn formulas and the minimization of Horn formulas. Topics discussed include The satisfiability problem for Horn formulas. NP-completeness of Horn formula minimization. Subclasses of Horn formulas for which the minimization problem is solvable in polynomial time. Approximation algorithms for Horn formula minimization.