This project focuses on the specification of domain-independent theories of problem solving. Most problem solving knowledge is implicit in the programs that have been written to solve problems. This project seeks to make explicit the problem solving knowledge in logic. Currently the system is focusing on the axioms for weak-methods such as means-ends analysis and forward-chaining. This project is also interested with the development of meta-level knowledge that operates over the declarative problem solving theories.