TY - GEN
T1 - Implementation and evaluation of contextual natural deduction for minimal logic
AU - Woltzenlogel Paleo, Bruno
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2016.
PY - 2016
Y1 - 2016
N2 - The contextual natural deduction calculus (NDc) extends the usual natural deduction calculus (ND) by allowing the implication introduction and elimination rules to operate on formulas that occur inside contexts. It has been shown that, asymptotically in the best case, NDc-proofs can be quadratically smaller than the smallest ND-proofs of the same theorems. In this paper we describe the first implementation of a theorem prover for minimal logic based on NDc. Furthermore, we empirically compare it to an equally simple ND theorem prover on thousands of randomly generated conjectures.
AB - The contextual natural deduction calculus (NDc) extends the usual natural deduction calculus (ND) by allowing the implication introduction and elimination rules to operate on formulas that occur inside contexts. It has been shown that, asymptotically in the best case, NDc-proofs can be quadratically smaller than the smallest ND-proofs of the same theorems. In this paper we describe the first implementation of a theorem prover for minimal logic based on NDc. Furthermore, we empirically compare it to an equally simple ND theorem prover on thousands of randomly generated conjectures.
UR - http://www.scopus.com/inward/record.url?scp=84978997731&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-41579-6_24
DO - 10.1007/978-3-319-41579-6_24
M3 - Conference contribution
AN - SCOPUS:84978997731
SN - 9783319415789
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 314
EP - 324
BT - Perspectives of System Informatics - 10th International Andrei Ershov Informatics Conference, PSI 2015, Revised Selected Papers
A2 - Mazzara, Manuel
A2 - Voronkov, Andrei
PB - Springer Verlag
T2 - 10th International Andrei Ershov Informatics Conference on Perspectives of System Informatics, PSI 2015
Y2 - 24 August 2015 through 27 August 2015
ER -