A propositional theorem prover to solve planning and other problems. - Allen Van Gelder; Fumiaki Okushi (Ann. Math. Artif. Intell., 1999)

Lemma and cut strategies for propositional model elimination. - Allen Van Gelder; Fumiaki Okushi (Ann. Math. Artif. Intell., 1999)

Parallel cooperative propositional theorem proving. - Fumiaki Okushi (Ann. Math. Artif. Intell., 1999)

Persistent and Quasi-Persistent Lemmas in Propositional Model Elimination. - Fumiaki Okushi; Allen Van Gelder (Ann. Math. Artif. Intell., 2004)