Implementation and evaluation of contextual natural deduction for minimal logic

Bruno Woltzenlogel Paleo

doi:10.1007/978-3-319-41579-6_24

Implementation and evaluation of contextual natural deduction for minimal logic

Bruno Woltzenlogel Paleo^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › peer-review

1 Citation (Scopus)

Abstract

The contextual natural deduction calculus (ND^c) 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, ND^c-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 ND^c. Furthermore, we empirically compare it to an equally simple ND theorem prover on thousands of randomly generated conjectures.

Original language	English
Title of host publication	Perspectives of System Informatics - 10th International Andrei Ershov Informatics Conference, PSI 2015, Revised Selected Papers
Editors	Manuel Mazzara, Andrei Voronkov
Publisher	Springer Verlag
Pages	314-324
Number of pages	11
ISBN (Print)	9783319415789
DOIs	https://doi.org/10.1007/978-3-319-41579-6_24
Publication status	Published - 2016
Event	10th International Andrei Ershov Informatics Conference on Perspectives of System Informatics, PSI 2015 - Kazan and Innopolis, Russian Federation Duration: 24 Aug 2015 → 27 Aug 2015

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9609
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	10th International Andrei Ershov Informatics Conference on Perspectives of System Informatics, PSI 2015
Country/Territory	Russian Federation
City	Kazan and Innopolis
Period	24/08/15 → 27/08/15

Access to Document

10.1007/978-3-319-41579-6_24

Cite this

Woltzenlogel Paleo, B. (2016). Implementation and evaluation of contextual natural deduction for minimal logic. In M. Mazzara, & A. Voronkov (Eds.), Perspectives of System Informatics - 10th International Andrei Ershov Informatics Conference, PSI 2015, Revised Selected Papers (pp. 314-324). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9609). Springer Verlag. https://doi.org/10.1007/978-3-319-41579-6_24

Woltzenlogel Paleo, Bruno. / Implementation and evaluation of contextual natural deduction for minimal logic. Perspectives of System Informatics - 10th International Andrei Ershov Informatics Conference, PSI 2015, Revised Selected Papers. editor / Manuel Mazzara ; Andrei Voronkov. Springer Verlag, 2016. pp. 314-324 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{688634e313ff444aba135cb46a736d0e,

title = "Implementation and evaluation of contextual natural deduction for minimal logic",

abstract = "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.",

author = "\{Woltzenlogel Paleo\}, Bruno",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2016.; 10th International Andrei Ershov Informatics Conference on Perspectives of System Informatics, PSI 2015 ; Conference date: 24-08-2015 Through 27-08-2015",

year = "2016",

doi = "10.1007/978-3-319-41579-6\_24",

language = "English",

isbn = "9783319415789",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "314--324",

editor = "Manuel Mazzara and Andrei Voronkov",

booktitle = "Perspectives of System Informatics - 10th International Andrei Ershov Informatics Conference, PSI 2015, Revised Selected Papers",

address = "Germany",

}

Woltzenlogel Paleo, B 2016, Implementation and evaluation of contextual natural deduction for minimal logic. in M Mazzara & A Voronkov (eds), Perspectives of System Informatics - 10th International Andrei Ershov Informatics Conference, PSI 2015, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9609, Springer Verlag, pp. 314-324, 10th International Andrei Ershov Informatics Conference on Perspectives of System Informatics, PSI 2015, Kazan and Innopolis, Russian Federation, 24/08/15. https://doi.org/10.1007/978-3-319-41579-6_24

Implementation and evaluation of contextual natural deduction for minimal logic. / Woltzenlogel Paleo, Bruno.
Perspectives of System Informatics - 10th International Andrei Ershov Informatics Conference, PSI 2015, Revised Selected Papers. ed. / Manuel Mazzara; Andrei Voronkov. Springer Verlag, 2016. p. 314-324 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9609).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › peer-review

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 - https://www.scopus.com/pages/publications/84978997731

U2 - 10.1007/978-3-319-41579-6_24

DO - 10.1007/978-3-319-41579-6_24

M3 - Conference Paper

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 -

Woltzenlogel Paleo B. Implementation and evaluation of contextual natural deduction for minimal logic. In Mazzara M, Voronkov A, editors, Perspectives of System Informatics - 10th International Andrei Ershov Informatics Conference, PSI 2015, Revised Selected Papers. Springer Verlag. 2016. p. 314-324. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-41579-6_24

Implementation and evaluation of contextual natural deduction for minimal logic

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this