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