New answers tagged lo.logic
0
I cannot comment so I'll try to give an answer:
from what I understand the OP is right: in most (all ?) FOL engine, you can of course add your own axioms but not your own axioms schemata (that is why you often hear that 'ATP cannot be applied to non finitely axiomatisable theories'). You can have a look at metamath, in which each theorem is in fact a theorem ...
Top 50 recent answers are included
