<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
% requires abbrev.bib

% *** logic textbooks (primarily classical logic) 

@BOOK{Kle:intm,
	AUTHOR = "S. C. Kleene",
	TITLE = "Introduction to Metamathematics",
	SERIES = "Bibliotheca Mathematica",
	VOLUME = 1,
	PUBLISHER = nh,
	ADDRESS = "Amsterdam",
	YEAR = 1952		
}

@BOOK{Fit:symli,
	AUTHOR = "Frederic B. Fitch",
	TITLE = "Symbolic Logic: An Introduction",
	PUBLISHER = "The Ronald Press Company",
	ADDRESS = "New York",
	YEAR = 1952
}

@BOOK{Men:intml,
	AUTHOR = "Elliott Mendelson",
	TITLE = "Introduction to Mathematical Logic",
	SERIES = "Wadsworth Mathematical Series",
	EDITION = "3rd",
	PUBLISHER = "Wadsworth {\&} Brooks / 
		Cole Advanced Books {\&} Software",
	ADDRESS = "Monterey, CA",
	YEAR = 1987,
	NOTE = "(1st ed., D.~Van Nostrand Co., Princeton, NJ, 1964; 
		2nd ed., D.~Van Nostrand Co., New York, 1979)"
}

@BOOK{Smu:firol,
	AUTHOR = "Raymond M. Smullyan",
	TITLE = "First-Order Logic",
	SERIES = "Ergebnisse der Mathematik unde ihrer Grenzgebiete",
	VOLUME = 43,
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1968
}
		  
@BOOK{vD:logs,
	AUTHOR = "Dirk {van Dalen}",
	TITLE = "Logic and Structure",
	EDITION = "3rd, augmented",
	SERIES = utext,
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1994,
	NOTE = "(1st ed., 1980; 2nd ed., 1983)"
}	
		  
@BOOK{EFT:matl,
	AUTHOR = "Heinz-Dieter Ebbinghaus and J{\"o}rg Flum 
		and Wolfgang Thomas",
	TITLE = "Mathematical Logic",
	EDITION = "2nd",
	SERIES = utm,
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1994,
	NOTE = "(1st ed., 1984)"
}
		  
@INCOLLECTION{Bar:intfol,
	AUTHOR = "Jon Barwise",
	TITLE = "An Introduction to First-Order Logic",
	EDITOR = "J. Barwise",
	BOOKTITLE = "Handbook of Mathematical Logic",
	SERIES = slfm,
	VOLUME = 90,
	CHAPTER = "A.1",
	PAGES = "5--46",
	PUBLISHER = nh,
	ADDRESS = "Amsterdam",
	YEAR = 1977
}

@INCOLLECTION{Hod:elepl,
	AUTHOR = "Wilfrid Hodges",
	TITLE = "Elementary Predicate Logic",
	EDITOR = "D. Gabbay and F. Guenthner",
	BOOKTITLE = "Handbook of Philosophical Logic, Volume {I}:
		Elements of Classical Logic",
	SERIES = synthl,
	VOLUME = 164,
	CHAPTER = "I.1",
	PAGES = "1--131",
	PUBLISHER = reidel,
	ADDRESS = "Dordrecht",
	YEAR = 1983
}

@BOOK{And:intmlt,
	AUTHOR = "Peter B. Andrews",
	TITLE = "An Introduction to Mathematical Logic and Type Theory:
		To Truth Through Proof",
	SERIES = "Computer Science and Applied Mathematics",
	PUBLISHER = ap,
	ADDRESS = "Orlando, FL",
	YEAR = 1986
}
@BOOK{Bor:comcl,
	AUTHOR = "Egon B{\"o}rger",
	TITLE = "Computability, Complexity, Logic",
	SERIES = slfm,
	VOLUME = 128,
	PUBLISHER = nh,
	ADDRESS = "Amsterdam",
	YEAR = 1989
}

@BOOK{Pra:abcsl,
	AUTHOR = "Dag Prawitz",
	TITLE = "ABC i symbolisk logik: Logikens spr{\aa}k och grundbegrepp",
	PUBLISHER = "Thales",
	ADDRESS = "Stockholm",
	YEAR = 1975
}	  	  
		  
@BOOK{Kri:loggdl,
	AUTHOR = "Jan Kristoferson",
	TITLE = "Logik: Grundkurs f{\"o}r {D}-linjen",
	PUBLISHER = "s.n.",
	ADDRESS = "s.l.",
	YEAR = 1994
}

@BOOK{Cam:setlc,
	AUTHOR = "Peter J. Cameron",
	TITLE = "Sets, Logic and Categories",
	SERIES = sums,
	PUBLISHER = springer,
	ADDRESS = "London",
	YEAR = 1999
}
		
% *** models and completeness
		  
@BOOK{CK:modt,
	AUTHOR = "Chen Chung Chang and H. Jerome Keisler",
	TITLE = "Model Theory",
	EDITION = "3rd",
	SERIES = slfm,
	VOLUME = 73,
	PUBLISHER = nh,
	ADDRESS = "Amsterdam",
	YEAR = 1990,
	NOTE = "(1st ed., 1973; 2nd ed., 1977)"		  
}

@INCOLLECTION{Kei:funmt,
	AUTHOR = "H. Jerome Keisler",
	TITLE = "Fundamentals of Model Theory",
	EDITOR = "J. Barwise",
	CHAPTER = "A.2",
	BOOKTITLE = "Handbook of Mathematical Logic",
	SERIES = slfm,
	VOLUME = 90,
	PAGES = "47--103",
	PUBLISHER = nh,
	ADDRESS = "Amsterdam",
	YEAR = 1977
}

% siia oleks vaja Hodges'i uut raamatut ka, samuti Doetsi oma

@INCOLLECTION{Leb:altsfo,
	AUTHOR = "Hugues Leblanc",
	TITLE = "Alternatives to Standard First-Order Semantics",
	EDITOR = "D. Gabbay and F. Guenthner",
	BOOKTITLE = "Handbook of Philosophical Logic, Volume {I}:
		Elements of Classical Logic",
	SERIES = synthl,
	VOLUME = 164,
	CHAPTER = "I.3",
	PAGES = "189--274",
	PUBLISHER = reidel,
	ADDRESS = "Dordrecht",
	YEAR = 1983
}

@INCOLLECTION{Smo:inct,
	AUTHOR = "C. Smorynski",
	TITLE = "The Incompleteness Theorems",
	EDITOR = "J. Barwise",
	CHAPTER = "D.1",
	BOOKTITLE = "Handbook of Mathematical Logic",
	SERIES = slfm,
	VOLUME = 90,
	PAGES = "821--865",
	PUBLISHER = nh,
	ADDRESS = "Amsterdam",
	YEAR = 1977
}

@ARTICLE{Put:modr,
	AUTHOR = "Hilary Putnam",
	TITLE = "Models and Reality",
	JOURNAL = jsl,
	VOLUME = 45,
	NUMBER = 3,
	PAGES = "464--482",
	YEAR = 1980
}

@INCOLLECTION{Hin:newfmt,
	AUTHOR = "Jaakko Hintikka",
	TITLE = "New Foundations for Mathematical Theories",
	EDITOR = "J. Oikkonen and J. V{\"a}{\"a}n{\"a}nen",
	BOOKTITLE = "Proc.\ of ASL Summer Meeting, Logic Colloquium '90, 
		Helsinki, Finland, 15--22 July 1990",
	SERIES = lnl,
	VOLUME = 2,
	PAGES = "122--144",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1993
}
 
 
% *** proof theory

@BOOK{Sch:prot,
	AUTHOR = "Kurt Sch{\"u}tte",
	TITLE = "Proof Theory",
	SERIES = "Grundlehren der mathematische Wissenschaften",
	VOLUME = 225,
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1977
}

@INCOLLECTION{Sch:protml,
	AUTHOR = "Kurt Sch{\"u}tte",
	TITLE = "Proof Theory",
	EDITOR = "E. Agazzi",
	BOOKTITLE = "Modern Logic---A Survey: Historical, Philosophical,
		and Mathematical Aspects of Modern Logic and Its Applications",
	SERIES = "Synthese Library",
	VOLUME = 149,
	PAGES = "37--43",
	PUBLISHER = reidel,
	ADDRESS = "Dordrecht",
	YEAR = 1980
}
  
@BOOK{Tak:prot,
	AUTHOR = "Gaisi Takeuti",
	TITLE = "Proof Theory",
	SERIES = slfm,
	VOLUME = 81,
	PUBLISHER = nh,
	ADDRESS = "Amsterdam",
	YEAR = 1975
}

@INCOLLECTION{Sch:protsa,
	AUTHOR = "Helmut Schwichtenberg",
	TITLE = "Proof Theory: Some Applications of Cut-Elimination",
	EDITOR = "J. Barwise",
	BOOKTITLE = "Handbook of Mathematical Logic",
	SERIES = slfm,
	VOLUME = 90,
	CHAPTER = "D.2",
	PAGES = "867--895",
	PUBLISHER = nh,
	ADDRESS = "Amsterdam",
	YEAR = 1977
}

@INCOLLECTION{Sta:hertgn,
	AUTHOR = "Richard Statman",
	TITLE = "{H}erbrand's Theorem and {G}entzen's Notion of Direct Proof",
	EDITOR = "J. Barwise",
	BOOKTITLE = "Handbook of Mathematical Logic",
	SERIES = slfm,
	VOLUME = 90,
	CHAPTER = "D.3",
	PAGES = "897--912",
	PUBLISHER = nh,
	ADDRESS = "Amsterdam",
	YEAR = 1977
}

@INCOLLECTION{Sun:sysd,
	AUTHOR = "G{\"o}ran Sundholm",
	TITLE = "Systems of Deduction",
	EDITOR = "D. Gabbay and F. Guenthner",
	BOOKTITLE = "Handbook of Philosophical Logic, Volume {I}:
		Elements of Classical Logic",
	SERIES = synthl,
	VOLUME = 164,
	CHAPTER = "I.2",
	PAGES = "133--188",
	PUBLISHER = reidel,
	ADDRESS = "Dordrecht",
	YEAR = 1983
}

@BOOK{Kan:prolm,
	AUTHOR = "Stig Kanger",
	TITLE = "Provability in Logic",
	SERIES = "Stockholm Studies in Philosophy",
	VOLUME = 1,
	PUBLISHER = "Almqvist \& Wiksell",
	ADDRESS = "Stockholm",
	YEAR = 1957
}

		  
@BOOK{Pra:natdpt,
	AUTHOR = "Dag Prawitz",
	TITLE = "Natural Deduction: A Proof-Theoretic Study",	
	SERIES = "Stockholm Studies in Philosophy",
	VOLUME = 3,
	PUBLISHER = "Almqvist \& Wiksell",
	ADDRESS = "Stockholm",
	YEAR = 1965
}

@BOOK{TS:baspt,
	AUTHOR = "Anne S. Troelstra and Helmut Schwichtenberg",
	TITLE = "Basic Proof Theory",
	SERIES = cttcs,
	VOLUME = 43,
	PUBLISHER = cup,
	YEAR = 1996
}

@BOOK{Ung:norcet,
	AUTHOR = "Anthony M. Ungar",
	TITLE = "Normalization, Cut-Elimination and the Theory of Proofs",
	SERIES = csli-ln,
	VOLUME = 28,
	PUBLISHER = csli,
	ADDRESS = "Stanford, CA",
	YEAR = 1992
}

@BOOK{Per:estlnd,
	AUTHOR = "Luiz Carlos P. D. Pereira",
	TITLE = "On the Estimation of the Length of Normal Derivations",
	SERIES = "Philosophical Studies",
	VOLUME = 4,
	PUBLISHER = "Akademilitteratur",
	ADDRESS = "Stockholm",
	YEAR = 1982
}

@BOOK{Hal:norpst,
	AUTHOR = "Lars Halln{\"a}s",
	TITLE = "On Normalization of Proofs in Set Theory",
	SERIES = "Dissertationes Mathematicae (Rozprawy Matematyczne)",
	VOLUME = 261,
	PUBLISHER = "Pa{\'n}stwowe Wydawnictwo Naukowe",
	ADDRESS = "Warszawa",
	YEAR = 1988
}


% formalization of consequence

@ARTICLE{Sag:logcr,
	AUTHOR = "Jos{\'e} M. Sag{\"u}illo",
	TITLE = "Logical Consequence Revisited",
	JOURNAL = bsl,
	VOLUME = 3,
	NUMBER = 2,
	PAGES = "216--241",
	YEAR = 1997,
	URL = "ftp://math.ucla.edu/pub/asl/bsl/0302/0302-004.ps"
}

@ARTICLE{Avr:simcr,
	AUTHOR = "Arnon Avron",
	TITLE = "Simple Consequence Relations",
	JOURNAL = iandc,
	VOLUME = 92,
	NUMBER = 1,
	PAGES = "105--139",
	YEAR = 1991
}
		  
@ARTICLE{Avr:axidi,
	AUTHOR = "Arnon Avron",
	TITLE = "Axiomatic Systems, Deduction, and Implication",
	JOURNAL = jlc,
	VOLUME = 2,
	NUMBER = 1,
	PAGES = "51--98",
	YEAR = 1992
}

@ARTICLE{FHV:whair,
	AUTHOR = "Ronald Fagin and Joseph Y. Halpern and Moshe Y. Vardi",
	TITLE = "What is an Inference Rule?",
	JOURNAL = jsl,
	VOLUME = 57,
	NUMBER = 3,
	PAGES = "1018--1045",
	YEAR = 1992
}

@INCOLLECTION{Acz:schc,
	AUTHOR = "Peter Aczel",
	TITLE = "Schematic Consequence",
	EDITOR = "B. Nordstr{\"o}m and K. Pettersson and G. Plotkin",
	BOOKTITLE = "Informal Proc.\ of Wksh.\ on Types for Proofs and 
		Programs, B{\aa}stad, Sweden, 8--12 June 1992",
	PAGES = "11--20",
	ADDRESS = "ftp://ftp.cs.chalmers.se/pub/cs-reports/baastad.92/proc.dvi.Z",	  
	YEAR = 1992
}


% deduction systems

@BOOK{Mas:thedsi,
	AUTHOR = "S. Yu. Maslov",
	TITLE = "Theory of Deductive Systems and Its Applications",
	SERIES = "Cybernetics",
	PUBLISHER = "Radio i svyaz'",
	ADDRESS = "Moscow",
	YEAR = 1986,
	NOTE = "In Russian"
}


@BOOK{Mas:thedsi-transl,
	AUTHOR = "S. Yu. Maslov",
	TITLE = "Theory of Deductive Systems and Its Applications",
	SERIES = "Foundations of Computing",
	PUBLISHER = mit,
	ADDRESS = "Cambridge, MA",
	YEAR = 1987
}

% labelled deduction

@INCOLLECTION{Gab:labdsp,
	AUTHOR = "Dov M. Gabbay",
	TITLE = "Labelled Deductive Systems: A Position Paper",
	EDITOR = "J. Oikkonen and J. V{\"a}{\"a}n{\"a}nen",
	BOOKTITLE = "Proc.\ of Logic Colloquium '90, 
		Helsinki, Finland, 15--22 July 1990",
	SERIES = lnl,
	VOLUME = 2,
	PAGES = "66--88",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1993
}

% *** epsilon-symbol

@ARTICLE{Tai:subm,
	AUTHOR = "W. W. Tait",
	TITLE = "The Substitution Method",
	JOURNAL = jsl,
	VOLUME = 30,
	NUMBER = 2,
	PAGES = "175--192",
	YEAR = 1965
}
		  
@BOOK{Lei:matlhe,
	AUTHOR = "A. C. Leisenring",
	TITLE = "Mathematical Logic and {H}ilbert's $\epsilon$-Symbol",
	PUBLISHER = "Gordon and Breach Science Publishers",
	ADDRESS = "New York",
	YEAR = 1969
}

@ARTICLE{DF:frevvf,
	AUTHOR = "Martin Davis and Ronald Fechter",
	TITLE = "A Free Variable Version of the First-Order Predicate 
		Calculus",
	JOURNAL = jlc,
	VOLUME = 1,
	NUMBER = 4,
	PAGES = "431--451",
	YEAR = 1991
}

@INCOLLECTION{Min:gentsh,
	AUTHOR = "G. E. Mints",
	TITLE = "{G}entzen-Type Systems and {H}ilbert's Epsilon
		Substitution Method {I}",
	EDITOR = "D. Prawitz and B. Skyrms and D. Westerst{\aa}hl",
	BOOKTITLE = "Proc.\ of 9th Int.\ Congress of Logic, Methodology
		and Philosophy of Science, Uppsala, Sweden,
		7--14 Aug 1991",
	SERIES = slfm,
	VOLUME = 134,
	PAGES = "91--122",
	PUBLISHER = nh,
	ADDRESS = "Amsterdam",
	YEAR = 1994
}

@ARTICLE{Min:thoses,
	AUTHOR = "Grigori Mints",
	TITLE = "{T}horalf {S}kolem and the Epsilon Substitution Method
		for Predicate Logic",
	JOURNAL = njpl,
	VOLUME = 1,
	NUMBER = 2,
	SPECIAL = "Thoralf Skolem",
	PAGES = "133--146",
	YEAR = 1996,
	URL = "http://www.hf.uio.no/filosofi/njpl/vol1no2/epsilon/"
}


% *** higher-order logic

@INCOLLECTION{BD:higol,
	AUTHOR = "Johan van Benthem and Kees Doets",
	TITLE = "Higher-Order Logic",
	EDITOR = "D. Gabbay and F. Guenthner",
	BOOKTITLE = "Handbook of Philosophical Logic, Volume {I}:
		Elements of Classical Logic",
	SERIES = synthl,
	VOLUME = 164,
	CHAPTER = "I.4",
	PAGES = "275--329",
	PUBLISHER = reidel,
	ADDRESS = "Dordrecht",
	YEAR = 1983
}

@INCOLLECTION{Lei:higol,
	AUTHOR = "Daniel Leivant",
	TITLE = "Higher Order Logic",
	EDITOR = "D. M. Gabbay and C. J. Hogger and J. A. Robinson",
	BOOKTITLE = "Handbook of Logic in Artificial Intelligence
		and Logic Programming, Volume 2: Deduction Methodologies",
	PAGES = "229--321",
	PUBLISHER = clarendon,
	ADDRESS = "Oxford",
	YEAR = 1994
}

@INCOLLECTION{Haz:prel,
	AUTHOR = "Allen Hazen",
	TITLE = "Predicative Logics",
	EDITOR = "D. Gabbay and F. Guenthner",
	BOOKTITLE = "Handbook of Philosophical Logic, Volume {I}:
		Elements of Classical Logic",
	SERIES = synthl,
	VOLUME = 164,
	CHAPTER = "I.5",
	PAGES = "331--407",
	PUBLISHER = reidel,
	ADDRESS = "Dordrecht",
	YEAR = 1983
}

@ARTICLE{Chu:forstt,
	AUTHOR = "Alonzo Church",
	TITLE = "A Formulation of the Simple Theory of Types",
	JOURNAL = jsl,
	VOLUME = 5,
	NUMBER = 2,
	PAGES = "56--68",
	YEAR = 1940
}

@ARTICLE{Pra:comhso,
	AUTHOR = "Dag Prawitz",
	TITLE = "Completeness and Hauptsatz for Second Order Logic",
	JOURNAL = theoria,
	VOLUME = 33,
	NUMBER = 3,
	PAGES = "246--258",
	YEAR = 1967
}

@ARTICLE{Pra:hauhol,
	AUTHOR = "Dag Prawitz",
	TITLE = "Hauptsatz for Higher Order Logic",
	JOURNAL = jsl,
	VOLUME = 33,
	NUMBER = 3,
	PAGES = "452--457",
	YEAR = 1968
}

@ARTICLE{Hen:comfof,
	AUTHOR = "Leon Henkin",
	TITLE = "The Completeness of First-Order Functional Calculus",
	JOURNAL = jsl,
	VOLUME = 14,
	NUMBER = 3,
	PAGES = "159--166",
	YEAR = 1949
}

@ARTICLE{Hen:comtt,
	AUTHOR = "Leon Henkin",
	TITLE = "Completeness in the Theory of Types",
	JOURNAL = jsl,
	VOLUME = 15,
	NUMBER = 2,
	PAGES = "81--91",
	YEAR = 1950
}

@ARTICLE{Hen:dismcp,
	AUTHOR = "Leon Henkin",
	TITLE = "The Discovery of My Completeness Proofs",
	JOURNAL = bsl,	
	VOLUME = 2,
	NUMBER = 2,
	PAGES = "127--158",
	YEAR = 1996,
	URL = "ftp://math.ucla.edu/pub/asl/bsl/0202/0202-001.ps"
}

@ARTICLE{And:genmdc,
	AUTHOR = "Peter B. Andrews",
	TITLE = "General Models, Descriptions, and Choice in Type Theory",
	JOURNAL = jsl,
	VOLUME = 37,
	NUMBER = 2,
	PAGES = "385--394",
	YEAR = 1972
}

@ARTICLE{And:genme,
	AUTHOR = "Peter B. Andrews",
	TITLE = "General Models and Extensionality",
	JOURNAL = jsl,
	VOLUME = 37,
	NUMBER = 2,
	PAGES = "395--397",
	YEAR = 1972
}

@ARTICLE{Den:pursol,
	AUTHOR = "Nicholas Denyer",
	TITLE = "Pure Second-Order Logic",
	JOURNAL = ndjfl,
	VOLUME = 33,
	NUMBER = 2,
	PAGES = "220--224",
	YEAR = 1992
}

@ARTICLE{AM:extnft,
	AUTHOR = "Toshiyasu Arai and Grigori Mints",
	TITLE = "Extended Normal Form Theorems for Logical Proofs
	      from Axioms",
	JOURNAL = tcs,
	VOLUME = 232,
	NUMBER = "1--2",
	PAGES = "121--132",
	YEAR = 2000
}


% ========================================================================
% ========================================================================


% *** theorem proving		
% *** textbooks, surveys etc


@BOOK{CL:symlmt,
	AUTHOR = "Chin-Liang Chang and Richard Char-tung Lee",
	TITLE = "Symbolic Logic and Mechanical Theorem Proving",
	SERIES = "Computer Science adn Applied Mathematics",
	PUBLISHER = ap,
	ADDRESS = "New York",
	YEAR = 1973
}

@BOOK{Fit:firola,
	AUTHOR = "Melvin C. Fitting",
	TITLE = "First-Order Logic and Automated Theorem Proving",
	EDITION = "2nd",
	SERIES = gtcs,
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1996,
	NOTE = "1st ed., 1990"		  
}	

@BOOK{GLM:protad,
	AUTHOR = "Jean Goubault-Larrecq and Ian Mackie",
	TITLE = "Proof Theory and Automated Deduction",
	SERIES = als,
	VOLUME = 6,
	PUBLISHER = kluwer,
	ADDRESS = "Dordrecht",
	YEAR = 1997
}  
		  
% *** Robinson's resolution

@ARTICLE{Rob:macolb,
	AUTHOR = "J. Alan Robinson",
	TITLE = "A Machine-Oriented Logic Based on the Resolution Principle",
	JOURNAL = jacm,
	YEAR = 1965,
	VOLUME = 12,
	NUMBER = 1,
	PAGES = "23--41"	
}

% *** Maslov's inverse method

@ARTICLE{Mas:invmed,
	AUTHOR = "S. Yu. Maslov",
	TITLE = "An Inverse Method of Establishing Deducibility in 
		Classical Predicate Calculus",
	JOURNAL = dan,
	VOLUME = 159,
	NUMBER = 1,
	PAGES = "17--20",
	YEAR = 1964,
	NOTE = "In Russian"	
}

@ARTICLE{Mas:invmed-transl,
	AUTHOR = "S. Yu. Maslov",
	TITLE = "An Inverse Method of Establishing Deducibility in 
		Classical Predicate Calculus",
	JOURNAL = smd,
	VOLUME = 5,
	NUMBER = ???,
	PAGES = "1420--1423",
	YEAR = 1964	
}

@ARTICLE{Zam:resms,
	AUTHOR = "N. K. Zamov",
	TITLE = "The Resolution Method without Skolemization",
	JOURNAL = dan,
	VOLUME = 293,
	NUMBER = 5,
	PAGES = ???,
	YEAR = 1987,
	NOTE = "In Russian"	
}

@ARTICLE{Zam:resms-transl,
	AUTHOR = "N. K. Zamov",
	TITLE = "The Resolution Method without Skolemization",
	JOURNAL = smd,
	VOLUME = 35,
	NUMBER = 2,
	PAGES = "399--401",
	YEAR = 1987	
}

@ARTICLE{Lif:whaim,
	AUTHOR = "Vladimir Lifshitz",
	TITLE = "What is the Inverse Method?",
	JOURNAL = jar,
	YEAR = 1989,
	VOLUME = 5,
	NUMBER = 1,
	PAGES = "1--23"		
}

% *** resolution a la Mints

@INCOLLECTION{Min:gentsr1,
	AUTHOR = "Grigori Mints",
	TITLE = "{G}entzen-type Systems and Resolution Rule, 
		Part {I}: Propositional Logic",
	EDITOR = "P. Martin-L{\"o}f and G. Mints",
	BOOKTITLE = "Proc.\ of Int.\ Conf.\ on Computer Logic, COLOG'88,
		Tallinn, USSR, 12--16 Dec 1988",
	SERIES = lncs,
	VOLUME = 417,
	PAGES = "198--231",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1990
}

@INCOLLECTION{Min:gentsr2,
	AUTHOR = "Grigori Mints",
	TITLE = "{G}entzen-type Systems and Resolution Rule, 
		Part {II}: Predicate Logic",
	EDITOR = "J. Oikkonen and J. V{\"a}{\"a}n{\"a}nen",
	BOOKTITLE = "Proc.\ of ASL Summer Meeting, 
		Logic Colloquium '90, Helsinki, Finland, 15--22 July 1990",
	SERIES = lnl,
	VOLUME = 2,
	PAGES = "163--190",	
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1993
}

@INCOLLECTION{Tam:resims,
	AUTHOR = "Tanel Tammet",
	TITLE = "Resolution, Inverse Method and the Sequent Calculus",
	EDITOR = "G. Gottlob and A. Leitsch and D. Mundici",
	BOOKTITLE = "Computational Logic and Proof Theory: 
		Proc.\ of 5th Kurt G{\"o}del Colloquium, KGC'97,
		Vienna, Austria, 25--29 Aug 1997",
	SERIES = lncs,
	VOLUME = 1289,
	PAGES = "65--83",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1997,
	URL = "http://www.cs.chalmers.se/~tammet/kgcinv.ps"
}		  


% Staalmarck's method

@TECHREPORT{Sta:assmpp,
	AUTHOR = "Gunnar St{\aa}lmarck",
	TITLE = "The {A}ssure Method: A Proof Procedure for Propositional
		Logic",
	NUMBER = 1,
	INSTITUTION = "Logikkonsult NP AB",
	ADDRESS = "Stockholm",
	YEAR = 1990		
}

@TECHREPORT{Wid:svatam,
	AUTHOR = "Filip Wideb{\"a}ck",
	TITLE = "Sv{\aa}ra tautologier f{\"o}r {ASSURE}-metoden",
	TYPE = "Graduation thesis [ME thesis]",
	NUMBER = "TRITA-NA E 91:60",
	INSTITUTION = "Dept.\ of Numerical Analysis and Computing Science,
		Royal Inst.\ of Techn., Stockholm",
	YEAR = 1991
}

@INCOLLECTION{SS:modvss,
	AUTHOR = "Gunnar St{\aa}lmarck and M{\aa}rten S{\"a}flund",
	TITLE = "Modelling and Verifying Systems and Software in 
	        Propositional Logic",
	EDITOR = "B. K. Daniels",
	BOOKTITLE = "Proc.\ of IFAC/EWICS/SARS Symp.\ on Safety of
		Computer Control Systems 1990, SAFECOMP'90, Gatwick, UK,
		30 Oct -- 2 Nov 1990: Safety, Security and Reliability
		Related Computers for the 1990s",
	SERIES = "IFAC Symposia Series",
	VOLUME = "1990:17",
	PAGES = "31--36",
	PUBLISHER = pp,
	ADDRESS = "Oxford",
	YEAR = 1990
}

@INCOLLECTION{SA:forvhs,
	AUTHOR = "Gunnar St{\aa}lmarck and Ove {\AA}kerlund",
	TITLE = "Formal Verification of Hardware and Software Systems
	        Using {NP}-{C}ircuit",
	EDITOR = "Yngve Malm{\'e}n and Veikko Rouhiainen",
	BOOKTITLE = "Reliability and Safety of Processes and Manufacturing
		Systems: Proc.\ of 12th Annual Symp.\ of the Society of
		Reliability Engineers, Scand.\ Chapter, Tampere, Finland,
		1--3 Oct 1991",
	PAGES = "65--76",
	PUBLISHER = eas,
	ADDRESS = "London",
	YEAR = 1991
}

@UNPUBLISHED{Sta:protct,	
	AUTHOR = "Gunnar St{\aa}lmarck",
	TITLE = "A Proof-Theoretic Concept of Tautological Hardness",
	MONTH = may,
	YEAR = 1994,
	NOTE = "Incomplete draft manuscript"
}

@TECHREPORT{Wid:stanns,
	AUTHOR = "Filip Wideb{\"a}ck",
	TITLE = "{S}t{\aa}lmarck's Notion of {$n$}-Saturation",
	NUMBER = "NP-K-FW-200",
	INSTITUTION = "Logikkonsult NP AB",
	ADDRESS = "Stockholm",
	MONTH = jan,
	YEAR = 1996
}

@INCOLLECTION{Bor:indsvt,
	AUTHOR = "Arne Bor{\"a}lv",
	TITLE = "The Industrial Success of Verification Tools Based on
	        {S}t{\aa}lmarck's Method",
	EDITOR = "O. Grumberg",
	BOOKTITLE = "Proc.\ of 9th Int.\ Conf.\ on Computer-Aided
	        Verification, CAV'97, Haifa, Israel, 22--25 June 1997",
	SERIES = lncs,
	VOLUME = 1254,
	PAGES = "7--10",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1997
}

@INCOLLECTION{SB:howppr,
	AUTHOR = "Mary Sheeran and Arne Bor{\"a}lv",
	TITLE = "How to Prove Properties of Recursively Defined 
		Circuits Using {S}t{\aa}lmarck's Method",
	EDITOR = "Mary Sheeran and Bernhard M{\"o}ller",
	BOOKTITLE = "Informal Proc.\ of Wksh.\ on Formal Techniques 
		for Hardware and Hardware-Like Systems, FTH'98,
		Marstrand, Sweden, 19 June 1998",
	PUBLISHER = "Dept.\ of Computing Science, Chalmers Univ.\ of 
		Technology and Univ.\ of G{\"o}teborg",
	YEAR = 1998
}

@INCOLLECTION{SS:tutspp,
	AUTHOR = "Mary Sheeran and Gunnar St{\aa}lmarck",
	TITLE = "A Tutorial on {S}t{\aa}lmarck's Proof Procedure for 
	        Propositional Logic",
	EDITOR = "G. Gopalakrishnan and P. Windley",
	BOOKTITLE = "Proc.\ of 2nd Int.\ Conf.\ on Formal Methods in
		Computer-Aided Design, FMCAD'98, Palo Alto, CA, USA,
		4--6 Nov 1998",
	SERIES = lncs,
	VOLUME = 1522,
	PAGES = "82--99",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1998
}

@INCOLLECTION{BS:forvr,
	AUTHOR = "Arne Bor{\"a}lv and Gunnar St{\aa}lmarck",
	TITLE = "Formal Verification in Railways",
	EDITOR = "Michael G. Hinchey and Jonathan P. Bowen",
	BOOKTITLE = "Industrial-Strength Formal Methods in Practice",
	SERIES = facit,
	PAGES = "329--350",
	PUBLISHER = springer,
	ADDRESS = "London",
	YEAR = 1999,
	URL = "http://www.ifad.dk/Projects/FMERail/arne.ps.gz"
}

@INCOLLECTION{Har:staahd,
	AUTHOR = "John Harrison",
	TITLE = "{S}t{\aa}lmarck's Algorithm as a {HOL} Derived Rule",
	EDITOR = "J. von Wright and J. Grundy and J. Harrison",
	BOOKTITLE = "Proc.\ of 9th Int.\ Conf.\ on Theorem Proving 
		in Higher-Order Logics, TPHOLs'96, Turku, Finland,
		26--30 Aug 1996",
	SERIES = lncs,
	VOLUME = 1125,
	PAGES = "221--234",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1996,
	URL = "http://www.cl.cam.ac.uk/users/jrh/papers/stalmarck_times.ps.gz"
}


% ========================================================================
% ========================================================================


% *** decision and model building
 
@BOOK{BBG:clad,
	AUTHOR = "Egon B{\"o}rger and Erich Gr{\"a}del and Yuri Gurevich",
	TITLE = "The Classical Decision Problem",
	SERIES = pml,
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1997
}

@ARTICLE{GKV:decptv,
	AUTHOR = "Erich Gr{\"a}del and Phokion G. Kolaitis 
		and Moshe Y. Vardi",
	TITLE = "On the Decision Problem for Two-Variable First-Order Logic",
	JOURNAL = bsl,
	VOLUME = 3,
	NUMBER = 1,
	PAGES = "53--69",
	YEAR = 1997
}

@ARTICLE{Zam:masimd,	
	AUTHOR = "N. K. Zamov",
	TITLE = "{M}aslov's Inverse Method and Decidable Classes",
	JOURNAL = apal,
	VOLUME = 42,
	NUMBER = 2,
	PAGES = "165--194",
	YEAR = 1989
}

@PHDTHESIS{Tam:resmdp,
	AUTHOR = "Tanel Tammet",
	TITLE = "Resolution Methods for Decision Problems and Finite-Model
	        Building",
	SCHOOL = "Dept.\ of Computer Sciences, Chalmers Univ.\ of Techn.\
	        and Univ.\ of G{\"o}teborg",
	YEAR = 1992
}

@BOOK{FLTZ:resmdp,
	AUTHOR = "Christian Ferm{\"u}ller and Alexander Leitch and
		Tanel Tammet and Nikolai Zamov",
	TITLE = "Resolution Methods for the Decision Problem",
	SERIES = lnai,
	VOLUME = 679,
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1993
}

@BOOK{Lei:resc,
	AUTHOR = "Alexander Leitch",
	TITLE = "The Resolution Calculus",
	SERIES = ttcs-eatcs,
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1997
}

@INCOLLECTION{Rab:dect,
	AUTHOR = "Michael O. Rabin",
	TITLE = "Decidable Theories",
	EDITOR = "J. Barwise",
	CHAPTER = "C.3",
	BOOKTITLE = "Handbook of Mathematical Logic",
	SERIES = slfm,
	VOLUME = 90,
	PAGES = "595--629",
	PUBLISHER = nh,
	ADDRESS = "Amsterdam",
	YEAR = 1977
}


% *** complexity of proofs

@INCOLLECTION{Tse:comdpc,
	AUTHOR = "G. S. Tseytin",
	TITLE = "On the Complexity of Derivation in Propositional Calculus",
	BOOKTITLE = "Studies in Constructive Mathematics and Mathematical
		Logic {II}",
	SERIES = "Zapiski Nauchnykh Seminarov LOMI",
	VOLUME = 8,
	PAGES = "235--259",
	PUBLISHER = "Nauka",
	ADDRESS = "Leningrad",
	YEAR = 1968,
	NOTE = "In Russian"
}

INCOLLECTION{Tse:comdpc-transl,
	AUTHOR = "G. S. Tseytin",
	TITLE = "On the Complexity of Derivation in Propositional Calculus",
	EDITOR = "A. O. Slisenko",
	BOOKTITLE = "Studies in Constructive Mathematics and Mathematical
		Logic {II}",
	SERIES = "Seminars in Mathematics: Steklov Mathem.\ Inst.",
	VOLUME = 8,
	PAGES = "115--125",
	PUBLISHER = "Consultants Bureau",
	ADDRESS = "New York",
	YEAR = 1970,
}

@ARTICLE{CR:relepp,
	AUTHOR = "Stephen A. Cook and Robert A. Reckhow",
	TITLE = "The Relative Efficiency of Propositional Proof Systems",
	JOURNAL = jsl,
	VOLUME = 44,
	NUMBER = 1,
	PAGES = "36--50",
	YEAR = 1979
}

@INCOLLECTION{BB:dedrnp,
	AUTHOR = "Maria Luisa Bonet and Samuel R. Buss",
	TITLE = "On the Deduction Rule and the Number of Proof Lines",
	BOOKTITLE = "Proc.\ of 6th Annual IEEE Symp.\ on Logic in Computer
		Science, LICS'91, Amsterdam, The Netherlands, 
		15--18 July 1991",
	PAGES = "286--297",
	PUBLISHER = ieee,
	ADDRESS = "Los Alamitos, CA",
	YEAR = 1991
}

@ARTICLE{Urq:harer,
	AUTHOR = "Alasdair Urquhart",
	TITLE = "Hard Examples of Resolution",
	JOURNAL = jacm,
	VOLUME = 34,
	NUMBER = 1,
	PAGES = "209--219",
	YEAR = 1987
}

@INCOLLECTION{Urq:compcp,
	AUTHOR = "Alasdair Urquhart",
	TITLE = "Complexity of Proofs in Classical Propositional Logic",
	EDITOR = "Y. N. Moschovakis",
	BOOKTITLE = "Proc.\ of Wksh.\ Logic from Computer Science,
		Berkeley, CA, USA, 13--17 Nov 1989",
	SERIES = "Mathematical Sciences Research Institute Publications",
	VOLUME = 21,
	PAGES = "597--608",
	PUBLISHER = springer,
	ADDRESS = "New York",
	YEAR = 1991
}

@ARTICLE{Urq:compp,
	AUTHOR = "Alasdair Urquhart",
	TITLE = "The Complexity of Propositional Proofs",
	JOURNAL = bsl,
	VOLUME = 1,
	NUMBER = 4,
	PAGES = "425--467",
	YEAR = 1995,
	URL = "ftp://math.ucla.edu/pub/asl/bsl/0104/0104-003.ps"
}

@ARTICLE{BP:propcp,
	AUTHOR = "Paul Beame and Toniann Pitassi",
	TITLE = "Propositional Proof Complexity: Past, Present, and Future",
	JOURNAL = beatcs,
	VOLUME = 65,
	PAGES = "66--89",
	YEAR = 1998
}

@INCOLLECTION{Pud:lenp,
	AUTHOR = "Pavel Pudl{\'a}k",
	TITLE = "The Lengths of Proofs",
	EDITOR = "S. R. Buss",
	BOOKTITLE = "Handbook of Proof Theory",
	SERIES = slfm,
	VOLUME = 137,
	CHAPTER = 8,
	PAGES = "547--637",
	PUBLISHER = nh,
	ADDRESS = "Amsterdam",
	YEAR = 1998
}

@ARTICLE{Sta:shorps,
	AUTHOR = "Gunnar St{\aa}lmarck",
	TITLE = "Short Resolution Proofs for a Sequence of Tricky Formulas",
	JOURNAL = actai,
	VOLUME = 33,
	NUMBER = 3,
	PAGES = "277--280",
	YEAR = 1996
}

@ARTICLE{Egl:ansopu,
	AUTHOR = "Uwe Egly",
	TITLE = "An Answer to an Open Problem of {U}rquhart",
	JOURNAL = tcs,	
	VOLUME = 198,
	NUMBER = "1--2",
	PAGES = "201--209",
	YEAR = 1998
}

@PHDTHESIS{dA:invcsp,	
	AUTHOR = "Marcello d'Agostino",
	TITLE = "Investigations into the Complexity of Some
		Propositional Calculi",
	TYPE = "{PhD} thesis 
                ({Programming Research Group Technical Monograph PRG-88})",
	SCHOOL = "Oxford Univ.\ Computing Lab.",
	MONTH  = nov,
	YEAR = 1990,
	URL = "http://www.unife.it/dgm/investigations.ps.gz"
}

@ARTICLE{dA:tabitt,
	AUTHOR = "Marcello d'Agostino",
	TITLE = "Are Tableaux an Improvement on Truth-Tables? 
		Cut-Free Proofs and Bivalence",
	JOURNAL = jlli,
	VOLUME = 1,
	NUMBER = ???,
	PAGES = "235--252",
	YEAR = 1992,
	URL = "http://www.unife.it/dgm/truthtab.ps.gz"
}

@ARTICLE{dAM:tamccr,
	AUTHOR = "Marcello d'Agostino and Marco Mondadori",
	TITLE = "The Taming of Cut: Classical Refutations with 
		Analytic Cut",
	JOURNAL = jlc,
	VOLUME = 4,
	NUMBER = ???,
	PAGES = "285--319",
	YEAR = 1994,
	URL = "http://www.unife.it/dgm/taming.ps.gz"
}

@ARTICLE{PC:thepmb,
	AUTHOR = "Jeremy Pitt and Jim Cunningham",
	TITLE = "Theorem Proving and Model Building with the
		Calculus {KE}",
	JOURNAL = jigpl,
	VOLUME = 4,
	NUMBER = 1,
	PAGES = "129--150",
	YEAR = 1996
}


% ========================================================================
% ========================================================================


% *** classical logic as constructive
% *** constructive interpretations of classical logic

@ARTICLE{Sel:norem1,
	AUTHOR = "Jonathan P. Seldin",
	TITLE = "Normalization and Excluded Middle {I}",
	JOURNAL = sl,
	VOLUME = 48,
	NUMBER = 2,
	PAGES = "193--217",
	YEAR = 1989
}

@ARTICLE{Sta:nortff,
	AUTHOR = "Gunnar St{\aa}lmarck",
	TITLE = "Normalization Theorems for Full First Order Classical
		Natural Deduction",
	JOURNAL = jsl,
	VOLUME = 56,
	NUMBER = 1,
	PAGES = "129--149",
	YEAR = 1991
}

@INCOLLECTION{Urb:strngl,
	AUTHOR = "Christian Urban",
	TITLE = "Strong Normalisation for a Gentzen-like Cut-Elimination
	      Procedure",
	EDITOR = "S. Abramsky",
	BOOKTITLE = "Proc.\ of 5th Int.\ Conf.\ on Typed Lambda Calculi
		  and Applications, TLCA'01, Krakow, Poland, 2--5 May 2001",
	SERIES = lncs,
	VOLUME = 2044,
	PAGES = "415--429",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 2001
} 		         
 
@INCOLLECTION{Lai:decncc,
	AUTHOR = "J. Laird",
	TITLE = "A Deconstruction of Non-deterministic Classical
	      Cut Elimination",
	EDITOR = "S. Abramsky",
	BOOKTITLE = "Proc.\ of 5th Int.\ Conf.\ on Typed Lambda Calculi
		  and Applications, TLCA'01, Krakow, Poland, 2--5 May 2001",
	SERIES = lncs,
	VOLUME = 2044,
	PAGES = "268--282",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 2001
} 	

@INCOLLECTION{Gri:fortnc,
	AUTHOR = "Timothy G. Griffin",
	TITLE = "The Formulae-as-Types Notion of Control",
	BOOKTITLE = "Conf.\ Record 17th Annual ACM Symp.\ on Principles
		of Programming Languages, POPL'90, San Francisco, CA, USA,
		17--19 Jan 1990",
	PAGES = "47--57",
	PUBLISHER = acm,
	ADDRESS = "New York",
	YEAR = 1990
}
		  
@INCOLLECTION{CM:finccc,
	AUTHOR = "Robert Constable and Chet Murthy",
	TITLE = "Finding Computational Content in Classical Proofs",
	EDITOR = "G. Huet and G. Plotkin",
	BOOKTITLE = "Logical Frameworks",
	PAGES = "341--362", 
	PUBLISHER = cup,
	YEAR = 1991
}

@PHDTHESIS{Mur:extccc,
	AUTHOR = "Chetan R. Murthy",
	TITLE = "Extracting Constructive Content from Classical Proofs",
	TYPE = "{PhD} thesis ({T}echnical report {TR 90-1151}",
	SCHOOL = "Dept.\ of Computer Science, Cornell Univ., Ithaca, NY",
	MONTH = aug,
	YEAR = 1990
}

@TECHREPORT{Mur:evascp-r,
	AUTHOR = "Chetan R. Murthy",
	TITLE = "An Evaluation Semantics for Classical Proofs",
	NUMBER = "TR 91-1213",
	INSTITUTION = "Dept.\ of Computer Science, Cornell Univ., Ithaca, NY",
	MONTH = jun,
	YEAR = 1991
}

@INCOLLECTION{Mur:evascp,
	AUTHOR = "Chetan R. Murthy",
	TITLE = "An Evaluation Semantics for Classical Proofs",
	BOOKTITLE = "Proc.\ of 6th Annual IEEE Symp.\ on Logic in 
		Computer Science, LICS'91, Amsterdam, The Netherlands, 
		15--18 July 1991",
	PAGES = "96--107",
	PUBLISHER = ieee,
	ADDRESS = "Los Alamitos, CA",
	YEAR = 1991
}

@TECHREPORT{Mur:clapph-r,
	AUTHOR = "Chetan R. Murthy",
	TITLE = "Classical Proofs as Programs: How, What, When, and Why",
	NUMBER = "TR 91-1215",
	INSTITUTION = "Dept.\ of Computer Science, Cornell Univ., Ithaca, NY",
	MONTH = jul,
	YEAR = 1991
}

@INCOLLECTION{Mur:clapph,
	AUTHOR = "Chetan R. Murthy",
	TITLE = "Classical Proofs as Programs: How, What, When, and Why",
	EDITOR = "J. P. Myers and M. K. O'Donnell",
	BOOKTITLE = "Proc.\ of Summer Symp.\ on Constructivity in Computer
		Science, San Antonio, TX, USA, 19--22 June 1991",
	SERIES = lncs,
	VOLUME = 613,
	PAGES = "71--88",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1992,
	URL = "ftp://ftp.cs.cornell.edu/pub/murthy/cincs91.dvi.Z"
}

@INCOLLECTION{Mur:comagt,
	AUTHOR = "Chetan R. Murthy",
	TITLE = "A Computational Analysis of {G}irard's Translation and {LC}",
	BOOKTITLE = "Proc.\ of 7th Annual IEEE Symp.\ on Logic in 
		Computer Science, LICS'92, Santa Cruz,
		CA, USA, 22--25 June 1992",
	PAGES = "90--101",	
	PUBLISHER = ieee,
	ADDRESS = "Los Alamitos, CA",
	YEAR = 1992,
	URL = "ftp://ftp.cs.cornell.edu/pub/murthy/lics92.dvi.Z"	
}

@PHDTHESIS{Nap:coml,
	AUTHOR = "Maria H. Napierala",
	TITLE = "Computational Logic",
	TYPE = "{PhD} thesis {CS/E 92-TH-008}",
        SCHOOL = "Dept.\ of Computer Sci.\ and Eng., 
                Oregon Grad.\ Inst.\ of Sci.\ and Techn., Portland, OR",
	MONTH = jul,
	YEAR = 1992,
	URL = "ftp://cse.ogi.edu/pub/tech_reports/1992/92-TH-008.ps.gz"
}

@INCOLLECTION{Par:fredac,
	AUTHOR = "Michel Parigot",
	TITLE = "Free deduction: An Analysis of ``Computations'' in Classical
		Logic",
	EDITOR = "A. Voronkov",
	BOOKTITLE = "Proc.\ of 1st Russian Conf.\ on Logic Programming,
		Irkutsk, 14--18 Sept.\ 1990, and 2nd Russian Conf.\ on Logic
		Programming, St.~Petersburg, 11--16 Sept.\ 1991",
	SERIES = lnai,
	VOLUME = 592,
	PAGES = ???,
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1992
}

@INCOLLECTION{Par:lammca,
	AUTHOR = "Michel Parigot",
	TITLE = "{$\lambda\mu$}-Calculus: An Algorithmic Interpretation of
		Classical Natural Deduction",
	EDITOR = "A. Voronkov",
	BOOKTITLE = "Proc.\ of Int.\ Conf.\ on Logic Programming
		and Automated Reasoning, LPAR'92, St Petersburg, Russia,
		15--20 July 1992",
	SERIES = lnai,
	VOLUME = 624,
	PAGES = "190--201",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1992,
	URL = "ftp://frege.logique.jussieu.fr/pub/distrib/parigot/lpar92+.dvi"
}

@INCOLLECTION{Par:strnso,
	AUTHOR = "Michel Parigot",
	TITLE = "Strong Normalization for Second Order Classical 
		Natural Deduction",
	BOOKTITLE = "Proc.\ of 8th Annual IEEE Symp.\ on Logic in Computer 
		Science, LICS'93, Montreal, Canada, 19--23 June 1993", 
	PAGES = "39--46",
	PUBLISHER = ieee,
	ADDRESS = "Los Alamitos, CA",
	YEAR = 1993,
	URL = "ftp://frege.logique.jussieu.fr/pub/distrib/parigot/lics93.dvi"
}	

@ARTICLE{Par:prosns,
	AUTHOR = "Michel Parigot",
	TITLE = "Proofs of Strong Normalisation for Second Order
	      Classical Natural Deduction",
	JOURNAL = jsl,
	VOLUME = 62,
	NUMBER = 4,
	PAGES = "1461--1479",
	YEAR = 1997
}

@INCOLLECTION{Par:clapp,
	AUTHOR = "Michel Parigot",
	TITLE = "Classical Proofs as Programs",
	EDITOR = "G. Gottlob and A. Leitsch and D. Mundici",
	BOOKTITLE = "Computational Logic and Proof Theory: Proc.\ of 
		3rd Kurt G{\"o}del Colloquium, KGC'93, Brno, Czech Republic, 
		24--27 Aug.\ 1993",
	SERIES = lncs,
	VOLUME = 713,
	PAGES = "263--276",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1993,
	URL = "ftp://frege.logique.jussieu.fr/pub/distrib/parigot/kgc93+.dvi"
}

@ARTICLE{Kri:clalso,
	AUTHOR = "Jean-Louis Krivine",
	TITLE = "Classical Logic, Storage Operators and Second-Order
		Lambda-Calculus",
	JOURNAL = apal,
	VOLUME = 68,
	NUMBER = 1,
	PAGES = "53--78",
	YEAR = 1994
}

@ARTICLE{Kri:gensti,
	AUTHOR = "Jean-Louis Krivine",
	TITLE = "A General Storage Theorem for Integers",
	JOURNAL = tcs,
	VOLUME = 129,
	NUMBER = 1,
	PAGES = "79--94",
	YEAR = 1994
}

@TECHREPORT{Bie:comilm-r,
	AUTHOR = "G. M. Bierman",
	TITLE = "A Computational Interpretation of the 
	      {$\lambda\mu$}-Calculus",
	NUMBER = 448,
	INSTITUTION = "Univ.\ of Cambridge Computer Laboratory",
	MONTH = sep,
	YEAR = 1998,
	URL = "http://www.cl.cam.ac.uk/~gmb/Papers/tr448.ps"
}

@INCOLLECTION{Bie:comilm,
	AUTHOR = "G. M. Bierman",
	TITLE = "A Computational Interpretation of the 
	      {$\lambda\mu$}-Calculus",
	EDITOR = "L. Brim and J. Gruska and J. Zlatuska",
	BOOKTITLE = "Proc.\ of 23rd Int.\ Symp.\ on Math.\ Found.\ of Comp.\
		  Science, MFCS'98, Brno, Czech Rep., 24--28 Aug.\ 1998",
	SERIES = lncs,
	VOLUME = 1450,
	PAGES = "336--345",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1998,
	URL = "http://www.cl.cam.ac.uk/~gmb/Papers/mfcs98.ps"
}

@INCOLLECTION{dG:cpslmc,
	AUTHOR = "Philippe de Groote",
	TITLE = "A {CPS}-Translation of the {$\lambda\mu$}-Calculus",
	EDITOR = "S. Tison",
	BOOKTITLE = "Proc.\ of 19th Int.\ Coll.\ on Trees in Algebra and
		Programming, CAAP'94, Edinburgh, UK, 11--13 Apr.\ 1994",
	SERIES = lncs,
	VOLUME = 787,
	PAGES = "85--99",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1994
}

@INCOLLECTION{dG:rellmc,
	AUTHOR = "Philippe de Groote",
	TITLE = "On the Relation between the {$\lambda\mu$}-Calculus and 
		the Syntactic Theory of Sequential Control",
	EDITOR = "F. Pfenning",
	BOOKTITLE = "Proc.\ of 5th Int.\ Conf.\ on Logic Programming and
		Automated Reasoning, LPAR'94, Kiev, Ukraine, 16--22 July 1994",
	SERIES = lnai,
	VOLUME = 822,
	PAGES = "31--43",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1994
}

@INCOLLECTION{dG:simceh,
	AUTHOR = "Philippe {de Groote}",
	TITLE = "A Simple Calculus of Exception Handling",
	EDITOR = "M. Dezani-Ciancaglini and G. Plotkin",
	BOOKTITLE = "Proc.\ of 2nd Int.\ Conf.\ on Typed Lambda Calculi
		and Applications, TLCA'95, Edinburgh, UK, 10--12 Apr.\ 1995",
	SERIES = lncs,
	VOLUME = 902,
	PAGES = "201--215",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1995
}

@INCOLLECTION{dG:strncn,
	AUTHOR = "Philippe de Groote",
	TITLE = "Strong Normalization of Classical Natural Deduction
	       with Disjunction",
	EDITOR = "S. Abramsky",
	BOOKTITLE = "Proc.\ of 5th Int.\ Conf.\ on Typed Lambda Calculi
		  and Applications, TLCA'01, Krakow, Poland, 2--5 May 2001",
	SERIES = lncs,
	VOLUME = 2044,
	PAGES = "182--196",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 2001
} 	

@INCOLLECTION{Mat:parsol,
	AUTHOR = "Ralph Matthes",
	TITLE = "{P}arigot's Second Order {$\lambda\mu$}-Calculus and 
	      Inductive Types",
	EDITOR = "S. Abramsky",
	BOOKTITLE = "Proc.\ of 5th Int.\ Conf.\ on Typed Lambda
		  Calculi and Appl., TLCA'01, Krakow, Poland,
		  2--5 May 2001",
	SERIES = lncs,
	VOLUME = 2044,
	PAGES = "329--343",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 2001,
	URL = "ftp://ftp.tcs.informatik.uni-muenchen.de/pub/matthes/publ/tlca01.ps" 
} 	

@INCOLLECTION{Abe:thiorl,
	AUTHOR = "Andreas Abel",
	TITLE = "A Third-Order Representation of the {$\lambda\mu$}-Calculus",
	EDITOR = "Simon J. Ambler and Roy L. Crole and Alberto Momigliano",
	BOOKTITLE = "Proc.\ of Wksh.\ on Mechanised Reasoning about 
		  Languages with Variable Binding, MERLIN 2001, Siena,
		  Italy, 18 June 2001",
	SERIES = entcs,
	VOLUME = "58(1)",
	PUBLISHER = elsevier,
	ADDRESS = "Amsterdam",
	YEAR = 2001
}         
 
@INCOLLECTION{Ong:semvcp,
	AUTHOR = "C.-H. Luke Ong",
	TITLE = "A Semantic View of Classical Proofs: Type-Theoretic, 
		Categorical, and Denotational Characterizations
		(Preliminary Extended Abstract)",
	BOOKTITLE = "Proc.\ of 11th Annual IEEE Symp.\ on Logic in 
		Computer Science, LICS'96, New Brunswick, NJ, USA,
		27--30 July 1996",
	PAGES = "230--241",
	PUBLISHER = ieee,
	ADDRESS = "Los Alamitos, CA",
	YEAR = 1996,
	URL = "ftp://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Luke.Ong/classical.ps.gz"
}

@INCOLLECTION{OS:curhff,
	AUTHOR = "C.-H. Luke Ong and Charles A. Stewart",
	TITLE = "A {C}urry-{H}oward Foundation for Functional Computation
		with Control",
	BOOKTITLE = "Conf.\ Record 24th ACM SIGPLAN-SIGACT Symp.\ on 
		Principles of Programming Languages, POPL'97, Paris, France, 
		15--17 Jan.\ 1997",
	PAGES = "215--227",
	PUBLISHER = acm,
	ADDRESS = "New York",
	YEAR = 1997,
	URL = "ftp://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Luke.Ong/popl97.ps.gz"
}

@PHDTHESIS{Ste:fortcc,
	AUTHOR = "Charles A. Stewart",
	TITLE = "On the Formulae-as-Types Correspondence for 
	      Classical Logic",
	SCHOOL = "Oxford Univ.\ Computing Lab.\ Programming Research Group",
	YEAR = 1999,
	URL = "http://www.linearity.org/cas/thesis/thesis-A4.ps"
}

@ARTICLE{SR:clalcs,
	AUTHOR = "Thomas Streicher and Bernhard Reus",
	TITLE = "Classical Logic, Continuation Semantics and
	      Abstract Machines",
	JOURNAL = jfp, 
	VOLUME = 8,
	NUMBER = 6,
	PAGES = "543--572",
	YEAR = 1998
} 

@TECHREPORT{RS:lamdc-r,
	AUTHOR = "Niels Jakob Rehof and Morten Heine S{\o}rensen",
	TITLE = "The {$\lambda_\Delta$}-calculus",
	TYPE = "TOPPS Prepublication",
	NUMBER = "D-175",
	INSTITUTION = "DIKU, Copenhagen",
	MONTH = oct,
	YEAR = 1993,
	URL = "ftp://ftp.diku.dk/diku/semantics/papers/D-175.ps"
}

@INCOLLECTION{RS:lamdc-c,
	AUTHOR = "Niels Jakob Rehof and Morten Heine S{\o}rensen",
	TITLE = "The {$\lambda_\Delta$}-calculus",
	EDITOR = "K. M. Hagiya and J. C. Mitchell",
	BOOKTITLE = "Proc.\ of 2nd Int.\ Symp.\ on Theoretical Aspects of
		Computer Software, TACS'94, Sendai, Japan, 19--22 Apr.\ 1994",
	SERIES = lncs,
	VOLUME = 789,
	PAGES = "516--542",	
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1994,
	URL = "ftp://ftp.diku.dk/diku/semantics/papers/D-189.ps"
}

@INCOLLECTION{Nak:confct,
	AUTHOR = "Hiroshi Nakano",
	TITLE = "A Constructive Formalization of the Catch/Throw Mechanism",
	BOOKTITLE = "Proc.\ of 7th Annual IEEE Symp.\ on Logic in Computer
		Science, LICS'92, Santa Cruz, CA, USA, 22--25 June 1992",
	PAGES = "82--89",
	PUBLISHER = ieee,
	ADDRESS = "Los Alamitos, CA",
	YEAR = 1992,
	URL = "http://www602.math.ryukoku.ac.jp/~nakano/papers/ct-lics92.ps.gz"
}

@ARTICLE{Nak:conlct,
	AUTHOR = "Hiroshi Nakano",
	TITLE = "A Constructive Logic behind the Catch/Throw Mechanism",
	JOURNAL = apal,
	SPECIAL = ???,
	VOLUME = 69,
	NUMBER = "2--3", 
	PAGES = "269--301",
	YEAR = 1994
}

@INCOLLECTION{Nak:nondct,
	AUTHOR = "Hiroshi Nakano",
	TITLE = "The Non-deterministic Catch and Throw Mechanism and
		Its Subject Reduction Property",
	EDITOR = "N. D. Jones and M. Hagiya and M. Sato",
	BOOKTITLE = "Logic, Language, and Computation: Festschrift in Honor
		of Satoru Takasu",
	SERIES = lncs,
	VOLUME = 792,
	PAGES = "61--72",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1994,
	URL = "http://www602.math.ryukoku.ac.jp/~nakano/papers/ct-takasu94.ps.gz"
}

@PHDTHESIS{Nak:logsct,
	AUTHOR = "Hiroshi Nakano",
	TITLE = "Logical Structures of the Catch and Throw Mechanism",
	SCHOOL = "Univ.\ of Tokyo",
	YEAR = 1995,
	URL = "http://www602.math.ryukoku.ac.jp/~nakano/papers/ct-thesis95.ps.gz"
}

@ARTICLE{Sat:intcnd,
	AUTHOR = "Masahiko Sato",
	TITLE = "Intuitionistic and Classical Natural Deduction Systems
		with the Catch and the Throw Rules",
	JOURNAL = tcs,
	VOLUME = 175,
	NUMBER = 1,
	PAGES = "75--92",
	YEAR = 1997,
	URL = "http://www.sato.kuis.kyoto-u.ac.jp/research/l/masahiko-catch.ps"
}

@INCOLLECTION{Sat:clabhk,
	AUTHOR = "Masahiko Sato",
	TITLE = "Classical {B}rouwer-{H}eyting-{K}olmogorov Interpretatio",
	EDITOR = "Ming Li and Akira Maruoka",
	BOOKTITLE = "Proc.\ of 8th Int.\ Conf.\ on Algorithmic 
		  Learning Theory, ALT'97, Sendai, Japan, 6--8 Oct.\ 1997",
	SERIES = lnai,
	VOLUME = 1316,
	PAGES = "176--196",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1997,
	URL = "http://www.sato.kuis.kyoto-u.ac.jp/research/l/masahiko-BHK.ps"
}

@INCOLLECTION{Kam:newfct,
	AUTHOR = "Yukiyoshi Kameyama",
	TITLE = "A New Formulation of the Catch/Throw Mechanism",
	EDITOR = "T. Ida and A. Ohori and M. Takeichi",
	BOOKTITLE = "Proc.\ of 2nd Fuji Int.\ Wksh.\ on Functional and
		Logic Programming, Shonan Village Center, Japan, 
		1--4 Nov.\ 1996",
	PAGES = ???,
	PUBLISHER = ws,
	ADDRESS = "Singapore",
	YEAR = 1997,
	URL = "http://logic.is.tsukuba.ac.jp/~kam/paper/kameyama-new-catch.ps"
}

@INCOLLECTION{KS:clactc,
	AUTHOR = "Yukiyoshi Kameyama and Masahiko Sato",
	TITLE = "A Classical Catch/Throw Calculus with Tag Abstractions
		and Its Strong Normalizability",
	EDITOR = "X. Lin",
	BOOKTITLE = "Proc.\ of 4th Computing: Australasian Theory Symp., 
		  CATS'98, Perth, Western Australia, 2--3 Feb.\ 1998",
	SERIES = "Australian Computer Science Communications",
	VOLUME = "20(3)",
	PAGES = "183--197",
	PUBLISHER = springer,
	YEAR = 1998,
	URL = "http://logic.is.tsukuba.ac.jp/~kam/paper/kameyama-classical-catch.ps"
}

@ARTICLE{KS:strnnc,
	AUTHOR = "Yukiyoshi Kameyama and Masahiko Sato",
	TITLE = "Strong Normalizability of the Non-deterministic Catch/Throw
	      Calculi",
	JOURNAL = tcs,
	VOLUME = 272,
	NUMBER = "1--2",
	SPECIAL = "Selected Papers from TTP-Tokyo'97",
	PAGES = "223--245",
	YEAR = 2002,
	URL = "http://logic.is.tsukuba.ac.jp/~kam/paper/tcs.ps"
}

@ARTICLE{Fuj:bincnd,
	AUTHOR = "Ken-etsu Fujita",
	TITLE = "A Binary-Conclusion Natural Deduction System",
	JOURNAL = ljigpl,
	VOLUME = 7,
	NUMBER = 4,
	PAGES = "517--545",
	YEAR = 1999
}

@UNPUBLISHED{Fuj:simscp,
	AUTHOR = "Ken-etsu Fujita",
	TITLE = "A Simple System of Classical Propositional Logic",
	NOTE = "Presented at Theories of Types and Proofs '97 Tokyo Meeting,
		Tokyo, Japan, 18--28 Sept 1997",
	MONTH = sep,
	YEAR = 1997
}

@ARTICLE{HKT:redrpf,
	AUTHOR = "Sachio Hirokawa and Yuichi Komori and Izumi Takeuti",
	TITLE = "A Reduction Rule for {P}eirce Formula",
	JOURNAL = sl,
	VOLUME = 56,
	NUMBER = 3,
	PAGES = "419--426",
	YEAR = 1996
}

@TECHREPORT{BKH:comllc-r,
	AUTHOR = "Kensuke Baba and Yukiyoshi Kameyama and Sachio Hirokawa",
	TITLE = "Combinatory Logic and $\lambda$-Calculus for Classical Logic",
	NUMBER = "DOI-TR-176",
	INSTITUTION = "Dept.\ of Informatics, Kyushu Univ., Fukuoka",
	MONTH = aug,
	YEAR = 2000,
	URL = "ftp://ftp.i.kyushu-u.ac.jp/pub/tr/trcs176.ps.gz"
}

@ARTICLE{BKH:comllc,
	AUTHOR = "Kensuke Baba and Yukiyoshi Kameyama and Sachio Hirokawa",
	TITLE = "Combinatory Logic and $\lambda$-Calculus for Classical Logic",
	JOURNAL = "Bull.\ of Informatics and Cybernetics",
	VOLUME = 32,
	NUMBER = 2,
	PAGES = "105--122",
	YEAR = 2000
}

@TECHREPORT{BHKKT:casccl,
	AUTHOR = "Kensuke Baba and Sachio Hirokawa and Ryo Kashima 
	       and Yuichi Komori and Izumi Takeuti",
	TITLE = "A Case Calculus for Classical Logic",
	NUMBER = "DOI-TR-178",
	INSTITUTION = "Dept.\ of Informatics, Kyushu Univ., Fukuoka",
	MONTH = aug,
	YEAR = 2000,
	URL = "ftp://ftp.i.kyushu-u.ac.jp/pub/tr/trcs178.ps.gz"
}

@ARTICLE{Zim:peirnd,
	AUTHOR = "Ernst Zimmermann",
	TITLE = "{P}eirce's Rule in Natural Deduction",
	JOURNAL = tcs,
	VOLUME = 275,
	NUMBER = ???,
	PAGES = "561--574",
	YEAR = 2002
}

@ARTICLE{Cro:conlcc,
	AUTHOR = "Tristan Crolard",
	TITLE = "A Confluent {$\lambda$}-Calculus with a Catch/Throw 
	      Mechanism",
	JOURNAL = jfp,
	VOLUME = 9,
	NUMBER = 6,
	PAGES = "625--647",
	YEAR = 1999,
	URL = "http://www.univ-paris12.fr/lacl/crolard/publications/jfp.ps.gz"
}

@TECHREPORT{Oga:prota-cpp,
	AUTHOR = "Ichiro Ogata",
	TITLE = "A Proof-Theoretical Approach to ``Classical Proofs 
		as Programs''",
	TYPE = "Technical Report",
	NUMBER = 20,
	INSTITUTION = "Electrotechnical Laboratory, Tsukuba, Japan",	
	YEAR = 1997,
	URL = "http://www.etl.go.jp/~ogata/Drafts/LKQ-lambdamu.ps.gz"
}

@TECHREPORT{Oga:prota-cps,
	AUTHOR = "Ichiro Ogata",
	TITLE = "A Proof-Theoretical Approach to Continuation Passing Style",
	TYPE = "Technical Report",
	NUMBER = 23,
	INSTITUTION = "Electrotechnical Laboratory, Tsukuba, Japan",	
	YEAR = 1997,
	URL = "http://www.etl.go.jp/~ogata/Drafts/LK-CPS.ps.gz"
}

@UNPUBLISHED{Oga:procp,
	AUTHOR = "Ichiro Ogata",
	TITLE = "Program with Classical Proofs",
	NOTE = "Presented at Theories of Types and Proofs '97 Tokyo Meeting,
		Tokyo, Japan, 18--28 Sept.\ 1997",
	MONTH = sep,
	YEAR = 1997,
	URL = "http://www.etl.go.jp/~ogata/Drafts/programNJ.ps.gz"
}


% *** Barbanera, Berardi

@INCOLLECTION{BB:extccc,
	AUTHOR = "Franco Barbanera and Stefano Berardi",
	TITLE = "Extracting Constructive Content from Classical Logic via
		Control-Like Reductions",
	EDITOR = "M. Bezem and J. F. Groote",
	BOOKTITLE = "Proc.\ of 1st Int.\ Conf.\ on Typed Lambda Calculi 
		and Applications, TLCA'93, Utrecht, The Netherlands, 
		16--18 March 1993",
	SERIES = lncs,
	VOLUME = 664,
	PAGES = "45--59",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1993
}

@ARTICLE{BB:strnrc,
	AUTHOR = "Franco Barbanera and Stefano Berardi",
	TITLE = "A Strong Normalization Result for Classical Logic",
	JOURNAL = apal,
	VOLUME = 76,
	NUMBER = 2,
	PAGES = "99--116",
	YEAR = 1995
}

@INCOLLECTION{BB:symlcc-c,
	AUTHOR = "Franco Barbanera and Stefano Berardi",
	TITLE = "A Symmetric Lambda Calculus for ``Classical'' Program
		Extraction",
	EDITOR = "M. Hagiya and J. C. Mitchell",
	BOOKTITLE = "Proc.\ of 2nd Int.\ Symp.\ on Theor.\ Aspects of
		Computer Software, TACS'94, Sendai, Japan, 19--22 Apr.\ 1994",
	SERIES = lncs,
	VOLUME = 789,
	PAGES = "495--515",	
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1994
}

@ARTICLE{BB:symlcc,
	AUTHOR = "Franco Barbanera and Stefano Berardi",
	TITLE = "A Symmetric Lambda Calculus for ``Classical'' Program
		Extraction",
	JOURNAL = iandc,
	SPECIAL = "Special Issue 2nd Int.\ Symp.\ on Theor.\ Aspects of
		Computer Software, TACS'94, Sendai, Japan, 19--22 Apr 1994",
	VOLUME = 125,
	NUMBER = 2,
	PAGES = "103--117",
	YEAR = 1996
}

@ARTICLE{BB:convsc,
	AUTHOR = "Franco Barbanera and Stefano Berardi",
	TITLE = "A Constructive Valuation Semantics for Classical Logic",
	JOURNAL = ndjfl,
	VOLUME = 37,
	NUMBER = 3,
	PAGES = "462--482",
	YEAR = 1996
}

@ARTICLE{Yam:strnsl,
	AUTHOR = "Yoriyuki Yamagata",
	TITLE = "Strong Normalization of a Symmetric Lambda Calculus
	      for Second-Order Classical Logic",
	JOURNAL = arml,
	VOLUME = 41,
	NUMBER = 1,
	PAGES = "91--99",
	YEAR = 2002
}


% *** Girard, Danos etc

@ARTICLE{Gir:newclc,
	AUTHOR = "Jean-Yves Girard",
	TITLE = "A New Constructive Logic: Classical Logic",
	JOURNAL = mscs,
	VOLUME = 1,
	NUMBER = 3,
	PAGES = "255--296",
	YEAR = 1991
}

@INCOLLECTION{DJS:lkqlkt,
	AUTHOR = "Vincent Danos and Jean-Baptiste Joinet and Harold Schellinx",
	TITLE = "{LKQ} and {LKT}: Sequent Calculi for Second Order Logic Based
		upon Dual Linear Decompositions of Classical Implication",
	EDITOR = "J.-Y. Girard and Y. Lafont and L. Regnier",
	BOOKTITLE = "Advances in Linear Logic: Proc.\ of Linear Logic 
		Wksh., Ithaca, NY, USA, 14--18 June 1993",
	SERIES = "London Math.\ Society Lecture Notes Series",
	VOLUME = 222,
	PAGES = "211--224",
	PUBLISHER = cup,
	YEAR = 1995,
	URL = "ftp://ftp.logique.jussieu.fr/pub/distrib/joinet/DanosJoinetSchellinx/lktlkq.ps.Z"
}

@UNPUBLISHED{DJS:newdll,
	AUTHOR = "Vincent Danos and Jean-Baptiste Joinet and Harold Schellinx",
	TITLE = "A New Deconstructive Logic: Linear Logic",
	NOTE = "To appear in " # jsl,
	MONTH = oct,
	YEAR = 1995,
	URL = "ftp://ftp.logique.jussieu.fr/pub/distrib/joinet/DanosJoinetSchellinx/decostringopolaro.ps.Z"
}

@INCOLLECTION{DJS:comicl,
	AUTHOR = "Vincent Danos and Jean-Baptiste Joinet and Harold Schellinx",
	TITLE = "Computational Isomorphisms in Classical Logic 
		(Extended Abstract)",
	EDITOR = "J.-Y. Girard and M. Okada and A. Scedrov",
	BOOKTITLE = "Proc.\ of Linear Logic '96 Tokyo Meeting, Keyo Univ.,
		Tokyo, Japan, 28 March -- 2 Apr.\ 1996",
	SERIES = entcs,
	VOLUME = 3,
	PUBLISHER = elsevier,
	ADDRESS = "Amsterdam",
	YEAR = 1996,
	URL = "http://www.elsevier.nl/locate/entcs/volume3.html"
}

@INCOLLECTION{CH:duac,
	AUTHOR = "Pierre-Louis Curien and Hugo Herbelin",
	TITLE = "The Duality of Computation",
	BOOKTITLE = "Proc.\ of 5th ACM SIGPLAN Int.\ Conf.\ on Functional
		  Programming, ICFP'00, Montreal, Canada, 18--21 Sept.\ 2000",
	SERIES = "SIGPLAN Notices",
	VOLUME = "35(9)",
	PUBLISHER = acm,
	ADDRESS = "New York",
	YEAR = 2000
}

@INCOLLECTION{Wad:calvdc,
	AUTHOR = "Philip Wadler",
	TITLE = "Call-by-Value is Dual to Call-by-Name",
	BOOKTITLE = "Proc.\ of 8th ACM SIGPLAN Int.\ Conf.\ on Functional 
	     Programming, ICFP'03, Uppsala, Sweden, 25--29 Aug.\ 2003",
	SERIES = "SIGPLAN Notices",
	VOLUME = "38(9)",
	PAGES = "189--201",
	PUBLISHER = acm,
	ADDRESS = "New York",
	YEAR = 2003,
	URL = "http://www.research.avayalabs.com/user/wadler/papers/dual/dual.pdf"
}


% *** Schwichtenberg and Berger

@INCOLLECTION{BS:proecp,
	AUTHOR = "Ulrich Berger and Helmut Schwichtenberg",
	TITLE = "Program Extraction from Classical Proofs",
	EDITOR = "Daniel Leivant",
	BOOKTITLE = "Selected Papers Int.\ Workshop on Logic and Computational
		Complexity, LCC'94, Indianapolis, USA, 13--16 Oct.\ 1994",
	SERIES = lncs,
	VOLUME = 960,
	PAGES = "77--97",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1995,
	URL = "http://www.mathematik.uni-muenchen.de/~schwicht/papers/lcc94/r1.dvi.Z"
}

@ARTICLE{BBS:refpec,
	AUTHOR = "Ulrich Berger and Wilfried Buchholz 
	       and Helmut Schwichtenberg",
	TITLE = "Refined Program Extraction from Classical Proofs",
	JOURNAL = apal,
	VOLUME = 114,
	NUMBER = "1--3",
	SPECIAL = "Commemorative Symp.\ Dedicated to Anne S. Troelstra
		on the Occasion of His 60th Birthday,
		Noordwijkerhout, The Netherlands, 16--18 Sept.\ 1999",
	PAGES = "3--25",
	YEAR = 2002
}

% *** complementary systems

@ARTICLE{Mor:senclf,
	AUTHOR = "Charles G. Morgan",
	TITLE = "Sentential Calculus for Logical Falsehoods",
	JOURNAL = ndjfl,
	VOLUME = 14,
	NUMBER = 3,
	PAGES = "347--353",
	YEAR = 1973
}

@ARTICLE{Cai:forsnt,
	AUTHOR = "Xavier Caicedo",
	TITLE = "A Formal System for the Non-Theorems of the Propositional
		Calculus",
	JOURNAL = ndjfl,
	VOLUME = 19,
	NUMBER = 1,
	PAGES = "147--151",
	YEAR = 1978
}

@ARTICLE{Var:comsl,
	AUTHOR = "Achille C. Varzi",
	TITLE = "Complementary Sentential Logics",
	JOURNAL = "Bulletin of the Section of Logic",
	VOLUME = 19,
	NUMBER = 4,
	PAGES = "112--116",
	PUBLISHER = "Inst.\ of Philos.\ and Sociol., 
		Polish Acad.\ of Sciences",
	YEAR = 1990
}

@ARTICLE{Var:comlcp,
	AUTHOR = "Achille C. Varzi",
	TITLE = "Complementary Logics for Classical Propositional Lanaguages",
	JOURNAL = "Kriterion",
	VOLUME = 4,
	PAGES = "20--24",
	YEAR = 1992
}

@INCOLLECTION{Var:trufb,
	AUTHOR = "Achille C. Varzi",
	TITLE = "Truth, Falsehood and Beyond",
	EDITOR = "L. Albertazzi and R. Poli",
	BOOKTITLE = "Topics in Philosophy and Artificial Intelligence",
	PAGES = "39--50",
	PUBLISHER = "Mitteleurop{\"a}isches Kulturinstitut",
	ADDRESS = "Basel",
	YEAR = 1991
}

@INCOLLECTION{CV:arrt,
	AUTHOR = "Roberto Casati and Achille C. Varzi",
	TITLE = "True and False: An Exchange",
	EDITOR = "Anil Gupta and Andr{\'e} Chapuis",
	BOOKTITLE = "Circularity, Definition, and Truth",
	PAGES = "365--370",
	PUBLISHER = "Indian Council of Philosophical Research",
	ADDRESS = "New Delphi",
	YEAR = 1999
}


% ========================================================================
% ========================================================================


% *** serious proof theory, ordinals etc

@ARTICLE{Mil:norfco,
	AUTHOR = "Larry W. Miller",
	TITLE = "Normal Functions and Constructive Ordinal Notations",
	JOURNAL = jsl,
	VOLUME = 41,
	NUMBER = 2,
	PAGES = "439--459",
	YEAR = 1976
}

@ARTICLE{CW:sloggh,
	AUTHOR = "E. A. Chicona dn S. S. Wainer",
	TITLE = "The Slow-Growing and the Grzegorvzyk Hierarchies",
	JOURNAL = jsl,
	VOLUME = 48,
	NUMBER = 2,
	PAGES = "399--408",
	YEAR = 1983
}

@ARTICLE{Wai:slogfg,
	AUTHOR = "S. S. Wainer",
	TITLE = "Slow Growing versus Fast Growing",
	JOURNAL = jsl,
	VOLUME = 54,
	NUMBER = 2,
	PAGES = "608--614",
	YEAR = 1989
}

@ARTICLE{FS:ordcrd,
	AUTHOR = "M. V. H. Fairtlough and S. S. Wainer",
	TITLE = "Ordinal Complexity of Recursive Definitions",
	JOURNAL = iandc,
	VOLUME = 99,
	NUMBER = 2,
	PAGES = "123--153",
	YEAR = 1992
}

@ARTICLE{Sch:finnit,
	AUTHOR = "Helmut Schwichtenberg",
	TITLE = "Finite Notations for Infinite Derivations",
	JOURNAL = apal,
	VOLUME = 94,
	NUMBER = "1--3",
	SPECIAL = "Meeting on Computability Theory, Oberwolfach, Germany,
		27 Jan.--3 Feb.\ 1996",
	PAGES = "201--222",
	YEAR = 1998
}

@ARTICLE{Min:redfid,
	AUTHOR = "Grigori Mints",
        TITLE = "Reduction of Finite and Infinite Derivations",
	JOURNAL = apal,
	VOLUME = 104,
	NUMBER = "1--3",
	SPECIAL = "Proc.\ of Workshop on Proof Theory and Complexity,
		PTAC'98, {\AA}rhus, Denmark, 3--7 Aug.\ 1998",
	PAGES = "167--188",
	YEAR = 2000
}

INCOLLECTION{AJ:conn,
	AUTHOR = "Klaus Aehlig and Felix Joachimski",
	TITLE = "On Continuous Normalization",
	EDITOR = "Julian C. Bradfield",
	BOOKTITLE = "Proc.\ of 16th Int.\ Wksh.\ on Computer Science Logic, 
		  CSL 2002 (Edinburgh, UK, 22--25 Sept.\ 2002)",
	SERIES = lncs,
	VOLUME = 2471,
	PAGES = "59--73",
	PUBLISHER = springer-verlag,
	ADDRESS = "Berlin",
	YEAR = 2002
}


% ========================================================================
% ========================================================================


% *** Frege structures

@INCOLLECTION{Acz:fresnp,
	AUTHOR = "Peter Aczel",
	TITLE = "{F}rege Structures and the Notions of Proposition,
	      Truth and Set",
	EDITOR = "Jon Barwise and H. Jerome Keisler and Kenneth Kunen",
	BOOKTITLE = "The Kleene Symp.: Proc.\ of Symp., Madison,
		  WI, USA, 18--24 June 1978",
	SERIES = slfm,
	VOLUME = 101,
	PAGES = "31--59",
	PUBLISHER = nh,	
	ADDRESS = "Amsterdam",
	YEAR = 1980
}

@INCOLLECTION{Sat:addpoi,
	AUTHOR = "Masahiko Sato",
	TITLE = "Adding Proof Objects and Inductive Definition Mechanisms
		to Frege Structures",
	EDITOR = "T. Ito and A. R. Meyer",
	BOOKTITLE = "Proc.\ of 1st Int.\ Conf.\ on Theoretical
		Aspects of Computer Software, TACS'91, Sendai, Japan,
		24--27 Japan 1991",
	SERIES = lncs,
	VOLUME = 526,
	PAGES = "38--52",	
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1991
}

% *** Feferman's theories of functions and classes, explicit mathematics, 
% *** Japanese realizability stuff


@INCOLLECTION{Fef:lanaem,
	AUTHOR = "Solomon Feferman",
	TITLE = "A Language and Axioms for Explicit Mathematics",
	EDITOR = "J. N. Crossley",
	BOOKTITLE = "Algebra and Logic: Papers 14th Summer Research 
		Institute of the Australian Math.\ Society, Monash Univ.,
		Clayton, Victoria, Australia, 6 Jan -- 16 Feb 1974",
	SERIES = lnm,
	VOLUME = 450,
	PAGES = "87--139",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1975
}

@INCOLLECTION{Fef:contfc,
	AUTHOR = "Solomon Feferman",
	TITLE = "Constructive Theories of Functions and Classes",
	EDITOR = "M. Boffa and D. van Dalen and K. McAloon",
	BOOKTITLE = "Proc.\ of Logic Colloquium '78, Mons, Belgium, 
		24 Aug -- 1 Sept 1978",
	SERIES = slfm,
	VOLUME = 97,
	PAGES = "159--224",
	PUBLISHER = nh,
	ADDRESS = "Amsterdam",
	YEAR = 1979
}

@BOOK{BFPS:iteids,
	AUTHOR = "Wilfried Buchholz and Solomon Feferman and
	       Wolfram Pohlers and Wilfried Sieg",
	TITLE = "Iterated Inductive Definitions and Subsystems of
	       Analysis: Recent Proof-Theoretical Results",
	SERIES = lnm,
	VOLUME = 897,
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1981
}

@INCOLLECTION{Fef:monid,
	AUTHOR = "Solomon Feferman",
	TITLE = "Monotone Inductive Definitions",
	EDITOR = "A. S. Troelstra and D. van Dalen",
	BOOKTITLE = "Proc.\ of L.~E.~J. Brouwer Centenary Symp.,
		Noordwijkerhout, The Netherlands, 8--13 June 1981",
	SERIES = slfm,
	VOLUME = 110,
	PAGES = "77--89",
	PUBLISHER = nh,
	ADDRESS = "Amsterdam",
	YEAR = 1982
}
	
@ARTICLE{Tak:monidc,
	AUTHOR = "Shuzo Takahashi",
	TITLE = "Monotone Inductive Definitions in a Constructive Theory
		of Functions and Classes",
	JOURNAL = apal,
	VOLUME = 42,
	NUMBER = 3,
	PAGES = "255--297",
	YEAR = 1989
}

@ARTICLE{Pal:typtii,
	AUTHOR = "Erik Palmgren",
	TITLE = "Type-Theoretic Interpretation of Iterated, 
	      Strictly Positive Inductive Definitions",
	JOURNAL = arml,
	VOLUME = 32,
	NUMBER = 2,
	PAGES = "75--99",
	YEAR = 1992
}

@ARTICLE{GR:strsml,
	AUTHOR = "Edward Griffor and Michael Rathjen",
	TITLE = "The Strength of Some {M}artin-{L}{\"o}f Type Theories",
	JOURNAL = arml,
	VOLUME = 33,
	NUMBER = ???,
	PAGES = "347--385",
	YEAR = 1994
}

@ARTICLE{Rat:monide,
	AUTHOR = "Michael Rathjen",
	TITLE = "Monotone Inductive Definitions in Explicit Mathematics",
	JOURNAL = jsl,
	VOLUME = 61,
	NUMBER = 1,
	PAGES = "125--146",
	YEAR = 1996
}

@ARTICLE{JS:totat,
	AUTHOR = "Gerhard J{\"a}ger and Thomas Strahm",
	TITLE = "Totality in Applicative Theories",
	JOURNAL = apal,
	VOLUME = 74,
	NUMBER = 2,
	PAGES = "105--120",
	YEAR = 1995
}

@ARTICLE{Gla:undufe,
	AUTHOR = "Thomas Gla{\ss}",
	TITLE = "Understanding Uniformity in {F}eferman's
	      Explicit Mathematics",
	JOURNAL = apal,
	VOLUME = 75,
	NUMBER = "1--2",
	PAGES = "89--106",
	YEAR = 1995
}

@ARTICLE{FJ:sysemn2,
	AUTHOR = "Solomon Feferman and Gerhard J{\"a}ger",
	TITLE = "Systems of Explicit Mathematics with Non-constructive
	      {$\mu$}-Operator, Part {II}",
	JOURNAL = apal,
	VOLUME = 79,
	NUMBER = 1,
	PAGES = "37--52",
	YEAR = 1996
}

@ARTICLE{GS:sysemn,
	AUTHOR = "Thomas Gla{\ss} and Thomas Strahm",
	TITLE = "Systems of Explicit Mathematics with Non-constructive
	      {$\mu$}-Operator and Join",
	JOURNAL = apal,
	VOLUME = 82,
	NUMBER = 2,
	PAGES = "193--219",
	YEAR = 1996
}

@ARTICLE{GRS:protsm,
	AUTHOR = "Thomas Gla{\ss} and Michael Rathjen and		
		Andreas Schl{\"u}ter",
	TITLE = "On the Proof-Theoretic Strength of Monotone Induction
		in the Explicit Mathematics",
	JOURNAL = apal,
	VOLUME = 85,
	NUMBER = 1,
	PAGES = "1--46",
	YEAR = 1997
}

@ARTICLE{Str:noncmo,
	AUTHOR = "Thomas Strahm",
	TITLE = "The Non-constructive {$\mu$}-Operator, Fixed Point
	      Theories with Ordinals and the Bar Rule",
	JOURNAL = apal,	    
	VOLUME = 104,
	NUMBER = "1--3",
	PAGES = "305--324",
	YEAR = 2000
}


@INCOLLECTION{Tup:finrlp1,
	AUTHOR = "Sergei Tupailo",
	TITLE = "Finitary Reductions for Local Predicativity, {I}:
	      Recursively Regular Ordinals",
	EDITOR = "S. Buss and P. Hajek and P. Pudlak",
	BOOKTITLE = "Logic Colloquium '98: Proc.\ of Ann.\ Europ.\
		  Summer Meeting of ASL, 
		  Prague, Czech Rep., 9--15 Aug.\ 1998",
	SERIES = lnl,
	VOLUME = 13,
	PAGES = "465--499",
	PUBLISHER = "Assoc.\ for Symb.\ Logic",
	ADDRESS = "Natick, MA",
	YEAR = 2000
}

@ARTICLE{Tup:reaaem,
	AUTHOR = "Sergei Tupailo",
	TITLE = "Realization of Analysis into Explicit
	      Mathematics",
	JOURNAL = jsl,
	VOLUME = 66,
	NUMBER = 4,
	PAGES = "1848--1864",
	YEAR = 2001
}

@ARTICLE{Tup:reaste,
	AUTHOR = "Sergei Tupailo",
	TITLE = "Realization of Constructive Set Theory into Explicit
	       Mathematics: A Lower Bound for Impredicative {M}ahlo 
	       Universe",
	JOURNAL = apal,
	VOLUME = 120,
	NUMBER = "1--3",
	PAGES = "165--196",
	YEAR = 2003
}


% Japanese stuff

@BOOK{HN:pxcl,
	AUTHOR = "Susumu Hayashi and Hiroshi Nakano",
	TITLE = "{PX}, a Computational Logic",
	SERIES = "Foundations of Computing",
	PUBLISHER = mit,
	ADDRESS = "Cambridge, MA",
	YEAR = 1988
}

@ARTICLE{Hay:towapt,
	AUTHOR = "Susumu Hayashi",
	TITLE = "Towards the Animation of Proofs---Testing Proofs 
	      by Examples",
	JOURNAL = tcs,
	VOLUME = 272,
	NUMBER = "1--2",
	SPECIAL = "Selected Papers TTP-Tokyo'97",
	PAGES = "177--195",
	YEAR = 2002
}

@ARTICLE{Tat:prosur,
	AUTHOR = "Makoto Tatsuta",
	TITLE = "Program Synthesis Using Realizability",
	JOURNAL = tcs,
	VOLUME = 90,
	NUMBER = 2,
	PAGES = "309--353",
	YEAR = 1991
}

@ARTICLE{KT:reaigi,
	AUTHOR = "Satoshi Kobayashi and Makoto Tatsuta",
	TITLE = "Realizability Interpretation of Generalized Inductive
		Definitions",
	JOURNAL = tcs,
	VOLUME = 131,
	NUMBER = 1,
	PAGES = "121--138",
	YEAR = 1994
}

@INCOLLECTION{Tat:monrdp,
	AUTHOR = "Makoto Tatsuta",
	TITLE = "Monotone Recursive Definition of Predicates
		and Its Realizability Interpretation",
	EDITOR = "T. Ito and A. R. Meyer",
	BOOKTITLE = "Proc.\ of 1st Int.\ Conf.\ on Theoretical
		Aspects of Computer Software, TACS'91, Sendai, Japan,
		24--27 Japan 1991",
	SERIES = lncs,
	VOLUME = 526,
	PAGES = "38--52",	
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1991
}

@ARTICLE{Tat:tworim,
	AUTHOR = "Makoto Tatsuta",
	TITLE = "Two Realizability Interpretations of Monotone
		Inductive Definitions",
	JOURNAL = ijfcs,
	VOLUME = 5,
	NUMBER = 1,
	PAGES = "1--21",
	YEAR = 1994
}					% journal version of Tat:monrdp

@INCOLLECTION{Tat:reaicd-c,
	AUTHOR = "Makoto Tatsuta",
	TITLE = "Realizability Interpretation of Coinductive Definitions
		and Program Synthesis with Streams",
	BOOKTITLE = "Proc.\ of 4th Int.\ Conf.\ on Fifth Generation 
		Computer Systems, FGCS'92, Tokyo, Japan, 1--5 June 1992,
		volume 2",
	PAGES = "666--673",
	PUBLISHER = "Ohmsha, Tokyo, and IOS, Amsterdam",
	YEAR = 1992
}

@ARTICLE{Tat:reaicd-j,
	AUTHOR = "Makoto Tatsuta",
	TITLE = "Realizability Interpretation of Coinductive Definitions
		and Program Synthesis with Streams",
	JOURNAL = tcs,
	VOLUME = 122,
	NUMBER = "1--2",
	PAGES = "119--136",
	YEAR = 1994
}

@INCOLLECTION{Tat:reamcd,
	AUTHOR = "Makoto Tatsuta",
	TITLE = "Realizability of Monotone Coinductive Definitions and Its
		Application to Program Synthesis",
	EDITOR = "J. Jeuring",
	BOOKTITLE = "Proc.\ of 4th Int.\ Conf.\ on Mathematics of Program
		Construction, MPC'98, Marstrand, Sweden, 15--17 June 1998",
	SERIES = lncs,
	VOLUME = 1422,
	PAGES = "338--364",
	PUBLISHER = springer,
	ADDRESS = "Berlin",
	YEAR = 1998
}

@INCOLLECTION{Tat:reactf,
	AUTHOR = "Makoto Tatsuta",	
	TITLE = "Realizability for Constructive Theory of Functions	
	      and Classes and Its Application to Program Synthesis",
	BOOKTITLE = "Proc.\ of 13th Ann.\ IEEE Symp.\ on Logic in
		  Computer Science, LICS'98, Indianapolis, IN, USA,
		  21--24 June 1998",
	PAGES = "358--367",
	PUBLISHER = ieee,
	ADDRESS = "Los Alamitos, CA",
	YEAR = 1998
}

@ARTICLE{Kam:typfth,
	AUTHOR = "Yukiyoshi Kameyama",
	TITLE = "A Type-Free Theory of Half-Monotone Inductive Definitions",
	JOURNAL = ijfcs,
	VOLUME = 6,
	NUMBER = 3,
	PAGES = "203--234",
	YEAR = 1995,
	URL = "http://www.sato.kuis.kyoto-u.ac.jp/~kameyama/link/kameyama-half-monotone.dvi"
}