# Algorithm to find a derivation in propositional calculus

Does such a algorithm exist? I mean given a set of axioms and a rule of inference (e.g. modus ponens) it should create a full derivation of a given theorem (or state that it's impossible). The possibility of deriving a theorem is relatively easy to find: just try all $2^N$ values for $N$ variables, but what about producing actual derivation?

-

It's easily possible. The simplest argument is using the British museum algorithm: Start with the axioms and in each round make all one-step derivations from the theorems you have so far. You will eventually derive all theorems. And because propositional calculus is complete, every tautology has a proof and this way you will find it.

However, this algorithm is far from efficient. There are many reasonably efficient algorithms for automated theorem proving, and for propositional logic they're decidable - either you find a proof or you'll have no way how to continue, which means there is no proof and the formula isn't a tautology.

Update: A complete example how to convert a resolution proof to a proof in some standard calculus would be quite tedious. I'll give just a sketch.

The resolution derivation rule says $$A_1\lor\ldots\lor A_n\lor B,\quad \lnot B\lor C_1\lor\ldots\lor C_m \quad\vdash\quad A_1\lor\ldots A_n\lor C_1\lor\ldots\lor C_m$$ Let's try proving it as an admissible rule for PC. Let's denote \begin{align} A &= A_1\lor\ldots\lor A_n C &= C_1\lor\ldots\lor C_m \end{align} so we should prove $$A\lor B,\; \lnot B\lor C \vdash A\lor C$$

We replace $\lor$ by its definition using $\rightarrow$: $$\lnot A\rightarrow B,\; B\rightarrow C \vdash \lnot A\rightarrow C$$ Now by the deduction theorem proving this is equivalent to proving $$\lnot A,\; \lnot A\rightarrow B,\; B\rightarrow C \vdash C$$ which is easily proved by two applications of the modus ponens rule.

So this transforms one resolution derivation into a proof in (some variant of) a classical PC calculus. Again, it uses things like the deduction theorem, which is essentially another proof transformation (converts one proof to another). By combining all these pieces, you can convert a full resolution proof into a full PC proof. Actually you could write a program in this manner that operates on proofs. There, the deduction theorem would be a function that takes a proof and converts it to another, this process we described would be another function etc.

-
As for the resolution calculus and the tableaux method - as I understand, they don't produce the actual derivation, but just allow to determine whether a formula is tautology or not. And about the first simplest algorithm - its complexity is entirely unacceptable, if I understand you correctly. I've estimated that a similar method would require about $O({2^n}^m})$ operations, where $n$ is the formula length and $m$ is number of axioms. – aplavin Oct 25 '12 at 21:14
@chersanya Yes, the complexity of the first algorithm is extreme. It's just a theoretical justification that the question is decidable. Actually both resolution and tableaux can produce a proof, but it's not a Hilbert-style proof as their derivation rules are different. With some effort, they can be converted to Hilbert-style. For example, let's take the resolution's derivation rule. If we prove that it's sound in some standard PC axiomatization, this meta-proof gives us a procedure how to convert such a resolution derivation into a standard proof. – Petr Pudlák Oct 26 '12 at 5:04
Can you explain the last point a bit? I can't get how to transform a resolution derivation into a standard proof. – aplavin Oct 26 '12 at 7:25