I was wondering if there exists any algorithm for automatic construction of nautral deduction proofs. I'm interested in propositional logic and first order logic.
If there is no algoritm, can you provide some proof of this fact?
PD0: I'm not interested in any page for solving these kind of problems. My question is more theorical.
PD1: This is not homework, just personal interest.
Usually we require the theorems of a proof system to be recursively enumerable, so you can at least write an algorithm that will eventually produce a proof of any theorem. This is usually a relatively easy algorithm to implement. Of course, if you give it something that is a non-theorem, you won't be able to tell with this approach.
For classical propositional logic, we could, of course, use truth tables to check whether something is a tautology first, and then do this search for a proof. This would give a computable (i.e. recursive) algorithm. It would be more direct and efficient to use a constructive proof of completeness for classical propositional logic though. There are certainly even more direct and efficient ways to search for a classical propositional logic proof.
For intuitionistic propositional logic, there is the proof system LJT described in Contraction-free sequent calculi for intuitionistic logic and implemented in tools like Djinn.
Theoremhood for a first-order theory in (classical or intuitionistic) first-order logic is generally not computable. Some particular first-order theories are decidable, but most aren't. They are at least semi-decidable via the argument in the first paragraph. There are, of course, tons of automated theorem provers that will attempt to find proofs, but they may fail. For theorems, they may fail due to resource limitations1. For non-theorems, they just don't have a way of showing that something is contingent. They could find a proof for the negation of your formula, but that technically doesn't rule out your formula being a theorem since your theory could be inconsistent. Model checking techniques could be used to attempt to find counter-models to show that some formula can't be a theorem (but may still be contingent). Most model checking tools are not aimed at full first-order logic though. They have essentially the same theoretical and practical limitations as automated theorem provers.
1 Just because something is computable doesn't mean it's computable within our universe.
