What is LKalculus? And why LK?
It is a theorem prover, a computer program which proves logic and mathematical theorems. LK means "classic logic" and differs from the "intuitionistic logic" LJ by the calculus rules.
Which are these rules?
Lkalculus algorithm uses the Oiva Ketonen's rules: proving by contradiction we separate a list of
true statements (ipothesis) from a list of false statements (thesis) by the separator
.
The Ketonen's deduction rules are
where t is a constant defined before the rule evaluation and c is a new constant (generally) different from the constants used before. A formal system with these rules is proved to be complete, that is: if a statement is a tautology then it is provable in this system. Moreover all provable statements are tautologies.
Does LKalculus prove (or disprove) all my statements?
Unfortunately not, in this system (and in all first-order logic systems) there are undecidable propositions.