refs.bib

%% This BibTeX bibliography file was created using BibDesk.
%% http://bibdesk.sourceforge.net/

%% Created for Mclaughlin, Sean at 2016-01-06 09:18:44 -0500 


%% Saved with string encoding Unicode (UTF-8) 


@string{lics95 = {10th Symp.\ on Logic in Computer Science}}

@string{tocl = {ACM Trans.\ on Computational Logic}}


@techreport{Franzen.1989.TR,
	Address = {Stockholm},
	Author = {Torkel Franz{\'e}n},
	Date-Added = {2016-01-06 14:17:29 +0000},
	Date-Modified = {2016-01-06 14:18:43 +0000},
	Institution = {Swedish Institute of Computer Science},
	Number = {R8906},
	Title = {Algorithmic Aspects of Intuitionistic Propositional Logic},
	Type = {Research Report},
	Year = {1987}}

@techreport{Franzen.1987.TR,
	Address = {Stockholm},
	Author = {Torkel Franz{\'e}n},
	Date-Added = {2016-01-06 14:16:47 +0000},
	Date-Modified = {2016-01-06 14:18:25 +0000},
	Institution = {Swedish Institute of Computer Science},
	Number = {R870X},
	Title = {Algorithmic Aspects of Intuitionistic Propositional Logic},
	Type = {Research Report},
	Year = {1987}}

@article{Ferrari.2012.TCL,
	Author = {Mauro Ferrari and Camillo Fiorentini and Guido Fiorino},
	Bibdate = {2012-05-10},
	Bibsource = {DBLP, http://dblp.uni-trier.de/db/journals/tocl/tocl13.html#FerrariFF12},
	Date-Added = {2016-01-06 14:15:05 +0000},
	Date-Modified = {2016-01-06 14:15:24 +0000},
	Journal = {ACM Trans. Comput. Log},
	Number = {2},
	Pages = {14},
	Title = {Simplification Rules for Intuitionistic Propositional Tableaux},
	Url = {http://doi.acm.org/10.1145/2159531.2159536},
	Volume = {13},
	Year = {2012},
	Bdsk-Url-1 = {http://doi.acm.org/10.1145/2159531.2159536}}

@article{Hudelmaier.1992.AML,
	Author = {J{\"o}rg Hudelmaier},
	Date-Added = {2016-01-05 14:44:07 +0000},
	Date-Modified = {2016-01-05 14:44:20 +0000},
	Journal = {Archive for Mathematical Logic},
	Pages = {331--353},
	Title = {Bounds on Cut-Elimination in Intuitionistic Propositional Logic},
	Volume = {31},
	Year = {1992}}

@phdthesis{Hudelmaier.1989.Thesis,
	Address = {T{\"u}bingen},
	Author = {J{\"o}rg Hudelmaier},
	Date-Added = {2016-01-05 14:43:32 +0000},
	Date-Modified = {2016-01-05 14:43:47 +0000},
	School = {University of T{\"u}bingen},
	Title = {Bounds for cut elimination in intuitionistic propositional logic},
	Year = {1989}}

@article{Vorobev.1958.AMST,
	Annote = {Translated from the Russian in AMST, 1970},
	Author = {Vorob'ev, N.N.},
	Date-Added = {2016-01-05 14:20:55 +0000},
	Date-Modified = {2016-01-05 14:21:16 +0000},
	Journal = {American Mathematical Society Translations},
	Number = {2},
	Pages = {37--71},
	Title = {A new algorithm for derivability in the constructive propositional calculus},
	Volume = {94},
	Year = {1970}}

@article{Andreoli.1992.JLC,
	Author = {Jean-Marc Andreoli},
	Date-Added = {2016-01-05 14:19:26 +0000},
	Date-Modified = {2016-01-05 14:19:26 +0000},
	Journal = jlc,
	Number = {3},
	Pages = {297--347},
	Title = {Logic Programming with Focusing Proofs in Linear Logic},
	Volume = {2},
	Year = {1992}}

@inproceedings{Herbelin.1994.CSL,
	Author = {Hugo Herbelin},
	Bibdate = {2009-09-22},
	Bibsource = {DBLP, http://dblp.uni-trier.de/db/conf/csl/csl94.html#Herbelin94},
	Booktitle = {CSL},
	Date-Added = {2016-01-05 14:11:10 +0000},
	Date-Modified = {2016-01-05 14:50:16 +0000},
	Editor = {Leszek Pacholski and Jerzy Tiuryn},
	Isbn = {3-540-60017-5},
	Pages = {61--75},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {A Lambda-Calculus Structure Isomorphic to Gentzen-Style Sequent Calculus Structure},
	Url = {http://dx.doi.org/10.1007/BFb0022247},
	Volume = {933},
	Year = {1994},
	Bdsk-Url-1 = {http://dx.doi.org/10.1007/BFb0022247}}

@phdthesis{Ketonen.1944.Thesis,
	Author = {Oiva Ketonen},
	Date-Added = {2016-01-05 13:58:51 +0000},
	Date-Modified = {2016-01-05 14:00:45 +0000},
	School = {Helsinki},
	Title = {Untersuchungen zum Pr\"adikatenkalk\"ul},
	Year = {1944}}

@inproceedings{Nigam.2008.IJCAR,
	Author = {Vivek Nigam and Dale Miller},
	Bibdate = {2008-09-05},
	Bibsource = {DBLP, http://dblp.uni-trier.de/db/conf/cade/ijcar2008.html#NigamM08},
	Booktitle = {Automated Reasoning, 4th International Joint Conference, {IJCAR} 2008, Sydney, Australia, August 12-15, 2008, Proceedings},
	Date-Added = {2016-01-04 15:42:32 +0000},
	Date-Modified = {2016-01-04 15:43:16 +0000},
	Editor = {Alessandro Armando and Peter Baumgartner and Gilles Dowek},
	Isbn = {978-3-540-71069-1},
	Pages = {507--522},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {Focusing in Linear Meta-logic},
	Url = {http://dx.doi.org/10.1007/978-3-540-71070-7_42},
	Volume = {5195},
	Year = {2008},
	Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-540-71070-7_42}}

@article{Smullyan.1968.JSL,
	Author = {Raymond M. Smullyan},
	Date-Added = {2016-01-04 15:01:21 +0000},
	Date-Modified = {2016-01-04 15:01:32 +0000},
	Journal = {J. of Symbolic Logic},
	Number = {4},
	Pages = {560--564},
	Title = {Analytic Cut},
	Volume = {33},
	Year = {1968}}

@inproceedings{Mints.1994.CP,
	Author = {G. Mints},
	Booktitle = {Constraint Programming: Proceedings 1993 {NATO} {ASI} Parnu, Estonia},
	Chapter = {3.4},
	Date-Added = {2016-01-04 13:53:38 +0000},
	Date-Modified = {2016-01-04 13:53:53 +0000},
	Editor = {B. Mayoh and E. Tyugu and J. Penjaam},
	Isbn = {3-540-57859-5},
	Pages = {282--304},
	Publisher = {Springer},
	Series = {NATO Advanced Science Institute Series},
	Title = {Resolution Strategies for the Intuitionistic Logic},
	Year = {1994}}

@article{Maehara.1954.NMJ,
	Author = {S. Maehara},
	Date-Added = {2016-01-04 04:26:15 +0000},
	Date-Modified = {2016-01-04 04:26:31 +0000},
	Journal = {Nagoya Mathematical Journal},
	Pages = {45--64},
	Title = {Eine Darstellung der intuitionistischen Logik in der klassischen},
	Year = {1954}}

@article{Egly.1999.FI,
	Author = {Egly and Schmitt},
	Date-Added = {2016-01-04 04:23:42 +0000},
	Date-Modified = {2016-01-04 04:23:55 +0000},
	Journal = {FUNDINF: Fundamenta Informatica},
	Publisher = {IOS Press},
	Title = {On Intuitionistic Proof Transformations, their Complexity, and Application to Constructive Program Synthesis},
	Volume = {39},
	Year = {1999}}

@inproceedings{Mints.1988.CCL,
	Author = {Grigori Mints},
	Booktitle = {Conference on Computer Logic (1988)},
	Date-Added = {2016-01-03 17:22:19 +0000},
	Date-Modified = {2016-01-03 17:22:40 +0000},
	Editor = {Per Martin-L{\"o}f and Grigori Mints},
	Pages = {198--231},
	Publisher = {Springer},
	Series = {Lecture Notes in Computer Science},
	Title = {Gentzen-type systems and resolution rules. Part {I}. Propositional logic},
	Volume = {417},
	Year = {1990}}

@misc{Dyckhoff.2008.Oasis,
	Author = {Roy Dyckhoff},
	Date-Added = {2016-01-03 17:16:53 +0000},
	Date-Modified = {2016-01-03 17:18:02 +0000},
	Howpublished = {Lecture Notes},
	Month = {October},
	Title = {Proof systems for intuitionistic logic},
	Year = {2008}}

@misc{Dyckhoff.1997.LJT,
	Author = {Roy Dyckhoff},
	Date-Added = {2016-01-03 15:08:50 +0000},
	Date-Modified = {2016-01-03 15:08:50 +0000},
	Title = {A Prolog implementation of {LJT}},
	Url = {http://www.cs.st-andrews.ac.uk/~rd/logic/nonmac/LJT.pl.html},
	Year = {1997},
	Bdsk-Url-1 = {http://www.cs.st-andrews.ac.uk/~rd/logic/nonmac/LJT.pl.html}}

@inproceedings{Heuerding.1996.Tableaux,
	Address = {Berlin},
	Author = {Alain Heuerding and Michael Seyfried and Heinrich Zimmermann},
	Booktitle = {Proceedings of the 5th International Workshop on Theorem Proving with analytic Tableaux and Related Methods ({TABLEAUX})},
	Date-Added = {2016-01-03 14:58:27 +0000},
	Date-Modified = {2016-01-03 14:58:39 +0000},
	Editor = {P. Migliolo and U. Moscato and D. Mundici and M. Ornaghi},
	Isbn = {3-540-61208-4},
	Month = may # {~15--17},
	Pages = {210--225},
	Publisher = {Springer},
	Series = {LNAI},
	Title = {Efficient loop-check for backward proof search in some non-classical propositional logics},
	Volume = {1071},
	Year = {1996}}

@inproceedings{Stoughton.1996.CADE,
	Author = {Allen Stoughton},
	Booktitle = {CADE-13 Workshop on Proof Search in Type-Theoretic Languages},
	Date-Added = {2016-01-03 14:54:25 +0000},
	Date-Modified = {2016-01-03 14:54:25 +0000},
	Pages = {109--116},
	Title = {porgi: a {P}roof-{O}r-{R}efutation {G}enerator for {I}ntuitionistic propositional logic},
	Year = 1996,
	Bdsk-Url-1 = {ftp://ftp.cis.ksu.edu/pub/CIS/Stoughton/porgi.ps.gz}}

@inproceedings{Pinto.1995.SG,
	Author = {Luis Pinto and Roy Dyckhoff},
	Booktitle = {Symposia Gaussiana, Conference~A},
	Date-Added = {2016-01-03 14:50:06 +0000},
	Date-Modified = {2016-01-03 14:50:20 +0000},
	Editor = {Behara and Fritsch and Lintz},
	Pages = {225--232},
	Publisher = {Walter de Gruyter, Berlin},
	Title = {Loop-free construction of counter-models for intuitionistic propositional logic},
	Year = {1995}}

@article{Sperner.1928.MZ,
	Author = {E. Sperner},
	Date-Added = {2016-01-03 02:29:05 +0000},
	Date-Modified = {2016-01-03 02:29:54 +0000},
	Journal = {Mathematische Zeitschrift},
	Pages = {544--548},
	Title = {Ein {S}atz {\"u}ber die {U}ntermengen einer endlichen {M}enge},
	Volume = {27},
	Year = {1928}}

@article{Hudelmaier.1993.JLC,
	Author = {J{\"o}rg Hudelmaier},
	Date-Added = {2016-01-03 02:10:22 +0000},
	Date-Modified = {2016-01-03 02:10:40 +0000},
	Journal = {Journal of Logic and Computation},
	Month = feb,
	Number = {1},
	Pages = {63--75},
	Title = {An {$O(n \log n)$}-Space Decision Procedure for Intuitionistic Propositional Logic},
	Volume = {3},
	Year = {1993}}

@incollection{Ladner.1977.SJC,
	Author = {R. E. Ladner},
	Booktitle = {SIAM Journal of Computation},
	Date-Added = {2016-01-02 13:19:25 +0000},
	Date-Modified = {2016-01-03 14:55:33 +0000},
	Title = {The computational complexity of provability in systems of modal propositional logic},
	Year = {1977}}

@inproceedings{Howe.1997.Tableaux,
	Address = {Berlin},
	Author = {Jacob M. Howe},
	Booktitle = {Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods},
	Date-Added = {2015-12-29 19:11:46 +0000},
	Date-Modified = {2015-12-29 19:12:12 +0000},
	Editor = {Didier Galmiche},
	Pages = {188--200},
	Publisher = {Springer},
	Series = {LNAI},
	Title = {Two Loop Detection Mechanisms: {A} Comparison},
	Volume = {1227},
	Year = {1997}}

@book{Gabbay.2000.GoalDirectedProofTheory,
	Author = {Dov M. Gabbay and Nicola Olivetti},
	Date-Added = {2015-12-29 18:52:06 +0000},
	Date-Modified = {2015-12-29 18:52:28 +0000},
	Publisher = {Kluwer Academic Publishers},
	Series = {Applied Logic Series},
	Title = {Goal-Directed Proof Theory},
	Volume = {21},
	Year = {2000}}

@article{Dyckhoff.1992.JSL,
	Author = {Roy Dyckhoff},
	Date-Added = {2015-12-29 18:20:44 +0000},
	Date-Modified = {2015-12-29 18:20:58 +0000},
	Journal = {Journal of Symbolic Logic},
	Pages = {795--807},
	Title = {Contraction-free sequent calculi for intuitionistic logic},
	Volume = {57},
	Year = {1992}}

@webpage{Agda,
	Date-Added = {2015-12-29 15:38:21 +0000},
	Date-Modified = {2016-01-03 14:35:00 +0000},
	Url = {http://wiki.portal.chalmers.se/agda/pmwiki.php},
	Bdsk-Url-1 = {http://wiki.portal.chalmers.se/agda/pmwiki.php}}

@webpage{Coq,
	Date-Added = {2015-12-29 15:37:58 +0000},
	Date-Modified = {2016-01-03 14:35:09 +0000},
	Url = {https://coq.inria.fr/},
	Bdsk-Url-1 = {https://coq.inria.fr/}}

@webpage{Djinn,
	Date-Added = {2015-12-29 15:33:41 +0000},
	Date-Modified = {2016-01-03 14:35:17 +0000},
	Url = {https://hackage.haskell.org/package/djinn},
	Bdsk-Url-1 = {https://hackage.haskell.org/package/djinn}}

@article{Statman.1979.TCS,
	Author = {R. Statman},
	Date-Added = {2015-12-29 14:42:56 +0000},
	Date-Modified = {2015-12-29 14:43:09 +0000},
	Journal = {Theoretical Computer Science},
	Key = {Statman 79},
	Pages = {67--72},
	Title = {Intuitionistic Propositional Logic is Polynomial-Space Complete},
	Volume = {9},
	Year = {1979}}

@inproceedings{Cook.1971.TOC,
	Author = {Stephen A. Cook},
	Booktitle = {Proceedings of the Third {ACM} Symposium on Theory of Computing},
	Date-Added = {2015-12-29 14:40:10 +0000},
	Date-Modified = {2015-12-29 14:41:09 +0000},
	Pages = {151--158},
	Title = {The Complexity of Theorem Proving Procedures},
	Topic = {complexity-theory;},
	Year = {1971}}

@article{Glivenko.1929.BCS,
	Author = {V. Glivenko},
	Date-Added = {2015-12-29 14:37:09 +0000},
	Date-Modified = {2015-12-29 16:25:45 +0000},
	Journal = {Bulletins de la classe des sciences},
	Pages = {183--188},
	Publisher = {Academie Royale de Belgique},
	Series = {5},
	Title = {Sur Quelques Points de la Logique de {M}. Brouwer},
	Volume = {15},
	Year = {1929}}

@article{Goedel.1933.EMK,
	Author = {Kurt G{\"o}del},
	Date-Added = {2015-12-29 14:30:20 +0000},
	Date-Modified = {2015-12-29 14:31:59 +0000},
	Journal = {Ergebnisse eines Mathematischen Kolloquiums},
	Pages = {34--38},
	Title = {Zur intuitionistischen Arithmetik und Zahlentheorie},
	Year = {1933}}

@article{Gentzen.1935.MZ,
	Author = {Gerhard Gentzen},
	Date-Added = {2015-12-29 14:24:15 +0000},
	Date-Modified = {2015-12-29 16:25:54 +0000},
	Journal = {Mathematische Zeitschrift},
	Pages = {176--210, 405--431},
	Title = {Untersuchungen {\"u}ber das {L}ogische {S}chliessen},
	Volume = {39},
	Year = {1935}}

@phdthesis{Brouwer.1907.Thesis,
	Author = {Brouwer, L.E.J},
	Date-Added = {2015-12-29 14:16:26 +0000},
	Date-Modified = {2015-12-29 14:17:08 +0000},
	School = {Universiteit van Amsterdam},
	Title = {Over de Grondslagen der Wiskunde},
	Year = {1907}}

@inproceedings{Riazanov.1999.CADE,
	Address = {Berlin},
	Author = {Alexandre Riazanov and Andrei Voronkov},
	Booktitle = {Proceedings of the 16th International Conference on Automated Deduction ({CADE}-16-99)},
	Date-Added = {2015-12-28 23:09:36 +0000},
	Date-Modified = {2015-12-29 16:25:30 +0000},
	Editor = {Harald Ganzinger},
	Isbn = {3-540-66222-7},
	Month = jul # {~7--10},
	Pages = {292--296},
	Publisher = {Springer},
	Series = {LNAI},
	Title = {Vampire},
	Volume = {1632},
	Year = {1999}}

@inproceedings{Hustadt.1998.Tableaux,
	Address = {Berlin},
	Author = {Ullrich Hustadt and Renate A. Schmidt},
	Booktitle = {Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods},
	Date-Modified = {2015-12-29 16:24:30 +0000},
	Pages = {187--201},
	Publisher = {Springer},
	Series = {LNAI},
	Title = {Simplification and Backjumping in Modal Tableau},
	Volume = {1397},
	Year = {1998}}

@inproceedings{Pfenning.1995.LICS,
	Address = {San Diego, California},
	Author = {Frank Pfenning},
	Booktitle = lics95,
	Date-Modified = {2015-12-29 16:23:43 +0000},
	Organization = {IEEE Computer Society Press},
	Pages = {156--166},
	Title = {Structural Cut Elimination},
	Year = {1995}}

@article{Pfenning.2000.IC,
	Author = {Frank Pfenning},
	Date-Modified = {2015-12-29 16:23:31 +0000},
	Journal = {Information and Computation},
	Month = mar,
	Number = {1/2},
	Pages = {84--141},
	Title = {Structural Cut Elimination {I}. {I}ntuitionistic and Classical Logic},
	Volume = 157,
	Year = 2000}

@article{Simmons.2014.TOCL,
	Author = {Robert J. Simmons},
	Date-Modified = {2015-12-29 16:24:01 +0000},
	Doi = {10.1145/2629678},
	Journal = tocl,
	Number = 3,
	Pages = 21,
	Title = {Structural Focalization},
	Volume = 15,
	Year = 2014,
	Bdsk-Url-1 = {http://dx.doi.org/10.1145/2629678}}