Ri-tries, prime implicates, and treewidth

Implicates and prime implicates are fundamental objects in the study of propositional formulas, playing a significant role in knowledge compilation, theory revision, abductive reasoning, and code generation. Ri-tries and the pi-trie algorithm respectively are novel tools for discovering and manipulating implicates and prime implicates. In this thesis we develop these tools and prove their correctness, along with other useful properties such as runtime and some associated lower bounds of difficulty. In addition, we display a version of pi-trie which takes advantage of formulas with simple graph-theoretic structure to effect a speedup.