A resolution theorem prover for intuitionistic logicTammet, TanelAutomated deduction - CADE 14 : proceedings : 14th International Conference on Automated Deduction : Townsville, North Queensland, Australia, July 13-17, 19971997 / p. 2-16 https://link.springer.com/chapter/10.1007/3-540-61511-3_65 Resolution, inverse method and the sequent calculusTammet, TanelComputational Logic and Proof Theory : 5th Kurt Gödel Colloquium, KGC'97 : Vienna, Austria, August 25-29, 1997 : proceedings1997 / p. 65-83 https://link.springer.com/content/pdf/10.1007/3-540-63385-5_33.pdf Towards efficient subsumptionTammet, TanelAutomated Deduction - CADE 15 : proceedings : 15th International Conference on Automated Deduction : Lindau, Germany, July 5-10, 19981998 / p. 427-441 https://link.springer.com/chapter/10.1007/BFb0054276