This project is currently an implementation of a proof-checker. But it is planned to be extended; for example, to support algorithm extraction from intuitionistic proofs, which is considered to be an interesting feature.
0
stars
0
forks
source link
We may write a template mechanism for automated proving of tautologies #8
Just the most straightforward and exponential one -- at the end of the propositional_lib.h, "culminating" it. So that after that there will be no more need to write many more lemmas, just one will be able to instantiate this mechanism with the desired tautology each time :)
Just the most straightforward and exponential one -- at the end of the propositional_lib.h, "culminating" it. So that after that there will be no more need to write many more lemmas, just one will be able to instantiate this mechanism with the desired tautology each time :)