0

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?

Oleg Dats
  • 425
  • 1
    You can see e.g. M.Fitting, Proof Methods for Modal and Intuitionistic Logics – Mauro ALLEGRANZA Apr 01 '21 at 12:42
  • 1
    In this answer: https://math.stackexchange.com/questions/2470868/propositional-logic-proving-contingency-without-truthtable/2475949 I outline a sequent calculus system due to Roy Dyckhoff which has the property that any search for a proof using the rules will terminate, and it's complete and sound for intuitionistic propositional logic. This is essentially the algorithm used by Coq's tauto tactic (though with some optimizations using the fact that some of the reductions are reversible and so can be applied unconditionally without needing to consider "back tracking"). – Daniel Schepler Apr 01 '21 at 17:35

0 Answers0