a program discovering himself how to solve propositional calculus
If there are no quantifiers, testing validity of such formulas is equivalent to testing satisfiability of the complement of the formula.  That can be done with a SAT solver.  SAT solvers and the satisfiability problem are well-studied.  So, the minimal set of concepts needed would be: enough to solve SAT.

Statements with quantifiers are harder (QBF).  Higher-order logics are harder still.