In classical logic exists law of excluded middle: (a or not a). We can append not a to the knowledge base and show contradiction. Then a is proved by contradiction. There exist effective Resolution method for automated theorem proving in this way. This idea used in Prolog.
In intuitionistic propositional logic there is no law of excluded middle. What are the algorithms for automated theorem proving?