1
$\begingroup$

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?

1 Answers 1

1

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.

  • 0
    Can you explain the last point a bit? I can't get how to transform a resolution derivation into a standard proof.2012-10-26