% This file was created with JabRef 2.3b2. % Encoding: ISO-8859-1 @PREAMBLE{ {\newcommand{\noopsort}[1]{} \newcommand{\singleletter}[1]{#1} } } @STRING{ADW = {Addison-Wesley}} @STRING{AMS = {American Mathematical Society}} @INPROCEEDINGS{Janicic06a, author = {Jani{\v c}i{\'c}, Predrag and Quaresma, Pedro}, title = {{S}ystem {D}escription: {GCLC}prover + {G}eo{T}hms}, booktitle = {Automated Reasoning}, year = {2006}, number = {4130}, series = {LNAI}, pages = {145--150}, publisher = {Springer}, comment = {IJCAR 2006, editores Furbach, Ulrich and Shankar, Natarajan}, crossref = {ijcar06}, owner = {pedro}, timestamp = {2007.05.18} } @INPROCEEDINGS{Liang04, author = {Tielin Liang and Dongming Wang}, title = {Towards a Geometric-Object-Oriented Language.}, booktitle = {Automated Deduction in Geometry}, year = {2004}, pages = {130-155}, bibsource = {DBLP, http://dblp.uni-trier.de}, crossref = {adg04}, ee = {http://dx.doi.org/10.1007/11615798_9}, owner = {pedro}, timestamp = {2007.05.21} } @INPROCEEDINGS{Quaresma06d, author = {Quaresma, Pedro and Jani{\v c}i{\'c}, Predrag}, title = {Integrating Dynamic Geometry Software, Deduction Systems, and Theorem Repositories}, booktitle = {Mathematical Knowledge Management}, year = {2006}, pages = {280--294}, crossref = {mkm06}, owner = {pedro}, timestamp = {2007.05.21} } @MISC{CabriWeb, author = {Cabri Web site}, howpublished = {http://www.cabri.com}, owner = {pedro}, timestamp = {2007.05.18} } @MISC{CinderellaWeb, author = {Cinderella Web site}, howpublished = {http://www.cinderella.de}, owner = {pedro}, timestamp = {2007.05.18} } @MISC{SketchpadWeb, author = {Geometer's~Sketchpad Web site}, howpublished = {http://www.keypress.com/sketchpad/}, owner = {pedro}, timestamp = {2007.05.18} } @ARTICLE{Bruijn72, author = {{de Bruijn}, N. G.}, title = {Lambda Calculus notation with nameless dummies, a tool for automatic formula manipulation, with aplication to the Church-Rosser Theorem}, journal = {Indagationes Mathematicae}, year = {1972}, volume = {34}, pages = {381--392}, number = {5} } @BOOK{Menezes96, title = {Handbook of Applied Cryptography}, publisher = {CRC Press}, year = {1996}, author = {A. Menezes, P. van Oorschot, S. Vanstone}, owner = {pedro}, timestamp = {2007.07.24} } @BOOK{Troelstra88, title = {Constructivism in Mathematics --- An Introduction}, publisher = {North-Holland Publishing Co.}, year = {1988}, author = {A.S.Troelstra and D.van Dalen}, volume = {1}, series = {Studies in Logic, and The Foundations of Mathematics}, address = {Amsterdam}, annote = {1 - constructive mathematics} } @INCOLLECTION{Aczel91, author = {Peter Aczel and David P. Carlisle and Nax Mendler}, title = {Two frameworks of theories and their implementation in {I}sabelle}, booktitle = {Logical Frameworks}, publisher = {Cambridge University Press}, year = {1991}, editor = {G. Huet and G. Plotkin}, pages = {3--39}, keywords = {Isabelle} } @BOOK{Aho83, title = {Data Structures and Algorithms}, publisher = {Addison-Wesley Publishing Company}, year = {1983}, author = {Aho, Alfred and Hopcroft, John and Ullman, Jeffrey} } @BOOK{Aho86, title = {Compilers, Principles, Techniques and Tools}, publisher = {Addison-Wesley}, year = {1986}, author = {Alfred Aho and Ravi Sethi and J. Ullman}, address = {Reading} } @BOOK{Alagic78, title = {The Design of Well-Structured and Correct Programs}, publisher = {Springer-Verlag}, year = {1978}, author = {Suad Alagi\v{c} and Michael A. Arbib}, address = {New York}, annote = {ucmt I-10-26} } @BOOK{Andrews86, title = {An Introduction to Mathematical Logic and Type Theory: To Truth through Proof}, publisher = {Academic Press, Inc.}, year = {1986}, author = {Peter B. Andrews}, annote = {Tenho fotocopias} } @BOOK{Arbib75, title = {Arrows, Structures and Functors}, publisher = {Academic Press}, year = {1975}, author = {Arbib, Michael A. and Manes, Ernest G.}, address = {New York}, annote = {Categorias, Teoria dos Functores, Algebra, Livre e Colivre} } @BOOK{Arbib79, title = {Arrows, Structures and Functors -- The Categorical Imperative}, publisher = {Academic Press, Inc.}, year = {1975}, author = {Michael A. Arbib and Ernest G. Manes}, address = {New York}, annote = {Categorias, Teoria dos Functores, Algebra, Topos} } @BOOK{Arbib80, title = {A Basis for Theoretical Computer Science}, publisher = {Springer-Verlag}, year = {1980}, author = {Michael Arbib and A. J. Kfoury and Robert N. Moll}, series = {Texts and Monographs in Computer Science}, address = {New York}, annote = {Ci{\^e}ncias da Computa{\c c}{\~a}o} } @MISC{Aspinall91, author = {David R. Aspinall}, title = {{Isabelle Modules}: a New Theory Mechanism for {Isabelle}}, howpublished = {Undergraduate dissertation, University of Cambridge}, year = {1991}, keywords = {Isabelle} } @INPROCEEDINGS{Atkins94, author = {Atkins, D. and Graff, M. and Lenstra, A. and Leyland, P.}, title = {The Magic Words are Squeamish Ossifrage}, booktitle = {ASIACRYPT 1994}, year = {1994}, pages = {263-277} } @ARTICLE{Avron93, author = {Arnon Avron}, title = {Gentzen-Type Systems, Resolution and Tableaux}, journal = {Journal of Automated Reasoning}, year = {1993}, volume = {10}, pages = {265-281}, annote = {pqa} } @ARTICLE{Avron91, author = {Arnon Avron}, title = {Simple Consequence Relations}, journal = {Information and Computation}, year = {1991}, volume = {92}, pages = {105--139}, number = {1}, month = {MAY}, annote = {ucmat (a revista)} } @BOOK{Baase83, title = {Computer Algorithms: Introduction to Design and Analysis}, publisher = {Addison-Wesley Publishing Company}, year = {1983}, author = {Baase, Sara} } @BOOK{Bakker80, title = {Mathematical Theory of Program Correctness}, publisher = {Prentice-Hall International}, year = {1980}, author = {Jaco de Bakker}, series = {Computer Science}, address = {London}, annote = {computer programs - testing; prova de correc\c{c}{\~a}o de programas; axiomatica de Hoare} } @MISC{Barbosa06, author = {Barbosa, Geraldo}, title = {Pequena an{\'a}lise estat{\'\i}stica da l{\'\i}ngua portuguesa: {M}achado de {A}ssis e {P}ero {V}az de {C}aminha}, howpublished = {http://www.linguateca.pt/Repositorio/Barbosa2006.pdf}, year = {2006} } @BOOK{Barendregt81, title = {The Lambda Calculus, Its Syntax and Semantics}, publisher = {North-Holland Publishing Company}, year = {1981}, author = {Hendrick Pieter Barendregt}, volume = {103}, series = {Studies in Logic and The Foundations of Mathematics}, address = {Amsterdam}, annote = {Lambda Calculus; Logica} } @INPROCEEDINGS{Basin94, author = {David A. Basin}, title = {Logic Frameworks for Logic Programs}, booktitle = {4th International Workshop on Logic Program Synthesis and Transformation, {LOPSTR '94}}, year = {1994}, publisher = {Springer-Verlag}, note = {To appear}, keywords = {Isabelle} } @INPROCEEDINGS{Basin93ssd, author = {David A. Basin and Alan Bundy and Ina Kraan and Sean Matthews}, title = {A Framework for Program Development Based on Schematic Proof}, booktitle = {Proceedings of the 7th International Workshop on Software Specification and Design}, year = {1993}, pages = {162--171}, publisher = {IEEE Computer Society Press}, keywords = {Isabelle} } @BOOK{Bergstra89, title = {Algebraic Specification}, publisher = {Addison-Wesley}, year = {1989}, author = {J. A. Bergstra}, optaddress = {Wokingham} } @ARTICLE{Bertot04, author = {Bertot, Yves and Guilhot, Fr{\'e}d{\'e}rique and Pottier, Lo{\"i}c}, title = {Visualizing Geometrical Statements with {G}eo{V}iew.}, journal = {Electr. Notes Theor. Comput. Sci.}, year = {2004}, volume = {103}, pages = {49--65}, bibsource = {DBLP, http://dblp.uni-trier.de}, ee = {http://dx.doi.org/10.1016/j.entcs.2004.09.013} } @BOOK{Berztiss75, title = {Data Structures: Theory and practice}, publisher = {Academic Press}, year = {1975}, author = {Berztss, A. T.}, edition = {2nd} } @INPROCEEDINGS{Bibel93, author = {W. Bibel and E. Eder}, title = {Methods and Calculi for Deduction}, booktitle = {Handbook of Logic in Artificial and Logic Programming}, year = {1993}, editor = {Dov M . Gabbay and C. J. Hogger and J. A. Robinson}, volume = {1}, pages = {67--182}, address = {Oxford}, publisher = {Oxford Science Publications}, annote = {Tenho fotocopias parciais. ucmt 03-00/Han/V.1} } @BOOK{Bird98, title = {Introduction to Functional Programming using Haskell}, publisher = {Prentice Hall}, year = {1998}, author = {Richard Bird}, optaddress = {London}, optedition = {second}, optseries = {Computer Science} } @BOOK{Bishop98, title = {Java Gently}, publisher = {Addison-Wesley}, year = {1998}, author = {Judy M. Bishop}, address = {Harlow, England}, edition = {2nd}, owner = {pedro}, timestamp = {2007.02.22} } @BOOK{Bollobas79, title = {Graph Theory: An Introductory Course}, publisher = {Springer-Verlag}, year = {1979}, author = {Bollob{\'a}s, B{\'e}la}, address = {New York} } @BOOK{Booch94, title = {Object Oriented Analysis and Design, with Applications}, publisher = {Addison Wesley Longman, Inc.}, year = {1994}, author = {Booch, Grady}, edition = {2nd}, note = {DMAT 68N/BOO; Programa{\c c}{\~a}o Orientada para objectos.} } @BOOK{Booch91, title = {Object Oriented Design with Applications}, publisher = {The Bejamin/Cummings Publishing Company, Inc.}, year = {1991}, author = {Booch, Grady}, address = {Redwood City, USA}, note = {Programa\c{c}{\~a}o Orientada para Objectos} } @BOOK{Borceaux94a, title = {Handbook of categorical Algebra 1, Basic Category Theory}, publisher = {Cambridge University Press}, year = {1994}, author = {Francis Borceaux}, series = {Encyclopedia of Mathematics and its applications}, address = {Cambridge}, annote = {ucma 18-01/BOR/V.1}, isbn = {0-521-44178-1}, language = {ingles} } @BOOK{Borceaux94c, title = {Handbook of Categorical Algebra 3, Categories of Sheaves}, publisher = {Cambridge University Press}, year = {1994}, author = {Francis Borceaux}, series = {Encyclopedia of Mathematics and its applications}, address = {Cambridge}, annote = {ucma 18-01/BOR/V.3}, isbn = {0-521-44180-3} } @ARTICLE{Botana02, author = {Botana, Francisco and {L. Valcarce}, Jos{\'e}}, title = {A dynamic-symbolic interface for geometric theorem discovery}, journal = {Computers and Education}, year = {2002}, volume = {38}, pages = {21--35} } @ARTICLE{Brink9?, author = {C. Brink and Rewitzky}, title = {The Student's Companion to Referencing in Mathematical Papers}, journal = {Questiones Mathematicae}, year = {199?}, annote = {J{\'a} n{\~a}o sei como obtive este artigo.} } @INPROCEEDINGS{Broy94, author = {Manfred Broy and Ursula Hinkel and Tobias Nipkow and Christian Prehofer and Birgit Schieder}, title = {Interpreter Verification for a Functional Language}, booktitle = {Proceedings of the 14th Conference on Foundations of Software Technology and Theoretical Computer Science}, year = {1994}, publisher = {Springer-Verlag LNCS}, note = {To appear}, keywords = {Isabelle} } @ARTICLE{Buchberger06, author = {B. Buchberger and A. Craciun and T. Jebelean and L. Kovacs and T. Kutsia and K. Nakagawa and F. Piroi and N. Popov and J. Robu and M. Rosenkranz and W. Windsteiger}, title = {Theorema: Towards Computer-Aided Mathematical Theory Exploration}, journal = {Journal of Applied Logic}, year = {2006}, volume = {4}, pages = {470--504}, number = {4}, file = {Theorema-JAL-revised.pdf:/home/pedro/Actividades/Investigacao/ArqArtigos/DemGeo/Theorema-JAL-revised.pdf:PDF}, url = {http://dx.doi.org/10.1016/j.jal.2005.10.006} } @BOOK{Buchmann00, title = {Introduction to Cryptography}, publisher = {Springer-Verlag}, year = {2000}, author = {Buchmann, Johannes}, address = {New York} } @BOOK{Budd97, title = {An Introduction to Object-Oriented Programming}, publisher = {Addison-Wesley}, year = {1996}, author = {Budd, Timothy}, edition = {2nd}, month = {December}, note = {DMAT 68U/BUD; Programa{\c c}{\~a}o Orientada para Objectos} } @BOOK{Bundy83, title = {The Computer Modelling of Mathematical Reasoning}, publisher = {Academic Press, Inc.}, year = {1983}, author = {Alan Bundy}, address = {24/28 Oval Road, London NW1}, annote = {inteligencia artificial, skolem} } @INPROCEEDINGS{Burstall82, author = {R.M. Burstall and J.A. Goguen}, title = {Algebras, Theories and Freeness: an introduction for computer scientists}, booktitle = {Theoretical Foundations of Programming Methodology}, year = {1982}, editor = {M. Broy and G. Schmidt}, pages = {329.349}, publisher = {D. Reidel Publishing Company}, annote = {Tenho uma fotocopia do artigo} } @TECHREPORT{Cant92tr, author = {A. Cant}, title = {Program Verification Using Higher Order Logic}, institution = {Electronics Research Laboratory, DSTO}, year = {1992}, number = {ERL-0600-RR}, keywords = {Isabelle} } @INPROCEEDINGS{Cant92ml, author = {A. Cant and M. A. Ozols}, title = {A Verification Environment for {ML} Programs}, booktitle = {Workshop on ML and its Applications}, year = {1992}, editor = {Peter Lee}, pages = {151--156}, address = {San Francisco, California}, month = {June}, organization = {ACM SIGPLAN}, keywords = {Isabelle} } @BOOK{Chang73, title = {Symbolic Logic and Mechanical Theorem Proving}, publisher = {Academic Press, Inc.}, year = {1973}, author = {Chin-Liang Chang and Richard Char-Tung Lee}, address = {Orlando}, annote = {Demonstra\c{c}{\~a}o Autom{\'e}tica de Teoremas; Descreve o Pr\'incipio da Resolu\c{c}{\~a}o assim como v{\'a}rias das suas implementa\c{c}{\~o}es} } @ARTICLE{Chou1988, author = {Chou, Shang-Ching}, title = {An Introduction to Wu's Method for Mechanical Theorem Proving in Geometry}, journal = {Journal of Automated Reasoning}, year = {1988}, volume = {4}, pages = {237-267}, owner = {pedro}, timestamp = {2006.11.24} } @BOOK{Chou87, title = {Mechanical Geometry Theorem Proving}, publisher = {D. Reidel Publishing Company}, year = {1987}, author = {Chou, Shang-Ching}, address = {Dordrecht} } @INPROCEEDINGS{Chou93, author = {Chou, Shang-Ching and Gao, Xiao-Shan and Zhang, Jing-Zhong}, title = {Automated production of traditional proofs for constructive geometry theorems}, booktitle = {Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science {LICS}}, year = {1993}, editor = {Vardi, Moshe}, pages = {48--56}, month = {June}, publisher = {IEEE Computer Society Press} } @ARTICLE{Chou96, author = {Chou, Shang-Ching and Gao, Xiao-Shan and Zhang, Jing-Zhong}, title = {Automated Generation of Readable Proofs with Geometric Invariants, {I}. Multiple and Shortest Proof Generation}, journal = {Journal of Automated Reasoning}, year = {1996}, volume = {17}, pages = {325-347} } @ARTICLE{Chou96a, author = {Chou, Shang-Ching and Gao, Xiao-Shan and Zhang, Jing-Zhong}, title = {Automated Generation of Readable Proofs with Geometric Invariants, {II}. Theorem Proving With Full-Angles}, journal = {Journal of Automated Reasoning}, year = {1996}, volume = {17}, pages = {349-370} } @UNPUBLISHED{Chou95, author = {Chou, Shang-Ching and Gao, Xiao-Shan and Zhang, Jing-Zhong}, title = {Automated Production of Traditional Proofs for Theorems in Euclidian Geometry}, note = {Obtido a partir da rede}, year = {1995} } @ARTICLE{Chou95a, author = {Chou, Shang-Ching and Gao, Xiao-Shan and Zhang, Jing-Zhong}, title = {Automated Production of Traditional Proofs in Solid Geometry}, journal = {Journal of Automated Reasoning}, year = {1995}, volume = {14}, pages = {257--291} } @BOOK{Church41, title = {The Calculi of Lambda-Conversion}, publisher = {Princeton University Press}, year = {1941}, author = {Alonzo Church}, address = {Princeton}, annote = {ucmat 03b chu; 2a impressao 1951}, keywords = {Logica; lambda-calculo; logica combinatoria}, language = {ingles} } @TECHREPORT{Ciesielski91, author = {B. Ciesielski and M. Wand}, title = {Using the Theorem Prover {Isabelle-91} to Verify a Simple Proof of Compiler Correctness}, institution = {Northeastern University, College of Computer Science}, year = {1991}, number = {NU-CCS-91-20}, month = {dec}, keywords = {Isabelle} } @MANUAL{Clavel99, title = {Maude: Specification and Programming in Rewriting Logic}, author = {Clavel, Manuel and Dur\'an, Francisco and Eker, Steven and Lincoln Patrick and Mart{\'\i}-Oliet, Narciso and Meseguer Jos\'e and Quesada, Jos\'e}, organization = {Computer Science Laboratory, SRI International}, month = {3}, year = {1999} } @MANUAL{Clavel05, title = {Maude Manual}, author = {Clavel, Manuel and Dur\'an, Francisco and Eker, Steven and Lincoln Patrick and Mart{\'\i}-Oliet, Narciso and Meseguer Jos\'e and Talcott, Carolyn}, organization = {Computer Science Laboratory, SRI International}, month = {4}, year = {2005}, note = {Version 2.1.1} } @ARTICLE{Clint72, author = {M. Clint and C. A. R. Hoare}, title = {Program Proving: Jumps and Functions}, journal = {Acta Informatica}, year = {1972}, pages = {214-224}, number = {1}, annote = {Sem{\^a}ntica de uma linguagem do tipo procedimental}, publisher = {Springer-Verlag} } @ARTICLE{Coelho86, author = {Coelho, H. and Pereira, L. M.}, title = {Automated reasoning in geometry theorem proving with Prolog}, journal = {Journal of Automated Reasoning}, year = {1986}, volume = {2}, pages = {329--390}, number = {4}, note = {% gramy}, file = {coelho86.pdf:/home/pedro/Actividades/Investigacao/ArqArtigos/DemGeo/coelho86.pdf:PDF}, timestamp = {2007.03.26} } @PHDTHESIS{Coen92, author = {Martin D. Coen}, title = {Interactive Program Derivation}, school = {University of Cambridge}, year = {1992}, month = {nov}, note = {Available as Computer Laboratory Technical Report 272}, keywords = {Isabelle} } @INBOOK{Cousot90, chapter = {15}, pages = {841--993}, title = {Methods and Logics for Proving Programs}, publisher = {Elsevier}, year = {1990}, author = {Patrick Cousot}, volume = {B}, series = {Handbook of Theoretical Computer Science}, address = {Amsterdam}, edition = {Second}, annote = {ucmt I-18-17}, isbn = {0-444-88074-7} } @BOOK{Crespo98, title = {Processadores de linguagens: da concep\c{c}c{\~a}o {\`a} implementa\c{c}{\~a}o}, publisher = {IST Press}, year = {1998}, author = {Rui Gustavo Crespo}, address = {Lisboa} } @BOOK{Crossley69, title = {Constructive Order Types}, publisher = {North-Holland Publishing Company}, year = {1969}, author = {John N. Crossley}, series = {Studies in Logic and The Foundations of Mathematics}, address = {Amsterdam}, annote = {Logica; Order Types} } @BOOK{Curry68, title = {Combinatory Logic}, publisher = {North-Holland Pub. Comp.}, year = {1968}, author = {Haskell B. Curry and Robert Feys}, volume = {I}, series = {Studies in Logic and the Foundations of Mathematics}, address = {Amsterdam}, edition = {2nd}, annote = {ucma - 03b/cur/v1}, keywords = {Logica combinatoria, Lambda-calculo}, language = {ingles}, lcnum = {a59-1593} } @BOOK{Curry72, title = {Combinatory Logic}, publisher = {North-Holland Pub. Comp.}, year = {1972}, author = {H. B. Curry and J. R. Hindley and J. P. Seldin}, volume = {II}, series = {Studies in Logic and the Foundations of Mathematics}, address = {Amsterdam}, edition = {2nd}, annote = {ucma-03b/cur/v.2}, isbn = {0-7204-2208-6}, keywords = {logica combinatoria; lambda-calculo}, language = {ingles} } @BOOK{Dahl72, title = {Structured Programming}, publisher = {Academic Press, Inc.}, year = {1972}, author = {O.-J. Dahl and E.W.Dijkstra and C.A.R.Hoare}, address = {24/28 Oval Road London NW1}, annote = {programa\c{c}{\~a}o estruturada} } @BOOK{vanDalen80, title = {Logic and Structure}, publisher = {Springer-Verlag}, year = {1980}, author = {Dirk van Dalen}, series = {Universitext}, annote = {ucmt 03B/DAL} } @UNPUBLISHED{Danos92, author = {Danos, Vicent and {Di~Cosmo}, Robert}, title = {Initiation to Linear Logic}, note = {http://www.dmi.ens.fr/users/dicosmo/CourseNotes/LinLog/}, year = {1992} } @BOOK{Davis89, title = {Truth, Deduction, and Computation}, publisher = {Computer Science Press}, year = {1989}, author = {Ruth E. Davis}, series = {Principles of Computer Science}, address = {New York}, annote = {ucmt 03b DAV}, isbn = {0-7167-8201-4} } @MANUAL{Dawson92, title = {ICLE - The Imperial College Logic Environment, Reference Manual}, author = {Mark Dawson}, organization = {Imperial College of Science, Technology \& Medicine}, address = {London}, year = {1992}, keywords = {ICLE} } @TECHREPORT{Dawson91, author = {Mark Dawson}, title = {Deriving Rules with the Imperial Logic Environment}, institution = {Department of Computing of the Imperial College of Science Technology and Medicine}, year = {1991}, type = {Technical Report}, number = {DOC-91-39}, address = {London}, month = {May}, keywords = {ICLE} } @BOOK{Diaconescu98, title = {{CafeOBJ} Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification}, publisher = {World Scientific}, year = {1998}, author = {Diaconescu, R{\u o}zvan and Futatsugi, Kokichi}, volume = {6}, series = {AMAST series in Computing}, annote = {Vou pedi-lo atraves da BlackWell} } @BOOK{Dijkstra76, title = {A Discipline of Programming}, publisher = {Prentice--Hall, Inc}, year = {1976}, author = {Edsger W. Dijkstra}, address = {New-Jersey}, annote = {1-electronic digital computers - programming} } @ARTICLE{Dijkstra75, author = {Edsger W. Dijkstra}, title = {Guarded Commands, Nondeterminacy and Formal Derivations of Programs}, journal = {Communications of the ACM}, year = {1975}, volume = {18}, pages = {453--457}, number = {8}, optmonth = {August} } @ARTICLE{Djoric04, author = {Djori\'c, Mirjana and Jani\v{c}i\'c, Predrag}, title = {Constructions, instructions, interactions}, journal = {Teaching Mathematics and its Applications}, year = {2004}, volume = {23}, pages = {69-88}, number = {2} } @ARTICLE{Djoric04a, author = {Djori\'c, Mirjana and Jani\v{c}i\'c, Predrag}, title = {Constructions, instructions, interactions}, journal = {Teaching Mathematics and its Applications}, year = {2004}, volume = {23}, pages = {69-88}, number = {2} } @MANUAL{Bison95, title = {Bison}, author = {Donnelly, Charles and Stallman, Richard}, organization = {Free Software Foundation}, address = {Boston, USA}, month = {November}, year = {1995}, note = {version 1.25} } @BOOK{Revesz86, title = {Introduction to Formal Languages}, publisher = {McGraw-Hill}, year = {1986}, author = {Gy~rgy E. R~v~sz}, address = {New York}, edition = {2nd} } @BOOK{Ehrig90, title = {Fundamentals of Algebraic Specification 2}, publisher = {Springer-Verlag}, year = {1990}, author = {H. Ehrig and B. Mahr}, volume = {21}, series = {EATCS - Monographs on Theoretical Computer Science}, address = {Berlin}, annote = {ucmat I-16-9}, isbn = {3-540-51799-5} } @BOOK{Ehrig85, title = {Fundamentals of Algebraic Specification 1}, publisher = {Springer-Verlag}, year = {1985}, author = {H. Ehrig and B. Mahr}, volume = {6}, series = {EATCS Monographs on Theoretical Computer Science}, address = {Berlin} } @ARTICLE{Elcock77, author = {Elcock, E. W.}, title = {Representation of knowledge in geometry machine}, journal = {Machine Intelligence}, year = {1977}, volume = {8}, pages = {11--29} } @MISC{Elo07, author = {Arpad Elo}, title = {Elo rating system}, howpublished = {http://en.wikipedia.org/wiki/Elo\_rating\_system}, owner = {pedro}, timestamp = {2007.12.12} } @MISC{Feferman94, author = {Solomon Feferman}, title = {Deciding the Undecidable: Wrestling with Hilbert's Problems.}, howpublished = {Text of inaugural lecture as the Patrick Suppes Family Professor in Humanities and Sciences, Stanford University.}, month = {May 13}, year = {1994} } @ARTICLE{Feruglio94, author = {Feruglio, {Gabriel Valiente}}, title = {Typesetting Commutative Diagrams}, journal = {TUGboat}, year = {1994}, volume = {15}, pages = {466--484}, number = {4} } @INPROCEEDINGS{Fiadeiro88, author = {Jos{\'e} Fiadeiro and Am{\'\i}lcar Sernadas}, title = {Structuring Theories on Consequence}, booktitle = {Recent Trends in Data Type Specification}, year = {1988}, editor = {D. Sannella and A. Tarlecki}, number = {332}, series = {Lecture Notes in Computer Science}, pages = {44-72}, publisher = {Springer-Verlag}, annote = {Tenho a fotocopia que pedi directamente ao primeiro autor.} } @TECHREPORT{Fisher87, author = {Michael Fisher and Howard Barringer}, title = {Program Logics - A Short Survey}, institution = {Department of Computer Science University of Manchester}, year = {1987}, type = {Technical Report Series}, number = {UMCS-86-11-1}, address = {Manchester M13 9PL, England}, annote = {Tenho fotocopia} } @BOOK{Fitting69, title = {Intuitionistic Logic, Model Theory and Forcing}, publisher = {North-Holland Publishing Company}, year = {1969}, author = {Melvin Chris Fitting}, series = {Studies in Logic and The Foundations of Mathematics}, address = {Amsterdam}, annote = {Logica; Model Theory} } @BOOK{Fonseca87, title = {Vamos trabalhar com a folha de c\'alculo}, publisher = {Projecto Minerva}, year = {1987}, author = {Fonseca, Eduarda}, address = {Lisboa}, edition = {2a ed} } @TECHREPORT{Frost93, author = {Jacob Frost}, title = {A Case Study of Co-induction in {Isabelle HOL}}, institution = {University of Cambridge, Computer Laboratory}, year = {1993}, number = {308}, month = {August}, keywords = {Isabelle} } @INPROCEEDINGS{Fuchs04, author = {Fuchs, Karl and Hohenwarter, Markus}, title = {Combination of Dynamic Geometry, Algebra and Calculus in the Software System GeoGebra}, booktitle = {Computer Algebra Systems and Dynamic Geometry Systems in Mathematics Teaching Conference 2004}, year = {2004}, pages = {128--133}, address = {Pecs, Hungary} } @BOOK{Gallier87, title = {Logic For Computer Science: Foundations of Automatic Theorem Proving}, publisher = {John Wiley \& Sons}, year = {1987}, author = {Jean H. Gallier}, series = {Computer Science and Technology Series}, address = {New York}, annote = {Automatic theorem proving; L{\'o}gica; Problemas NP-Completos} } @MISC{GEXWeb, author = {Gao, Xiao-Shan}, title = {{GEX}}, howpublished = {http://www.mmrc.iss.ac.cn/\~{}xgao/software.html} } @MISC{MMPGeometerWeb, author = {Gao, X.S. and Lin, Q.}, title = {{MMP/G}eometer}, howpublished = {http://www.mmrc.iss.ac.cn/\~{}xgao/software.html} } @ARTICLE{Gao04, author = {Gao, Xiao-Shan and Lin, Qiang}, title = {{MMP/G}eometer - A Software Package for Automated Geometric Reasoning}, journal = {Lecture Notes in Computer Science}, year = {2004}, volume = {2930}, pages = {44--66}, comment = {4th International Workshop, ADG 2002, Hagenberg Castle, Austria, September 4-6, 2002. Revised Papers}, owner = {pedro}, timestamp = {2007.05.18} } @INPROCEEDINGS{Gelertner59, author = {Gelernter, H.}, title = {Realization of a geometry theorem proving machine}, booktitle = {Proceedings of the International Conference Information Processing}, year = {1959}, pages = {273--282}, address = {Paris}, month = {June 15-20}, note = {%gramy} } @BOOK{Girard87, title = {Proof Theory and Logical Complexity}, publisher = {Bibliopolis}, year = {1987}, author = {Jean-Yves Girard}, volume = {1}, series = {Studies in Proof Theory}, address = {Napoli}, annote = {ucmat 03F/GIR}, isbn = {0-444-98715-0}, keywords = {L{\'o}gica, Teoria da Prova}, language = {ingl{\^e}s} } @BOOK{Girard88, title = {Proofs and Types}, publisher = {Cambridge University Press}, year = {1988}, author = {Jean-Yves Girard and P. Taylor and Y. Lafont}, annote = {Tenho fotocopias} } @MISC{glicko07, author = {Mark E. Glickman}, title = {Glicko ratings}, howpublished = {http://math.bu.edu/people/mg/glicko/}, owner = {pedro}, timestamp = {2007.12.12} } @INBOOK{Goguen91, chapter = {14 - Types as theories}, pages = {357--390}, title = {Topology and Category Theory in Computer Science}, publisher = {Oxford University Press}, year = {1991}, editor = {G. M. Reed, A. W. Roscoe and R.F. Watcher}, author = {Joseph Goguen}, series = {Oxford Science Publications}, address = {Oxford}, annote = {ucmt I-18-13}, isbn = {0-19-853760-3}, keywords = {Computer Science; Topology; Categories.} } @INPROCEEDINGS{Goguen90, author = {Joseph Goguen}, title = {Proving and Rewriting}, booktitle = {Proceedings 2nd International Conference on Algebraic and Logic Programming}, year = {1990}, address = {Nancy, France}, month = {October}, annote = {Est{\~a}p na documenta\c{c}{\~a}o do 2OBJ/OBJ3}, keywords = {OBJ} } @TECHREPORT{Goguen88, author = {Joseph Goguen}, title = {OBJ as Theorem Prover with Applications to Hardware Verification}, institution = {SRI International}, year = {1988}, number = {SRI-CSL-88-4R2}, month = {August}, annote = {Est{\'a} na documenta\c{c}{\~a}o do 2OBJ/OBJ3}, keywords = {OBJ} } @ARTICLE{Goguen92a, author = {Joseph Goguen and Rod Burstall}, title = {Institutions: Abstract Model Theory for Specification and Programming}, journal = {Journal of the Association for Computing Machinery}, year = {1992}, volume = {39}, pages = {95--146}, number = {1}, month = {January}, annote = {ciuc}, language = {Ingl{\^e}s} } @INBOOK{Goguen85, pages = {313--333}, title = {A Study in the Foundations of Programming Methodology: Specifications, Institutions, Charters and Parchments}, publisher = {Springer-Verlag}, year = {1985}, author = {Joseph Goguen and Rod Burstall}, volume = {240}, series = {Lecture Notes in Computer Science}, annote = {(ucmt XXII-3)} } @ARTICLE{Goguen84a, author = {Joseph Goguen and Rod Burstall}, title = {Some Fundamental Algebraic Tools for the Semantics of Computation, Part 1: Comma Categories, Colimits, Signatures and Theories}, journal = {Theoretical Computer Science}, year = {1984}, volume = {31}, pages = {175-209}, number = {2}, annote = {Tenho a fotocopia do artigo.} } @ARTICLE{Goguen84b, author = {Joseph Goguen and Rod Burstall}, title = {Some Fundamental Algebraic Tools for the Semantics of Computation, Part 2: Signed and Abstract Theories}, journal = {Theoretical Computer Science}, year = {1984}, volume = {31}, pages = {263--295}, number = {3}, annote = {Tenho as fotocopias do artigo. Obtive-as por pedido ao Centro de Informatica da Univ. do Porto.} } @TECHREPORT{Goguen88a, author = {Joseph Goguen and Timothy Winkler}, title = {Introducing {OBJ}}, institution = {SRI International, Computer Science Lab}, year = {1988}, type = {Technical Report}, number = {SRI-CSL-88-9}, month = {August}, annote = {Nao tenho esta referencia. E' importante so' por causa da data.} } @TECHREPORT{Goguen92, author = {Joseph Goguen and Timothy Winkler and Jos{\'e} Meseguer and Kokichi Futatsugi and Jean-Pierre Jouannaud}, title = {Introducing {OBJ}}, institution = {SRI International}, year = {1992}, type = {Technical Report}, number = {SRI-CSL-92-03}, month = {March}, note = {Draft} } @TECHREPORT{Goldstein73, author = {Goldstein, Ira}, title = {Elementary {G}eometry {T}heorem {P}roving}, institution = {MIT}, year = {1973}, type = {AI Lab memo}, number = {280}, month = {April}, file = {AIM-280.pdf:/home/pedro/Actividades/Investigacao/ArqArtigos/DemGeo/AIM-280.pdf:PDF}, owner = {pedro}, timestamp = {2007.04.05} } @BOOK{Goossens97, title = {The \LaTeX Graphics Companion}, publisher = {Addison-Wesley}, year = {1997}, author = {Goossens, Michel and Rahtz, Sebastian and Mittelbach, Frank}, address = {Reading}, isbn = {0-201-85469-4} } @BOOK{Gordon79, title = {Edinburgh LCF}, publisher = {Springer-Verlag}, year = {1979}, author = {Michael J. Gordon and Arthur J. Milner and Cristopher P. Wadsworth}, volume = {78}, series = {Lecture Notes in Computer Science}, address = {Berlin}, annote = {Demonstra\c{c}{\~a}o Autom{\'a}tica de Teoremas, Standard ML, tacticas, tacticais.} } @BOOK{Byron94, title = {Programa{\c c}{\~a}o em Pascal}, publisher = {McGraw-Hill}, year = {1994}, author = {Gottfired, Byron}, address = {Lisboa}, edition = {2nd} } @ARTICLE{Greeno79, author = {Greeno, J.G. and Magone, M. E. and Chaiklin, S.}, title = {Theory of constructions and set in problem solving}, journal = {Memory and Cognition}, year = {1979}, volume = {7}, pages = {445--461}, number = {6}, note = {% gramy} } @BOOK{Gries81, title = {The Science of Programming}, publisher = {Springer-Verlag}, year = {1981}, author = {David Gries}, address = {New York}, annote = {ucmt I-12-16} } @TECHREPORT{Girard00, author = {Grirard, Jean-Yves}, title = {Linear Logic: Its syntax and Semantics}, institution = {Laboratoire de Mathem{\'}atiques Discr{\'e}tes}, year = {2000}, number = {LMSLNS222}, note = {Obtido por via electronica} } @BOOK{Hahn93, title = {LaTeX for everyone}, publisher = {Prentice-Hall}, year = {1993}, author = {Jane Hahn}, address = {New Jersey}, annote = {ucdee}, isbn = {0-13-605908-2} } @BOOK{Hamilton88, title = {Logic for Mathematicians}, publisher = {Cambridge University Press}, year = {1991}, author = {A. G. Hamilton}, isbn = {0-521-36865-0} } @MANUAL{Haskell97b, title = {Standard Libraries for the Haskell Programming Language}, author = {Hammond, Kevin and Peterson, John and Augustsson, Lennart and Fasel, Joseph and Gordon, Andrew and Peyton-Jones, Simon and Reid, Alastair}, edition = {Version 1.4}, month = {April 6}, year = {1997} } @BOOK{Harary72, title = {Graph Theory}, publisher = {Addison-Wesley}, year = {1972}, author = {Harary, Frank}, address = {Reading, Massachusetts} } @MANUAL{Harper86, title = {Introduction to Standard ML}, author = {Robert Harper}, organization = {University of Edinburgh}, year = {1986}, annote = {Standard ML, linguagem funcional com tipos.} } @ARTICLE{Harper93, author = {Robert Harper and Furio Honsell and Gordon Plotkin}, title = {A Framework for Defining Logics}, journal = {Journal of the Association for Computing Machinery}, year = {1993}, volume = {40}, pages = {143--184}, number = {1}, month = {January}, key = {Harper93} } @TECHREPORT{Harper92, author = {Robert Harper and Frank Pfenning}, title = {A Module System for a Programming Language Based on the {LF} Logical Framework}, institution = {Carnegie Mellon University}, year = {1992}, number = {CMU-CS-92-191}, address = {Pittsburgh, Pennsylvania}, month = {September}, key = {Harper92} } @BOOK{Heijenoort67, title = {From Frege to G{\"o}del. A Source Book in Mathematical Logic, 1879--1931}, publisher = {Harvard University Press}, year = {1967}, author = {Jean van Heijenoort}, series = {Source Books in the History of the Sciences}, address = {Cambridge, Massachusetts}, keywords = {Logic}, language = {english}, lcnum = {67-10905} } @BOOK{Helman86, title = {Intermediate problem solving and data structures : walls and mirrors}, publisher = {The Benjamin/Cummings}, year = {1986}, author = {Helman, Paul and Veroff, Robert}, address = {Menlo Park, California} } @INBOOK{Herbrand30, pages = {525--581}, title = {Investigations in proof thoery: The properties of true propositions}, publisher = {Harvard University Press}, year = {1967}, author = {J. Herbrand}, volume = {From Frege to G{\"o}del: A Source Book in Mathematical Logic, 1879-1931}, address = {Cambridge, Massachusetts}, language = {english} } @BOOK{Herrlich73, title = {Category Theory}, publisher = {Allyn and Bacon Inc.}, year = {1973}, author = {Horst Herrlich and George Strecker}, annote = {Tenho fotocopias}, lcnum = {78-182352} } @ARTICLE{Heuerding96, author = {Alain Heuerding and Gerhard J{\"a}ger and Stefan Schwendimann and Michael Seyfried}, title = {The Logics Workbench LWB: A Snapshot}, journal = {Euromath Bulletin}, year = {1996}, volume = {1}, pages = {177--186}, number = {2}, annote = {pedro, ap{\^e}ndice 1} } @BOOK{Heyting71, title = {Intuitionism, An Introduction --- Third Revised Edition}, publisher = {North-Holland Publishing Company}, year = {1971}, author = {A. Heyting}, series = {Studies in Logig and The Foundations of Mathematics}, address = {Amsterdam}, edition = {3}, annote = {L{\'o}gica; Intuicionismo} } @BOOK{Heyting56, title = {Intuitionism, An Introduction}, publisher = {North-Holland Publishing Co.}, year = {1956}, author = {A. Heyting}, series = {Studies in Logic, and The Foundations of Mathematics}, address = {Amsterdam}, annote = {Logica, Intuicionismo, Construtivismo} } @BOOK{Hilbert03, title = {Fundamentos da Geometria}, publisher = {Gradiva}, year = {2003}, editor = {A.J. Franco de Oliveira}, author = {David Hilbert}, address = {Lisboa} } @ARTICLE{Hindley69, author = {R. Hindley}, title = {The Principal Type-Scheme of an Object in Combinatory Logic}, journal = {Transaction of the American Mathematical Society}, year = {1969}, volume = {146}, pages = {29--60}, month = {December}, keywords = {Lambda Calculus com Tipos, Hindley-Milner tipos.} } @MISC{Hinsolt96, author = {Hinsolt, Michael}, title = {The GML File Format}, howpublished = {URL:http://infosun.fmi-passau.de/Graphlet/GML/}, year = {1996} } @INBOOK{Hoare89, pages = {245--305}, title = {Notes on an Approach to Category Theory for Computer Scientists}, publisher = {Springer-Verlag}, year = {1989}, author = {C. A. R. Hoare}, volume = {55}, series = {F:Computer and Systems Sciences}, address = {Berlin}, annote = {teoria das categorias, preordens, monoides} } @ARTICLE{Hoare87, author = {C. A. R. Hoare}, title = {An Overview of Some Formal Methods for Program Design}, journal = {Computer}, year = {1987}, volume = {20}, pages = {85 -- 91}, number = {9}, month = {September}, annote = {ciuc} } @ARTICLE{Hoare73, author = {C. A. R. Hoare}, title = {An Axiomatic Definition of the Programming Language PASCAL}, journal = {Acta Informatica}, year = {1973}, volume = {2}, pages = {335--355}, annote = {Sem{\^a}ntica de uma linguagem procedimental}, publisher = {Springer-Verlag} } @ARTICLE{Hoare72, author = {C. A. R. Hoare}, title = {Proof of Correctness of Data Representations}, journal = {Acta Informatica}, year = {1972}, volume = {1}, pages = {271-281}, note = {Springer-Verlag}, annote = {Observat{\'o}rio Astron{\'o}mico de Coimbra} } @ARTICLE{Hoare71, author = {C. A. R. Hoare}, title = {Procedures and Parameters: An Axiomatic Approach}, journal = {Lecture Notes in Mathematics}, year = {1971}, volume = {188}, pages = {102--106}, annote = {Sem{\^a}ntica de uma linguagem procedimental}, publisher = {Springer} } @ARTICLE{Hoare69, author = {C. A. R. Hoare}, title = {An Axiomatic Basis for Computer Programming}, journal = {Communications of the ACM}, year = {1969}, volume = {12}, pages = {576--580,583}, number = {10}, month = {October}, annote = {ciuc} } @BOOK{Hodges93, title = {Model Theory}, publisher = {Cambridge University Press}, year = {1993}, author = {Wilfrid Hodges}, volume = {42}, series = {Encyclopedia of Mathematics and its Applications}, address = {Cambridge}, annote = {ucmt 03C-HOD-ex2}, isbn = {0-521-30442-3} } @BOOK{Horowitz87, title = {Fundamentals of Data Structures in Pascal}, publisher = {Computer Science Press}, year = {1987}, author = {Horowitz, Ellis and Sahni, Sartaj} } @INPROCEEDINGS{Howard80, author = {W. A. Howard}, title = {The formulae-as-types notion of construction}, booktitle = {To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism}, year = {1980}, editor = {J. R. Hindley and J. P. Seldin}, publisher = {Academic Press}, annote = {Nao tenho este livro!} } @ARTICLE{Hsiang87, author = {Jieh Hsiang}, title = {Rewrite Method for Theorem Proving in First Order Theory with Equality}, journal = {Journal of Symbolic Computation}, year = {1987}, pages = {133-151}, number = {3} } @INPROCEEDINGS{Huang94, author = {X. Huang and M. Kerber and M. Kohlhase and E. Melis and D. Nesmith and J. Richts and J. Siekmann}, title = {KEIM: A Toolkit for Automated Deduction}, booktitle = {Proceedings of CADE12}, year = {1994}, annote = {pedro, Keim} } @BOOK{Hudak2000, title = {The Haskell School of Expression}, publisher = {Cambridge University Press}, year = {2000}, author = {Paul Hudak} } @TECHREPORT{Hudak97, author = {Hudak, Paul and Peterson, John and Fasel, Joseph}, title = {A Gentle Introduction to Haskell, Version 1.4}, institution = {Yale University and Univeristy of California}, year = {1997}, month = {March} } @MANUAL{Jackiw01, title = {The Geometer's Sketchpad v4.0}, author = {Jackiw, Nicholas}, organization = {Emeryville: Key Curriculum Press}, year = {2001}, owner = {pedro}, timestamp = {2007.05.18} } @INPROCEEDINGS{Janicic03, author = {Jani\v{c}i\'c, Predrag and Trajkovi\'c, Ivan}, title = {WinGCLC --- a Workbench for Formally Describing Figures}, booktitle = {Proceedings of the 18th Spring Conference on Computer Graphics (SCCG 2003)}, year = {2003}, pages = {251--256}, month = {April, 24-26}, publisher = {ACM Press, New York, USA} } @INPROCEEDINGS{Janicic03a, author = {Jani\v{c}i\'c, Predrag and Trajkovi\'c, Ivan}, title = {WinGCLC --- a Workbench for Formally Describing Figures}, booktitle = {Proceedings of the 18th Spring Conference on Computer Graphics (SCCG 2003)}, year = {2003}, pages = {251--256}, address = {Budmerice, Slovakia}, publisher = {ACM Press, New York, USA} } @INPROCEEDINGS{Janicic06b, author = {Jani{\v c}i{\' c}, Predrag and Quaresma, Pedro}, title = {Automatic Verification of Regular Constructions in Dynamic Geometry Systems}, booktitle = {Automated Deduction in Geometry}, year = {2007}, number = {4869}, series = {LNAI}, pages = {39--51}, address = {Berlin / Heidelberg}, publisher = {Springer}, note = {6th International Workshop, ADG 2006, Pontevedra, Spain, August 31-September 2, 2006. Revised Papers} } @ARTICLE{Janicic06c, author = {Predrag Jani{\v c}i{\'c}}, title = {{GCLC} --- A Tool for Constructive Euclidean Geometry and More Than That}, journal = {Lecture Notes in Computer Science}, year = {2006}, volume = {4151}, pages = {58--73}, comment = {Mathematical Software - ICMS 2006}, owner = {pedro}, timestamp = {2007.05.18} } @UNPUBLISHED{Janicic06x, author = {Jani{\v c}i{\'c}, Predrag}, title = {GCLC 5.0/WinGCLC 2006}, note = {Manual for the GCLC Dynamic Geometry Software}, year = {2006}, owner = {pedro}, timestamp = {2006.11.24} } @ARTICLE{Janicic02, author = {Jani{\v c}i{\'c}, Predrag and Bundy, Alan}, title = {A General Setting for Flexibly Combining and Augmenting Decision Procedures}, journal = {Journal of Automated Reasoning}, year = {2002}, volume = {28}, pages = {257-305}, number = {3}, note = {% tenho o artigo} } @MANUAL{Hugs97, title = {Hugs 1.4}, author = {Jones, Mark and Peterson, John}, month = {April}, year = {1997} } @ARTICLE{Phipps86, author = {Thomas E. Phipps Jr.}, title = {The Inversion of Large Matrices}, journal = {Byte}, year = {1986}, pages = {181 -- 188}, month = {April}, annote = {Interessante. N{\~a}o chegou a ser utilizado.} } @TECHREPORT{Kalvala94, author = {Sara Kalvala}, title = {A Gentle Introduction to Isabelle}, institution = {University of Cambridge, Computer Laboratoty}, year = {1994} } @ARTICLE{Kapur86, author = {Kapur, D.}, title = {Using Gr\"obner bases to reason about geometry problems}, journal = {Journal of Symbolic Computation}, year = {1986}, volume = {2}, pages = {399--408}, number = {4}, note = {% gramy} } @BOOK{Keisler71, title = {Model Theory for Infinitary Logic}, publisher = {North-Holland Publishing Company}, year = {1971}, author = {H. J. Keisler}, volume = {62}, series = {Studies in Logic and The Foundations of Mathematics}, address = {Amsterdam}, annote = {Logica; Model Theory} } @INBOOK{Kleene52, chapter = {-}, pages = {-}, title = {Permutability of Inferences in Gentzen's Calculi LK and LJ}, publisher = {unknown}, year = {1952}, editor = {-}, author = {S. C. Kleene}, annote = {ucmat A-6-11} } @BOOK{Kleene52a, title = {Introduction to Metamathematics}, publisher = {North-Holland Publishing Co.}, year = {1952}, author = {Stephen Cole Kleene}, volume = {I}, series = {Bibliotheca Mathematica, A serie of Monographs on Pure and Applied Mathematics}, address = {Amsterdam}, annote = {Intuicionismo, L{\'o}gica, Fun\c{c}{\~o}es Recursivas Fun\c{c}{\~o}es Comput{\'a}veis} } @BOOK{Kleene65, title = {The Foundations of Intuitionistic Mathematics}, publisher = {North-Holland Publishing Co.}, year = {1965}, author = {S. C. Kleene and R. E. Vesley}, series = {Studies in Logic, and The Foundations of Mathematics}, address = {Amsterdam}, annote = {Logica, Intuicionismo, Construtivismo} } @BOOK{Kneale91, title = {O Desenvolvimento da L{\'o}gica}, publisher = {Funda\c{c}{\~a}o Calouste Gulbenkian --- Servi\c{c}o de Educa\c{c}{\~a}o}, year = {1991}, author = {William Kneale and Martha Kneale}, address = {Lisboa}, edition = {3}, annote = {Tradu\c{c}{\~a}o de: The Development of Logic, W.Kneale and M.Kneale, The Claredon Press, Oxford, 1962. L{\'o}gica} } @BOOK{Knuth86, title = {The {\TeX}book}, publisher = {Addison-Wesley Publishing Company}, year = {1986}, author = {Donald E. Knuth}, address = {Reading, Massachusetts}, annote = {TeX} } @BOOK{knuth81, title = {The Art of Computer Programming}, publisher = {Addisson-Wesley Publishing Company}, year = {1981}, author = {Knuth, Donald E.}, volume = {2, Seminumerical algorithms}, address = {Reading, USA}, edition = {2nd} } @BOOK{Knuth73, title = {The Art of Computer Programming}, publisher = {Addisson-Wesley Publishing Company}, year = {1973}, author = {Knuth, Donald E.}, volume = {1, Fundamental Algorithms}, address = {Reading, USA}, edition = {2nd} } @ARTICLE{Kock77, author = {A. Kock and G. E. Reyes}, title = {Doctrines in Categorical Logic}, journal = {Handbook of Mathematical Logic -- Studies in Logic and the Foundations of Mathematics}, year = {1977}, volume = {90}, pages = {283 -- 313} } @MISC{Kohlhase96, author = {Michael Kohlhase and Carolyn Talcott}, title = {Mechanized Reasoning}, howpublished = {http://www-formal.stanford.edu/clt/ARS/ars-db.html} } @MISC{Kohlhase98, author = {Michael Kohlhase and Carolyn Talcott}, title = {Mechanized Reasoning Systems}, howpublished = {http://www-formal.stanford.edu/clt/ARS/ars-db.html}, year = {1998}, annote = {http://www-formal.stanford.edu/clt/ARS/systems.html} } @INPROCEEDINGS{Kolyang96, author = {Kolyang and T. Santen and B. Wolff}, title = {A Structure Preserving Encoding of Z in Isabelle/HOL}, booktitle = {Theorem Proving in Higher Order Logics --- 9th International Conference}, year = {1996}, editor = {J. von Wright and J. Grundy and J. Harrison}, number = {1125}, series = {LNCS}, pages = {283--298}, publisher = {Springer Verlag}, annote = {tenho o artigo que obtive a partir da pagina da Web}, language = {english} } @INPROCEEDINGS{Kortenkamp04, author = {Kortenkamp, Ulrich and Richter-Gebert, J{\"u}rgen}, title = {Using Automatic Theorem Proving to Improve the Usability of Geometry Software}, booktitle = {Procedings of the Mathematical User-Interfaces Workshop 2004}, year = {2004} } @ARTICLE{Kozen2000, author = {Kozen, Dexter}, title = {On Hoare Logic and Kleene Algebra with Tests}, journal = {ACM Transactions on Computational Logic}, year = {2000}, note = {Obtido por via electr{\'o}nica do arquivo http://www.acm.org/tocl/} } @BOOK{Kuratowski72, title = {Introduction to Set Theory and Topology}, publisher = {Pergamon Press}, year = {1972}, author = {Kazimierz Kuratowski}, volume = {101}, series = {Pure and Applied Mathematics}, address = {Warszawa}, annote = {ucma D.06.01}, lcnum = {72-149123} } @BOOK{Kuratowski76, title = {Set Theory}, publisher = {North-Holland Publishing Company}, year = {1976}, author = {K. Kuratowski and A. Mostowski}, volume = {86}, series = {Studies in Logic and the Foundations of Mathematics}, address = {Amsterdam}, annote = {ucma B.03.41}, isbn = {0 7204 0470 3}, lcnum = {74 83731} } @ARTICLE{Laborde90, author = {Laborde, J. M. and Str{\"a}sser, R.}, title = {Cabri-G{{\'e}}om{{\`e}}tre: A microworld of geometry guided discovery learning}, journal = {International reviews on mathematical education- Zentralblatt fuer didaktik der mathematik}, year = {1990}, volume = {90}, pages = {171--177}, number = {5}, owner = {pedro}, timestamp = {2007.05.18} } @INBOOK{Lambek75, pages = {-}, title = {On the unity of Algebra and Logic}, publisher = {Springer-Verlag}, year = {1975}, editor = {F. Borceaux}, author = {Joachim Lambek}, series = {Lectures Notes in Mathematics} } @BOOKLET{Lambek93, title = {What is a deductive system}, author = {J. Lambek}, howpublished = {TEMPUS Summer School 1993 -- Algebraic and Categorical Methods in Computer Science}, address = {Brno, Czech Republic}, year = {1993} } @ARTICLE{Lambek71, author = {Joachim Lambek}, title = {Deductive Systems and Categories {III}}, journal = {Lecture Notes in Mathematics}, year = {1971}, pages = {57 -- 82}, number = {274}, annote = {Cartesian Closed Categories; Intuitionist Propositional Calculus; Combinatory Logic} } @ARTICLE{Lambek69, author = {Joachim Lambek}, title = {Deductive Systems and Categories {II}}, journal = {Lecture Notes in Mathematics}, year = {1969}, pages = {76-122}, number = {86}, annote = {Standard Constructions and Closed Categories} } @ARTICLE{Lambek58, author = {Joachim Lambek}, title = {Deductive Systems and Categories {I}}, journal = {Mathematical Systems Theory}, year = {1958}, volume = {2}, pages = {287 -- 318}, number = {4}, annote = {Syntatic Calculus and Residuated Categories} } @BOOK{Lambek88, title = {Introduction to Higher Order Categorical Logic}, publisher = {Cambridge University Press}, year = {1988}, author = {Joachim Lambek and P. J. Scott}, series = {Cambridge Studies in Advanced Mathematics}, address = {Cambridge}, annote = {Categorias, Logica} } @BOOK{Lamport94, title = {{\LaTeX}: A Document Preparation System}, publisher = {Addison-Wesley Publishing Company}, year = {1994}, author = {Leslie Lamport}, address = {Reading,Massachusetts}, edition = {2nd}, annote = {TeX, LaTeX} } @BOOK{Lamport86, title = {{\LaTeX}: A Document Preparation System}, publisher = {Addison-Wesley Publishing Company}, year = {1986}, author = {Leslie Lamport}, address = {Reading,Massachusetts}, month = {9}, annote = {TeX, LaTeX} } @BOOK{Lesser87, title = {Programa{{\c c}}{{\~a}}o em Logo}, publisher = {Editorial Presen{{\c c}}a, Lda}, year = {1987}, author = {Lesser, Martin}, address = {Lisboa} } @INPROCEEDINGS{Lester94, author = {D. Lester and S. Mintchev}, title = {Towards Machine-Checked Compiler Correctness for Higher-Order Languages}, booktitle = {{CSL} '94}, year = {1994}, organization = {European Association for Computer Science Logic}, publisher = {Springer LNCS, in press}, keywords = {Isabelle} } @INPROCEEDINGS{Li00, author = {Li, H.}, title = {Clifford algebra approaches to mechanical geometry theorem proving}, booktitle = {Mathematics Mechanization and Applications}, year = {2000}, editor = {Gao, X.-S. and Wang, D.}, pages = {205--299}, address = {San Diego, CA}, publisher = {Academic Press}, note = {% gramy} } @INPROCEEDINGS{Liang06, author = {Tielin Liang and Dongming Wang}, title = {Geometric Constraint Handling in {GOOL}}, booktitle = {Automated Deduction in Geometry}, year = {2006}, pages = {66--73}, owner = {pedro}, timestamp = {2007.05.21} } @BOOK{Lippman98, title = {C++ Primer}, publisher = {Addison-Wesley}, year = {1998}, author = {Lippman, Stanley B. and Lajoie, Jos{{\'e}}}, edition = {3rd Edition}, note = {DEPMAT 68N/LIP} } @BOOK{Lipson81, title = {Elements of Algebra and Algebra Computing}, publisher = {Addison--Wesley}, year = {1981}, author = {John D. Lipson}, annote = {1 - algebra; 2 - algebra-data processing} } @BOOK{Lloyd87, title = {Foundations of Logic Programming}, publisher = {Springer-Verlag}, year = {1987}, author = {J. W. Lloyd}, address = {Berlin}, annote = {Prolog; L{\'o}gica} } @BOOK{Loeckx72, title = {Computability and Decidability, An introduction for students of Computer Science}, publisher = {Springer-Verlag}, year = {1972}, author = {J. Loeckx}, volume = {68}, series = {Lectures ANNOTEs in Economics and Mathematical Systems}, address = {Berlin} } @BOOK{Spivak86, title = {The Joy of TeX}, publisher = {American Mathematical Society}, year = {1986}, author = {M.D.Spivak}, address = {Providence, Rhode Island}, annote = {TeX, AMSTeX} } @ARTICLE{Machiavelo04, author = {Machiavelo, Ant\'onio}, title = {O que vem \`a rede \dots}, journal = {Gazeta de Matem\'atica}, year = {2004}, pages = {14-15}, number = {147}, month = {Julho} } @BOOK{MacLane71, title = {Categories for the Working Mathematician}, publisher = {Springer-Verlag}, year = {1971}, author = {S. MacLane}, address = {New York}, annote = {Teoria das Categorias} } @BOOK{Main97, title = {Data Structures and other Objects Using C++}, publisher = {Addison-Wesley}, year = {1997}, author = {Main, Michael and Savitch, Walter}, note = {DMAT 68P/MAI} } @BOOK{Malitz79, title = {Introduction to Mathematical Logic}, publisher = {Springer-Verlag}, year = {1979}, author = {J. Malitz}, address = {New-York}, annote = {Logic, Symbolic and Mathematical} } @INPROCEEDINGS{Maric04a, author = {Mari{\'c}, Filip and Jani{\v c}i{\'c}, Predrag}, title = {SMT-LIB in XML clothes}, booktitle = {Proceedings of the 2nd Workshop on Pragmatics of Decision Procedures in Automated Reasoning}, year = {2004}, organization = {PDPAR 2004}, note = {%tenho o artigo} } @INPROCEEDINGS{Maric04aa, author = {Mari{\'c}, Filip and Jani{\v c}i{\'c}, Predrag}, title = {ARGO-LIB: A Generic Platform for Decision Procedures}, booktitle = {Lecture Notes in Artificial Intelligence}, year = {2004}, volume = {3097}, pages = {213-217}, organization = {IJCAR-04}, publisher = {Springer} } @MASTERSTHESIS{Gomes89, author = {Martinez Gomes, Teresa}, title = {M{\'e}todos de Simula\c{c}{\~a}o de Teletr{\'a}fego (an{\'a}lise da precis{\~a}o dos resultados)}, school = {Departamento de Engenharia Electrot{\'e}cnica da U.C.}, year = {1989} } @MISC{Martins88, author = {Martins, Maria Teresa}, howpublished = {Apontamentos de um Curso}, month = {Abril}, year = {1988}, annote = {Teoria das Categorias} } @TECHREPORT{Mason87, author = {Ian A. Mason}, title = {Hoare's Logic in the LF}, institution = {Laboratory for Foundations of Computer Science, Department of Computer Science - University of Edinburgh}, year = {1987}, type = {LCFS Report Series}, number = {ECS-LFCS-87-32}, month = {june} } @BOOK{Mason91, title = {lex \& yacc}, publisher = {0'Reily \& Associates}, year = {1991}, author = {Tony Mason and Doug Brown}, address = {Sebastopol (USA)}, edition = {2nd} } @ARTICLE{Matsuda04, author = {Matsuda, Noboru and Vanlehn, Kurt}, title = {GRAMY: A Geometry Theorem Prover Capable of Construction}, journal = {Journal of Automated Reasoning}, year = {2004}, volume = {32}, pages = {3--33} } @MANUAL{Merill04, title = {MERILL, An Equational Reasoning System in Standard ML, A User Guide}, author = {Brian Mattews}, organization = {Software Engineering Group, Informatics Department Rutherford Appleton Laboratory}, month = {October}, year = {1996}, annote = {fui buscar em ftp.dcs.gla.ac.uk/pub/merill}, keywords = {MERILL} } @MANUAL{McCombs03, title = {Maude 2.0 Primer}, author = {Theodore McCombs}, edition = {ver. 1.0}, month = {8}, year = {2003} } @BOOK{McConnell01, title = {Analysis of algorithms : an active learning approach}, publisher = {Jones and Bartlett}, year = {2001}, author = {McConnell, Jeffrey J.}, address = {Sudbury, Massachusetts} } @BOOK{Mendelson64, title = {Introduction to Mathematical Logic}, publisher = {D. Van Nostrand Company, Inc.}, year = {1968}, author = {Elliott Mendelson}, address = {Princeton}, annote = {ucmt A-01-34} } @BOOK{Mendes05, title = {Prepara{\c c}{\~a}o de Textos Cient{\'\i}ficos Usando {\LaTeX}}, publisher = {Edi{\c c}{\~o}es S{\'\i}labo}, year = {2005}, author = {Mendes, Mateus and Almeida, Jorge}, owner = {pedro}, timestamp = {2007.08.16} } @BOOK{Menezes01, title = {Handbook of Applied Cryptography}, publisher = {CRC Press}, year = {2001}, author = {Menezes, Alfred J. and {van}~Oorschot, Paul C. and Vanstone, Scott A.}, edition = {5th}, optnumber = {6}, optseries = {Series: Discrete Mathematics and Its Applications} } @INPROCEEDINGS{Meseguer89, author = {Meseguer, Jos{\'e}}, title = {General Logics}, booktitle = {Logic Colloquium'87}, year = {1989}, editor = {H.D. Ebbinghaus et. al.}, pages = {275--329}, address = {North-Holland}, publisher = {Elsevier Science Publishers B.V.} } @ARTICLE{Meseguer93, author = {Jos{\'e} Meseguer and Joseph A. Goguen}, title = {Order-Sorted Algebre Solves the Constructor-Selector, Multiple Representation, and Coercion Problems}, journal = {Information and Computation}, year = {1993}, volume = {103}, pages = {114--158}, number = {1}, month = {March}, note = {Academic Press, Inc., San Diego}, annote = {ISSN 0890-5401} } @BOOK{Meyer90, title = {Introduction to the Theory of Programming Languages}, publisher = {Prentice Hall International}, year = {1990}, author = {B. Meyer}, address = {New York} } @BOOK{Meyer88, title = {Object-Oriented Software Construction}, publisher = {Prentice-Hall International}, year = {1988}, author = {Meyer, Bertrand}, note = {DMAT 68N/MEY; Programa\c{c}{\~a}o Orientada para Objectos} } @INPROCEEDINGS{Michaylov91, author = {Spiro Michaylov and Frank Pfenning}, title = {Natural Semantics and Some of its Meta-Theory in {Elf}}, booktitle = {Proceedings of the Second International Workshop on Extensions of Logic Programming}, year = {1991}, editor = {L.-H. Eriksson and L. Halln\u{a}s and P. Schroeder-Heister}, pages = {299--344}, address = {Stockholm, Sweden}, month = {January}, publisher = {Springer-Verlag LNAI 596}, key = {Michaylov91} } @BOOK{Mitchel65, title = {Theory of Categories}, publisher = {Academic Press}, year = {1965}, author = {Barry Mitchel}, series = {Pure and Applied Mathematics}, address = {New York}, annote = {Teoria das Categorias} } @ARTICLE{Murty71, author = {Katta G. Murty}, title = {Solving the Fixed Charge Problem by Ranking the Extremes Points}, journal = {Operations Research}, year = {1971}, volume = {19}, pages = {1529 -- 1538} } @INPROCEEDINGS{Mery92, author = {D. {M{\'e}ry} and A. Mokkedem}, title = {Crocos: an Integrated Environment for Interactive Verification of {SDL} Specifications}, booktitle = {Computer Aided Verification: Fourth International Workshop, {CAV} '92}, year = {1993}, editor = {G. v. Bochmann and D. K. Probst}, publisher = {Springer-Verlag LNCS 663}, keywords = {Isabelle} } @INPROCEEDINGS{Mery91a, author = {D. {M{\'e}ry} and A. Mokkedem}, title = {A Proof Environment for a Subset of {SDL}}, booktitle = {Fifth {SDL} Forum Evolving Methods}, year = {1991}, editor = {O. Faergemand and R. Reed}, publisher = {North-Holland}, keywords = {Isabelle} } @INPROCEEDINGS{Mery91b, author = {D. {M{\'e}ry} and A. Mokkedem}, title = {Demonstration of {Crocos}}, booktitle = {Fifth {SDL} Forum Evolving Methods}, year = {1991}, editor = {O. Faergemand and R. Reed}, publisher = {North-Holland}, keywords = {Isabelle} } @MANUAL{Nakagawa99, title = {CafeOBJ User's Manual, ver. 1.3}, author = {Ataru Nakagawa and Toshimi Sawada and Kokichi Futatsugi}, year = {1999} } @MANUAL{Nakagawa00, title = {CafeOBJ User{\'{}}s Manual, ver1.4}, author = {Nakagawa, Ataru T. and Sawada, Toshimi and Futatsugi, Kokichi}, year = {2000}, annote = {Documento "postscript" obtido a partir da "internet"} } @INPROCEEDINGS{Narboux06c, author = {Julien Narboux}, title = {Mechanical Theorem Proving in {T}arski's geometry}, booktitle = {Proceedings of Automatic Deduction in Geometry 06}, year = {2006}, owner = {pedro}, timestamp = {2007.05.07} } @ARTICLE{Narboux04, author = {Narboux, Julien}, title = {A Decision Procedure for Geometry in {C}oq}, journal = {Lecture Notes in Computer Science}, year = {2004}, volume = {3223}, pages = {225--240}, comment = {Proceedings TPHOLS 2004}, file = {GeometryInCoqTphol04.pdf:/home/pedro/Actividades/Investigacao/ArqArtigos/DemGeo/GeometryInCoqTphol04.pdf:PDF}, owner = {pedro}, timestamp = {2007.05.18} } @MANUAL{Nesmith93, title = {Using Keim}, author = {Dan Nesmith}, year = {1993}, annote = {pedro, veio com o programa} } @TECHREPORT{Nevins74, author = {Nevins, Arthur J.}, title = {Plane Geometry Theorem Proving Using Forward Chaining}, institution = {MIT}, year = {1974}, type = {AI Lab memo}, number = {303}, month = {Jan}, abstract = {A computer program is described which operates on a subset of plane geometry. Its performance not only compares favorably with previous computer programs, but within its limited problem domain (e.g. no curved lines nor introduction of new points), it also invites comparison with the best human theorem provers. The program employs a combination of forward and backward chaining with the forward component playing the more important role. This, together with a deeper use of diagrammatic information, allows the program to dispense with the diagram filter in contrast with its central role in previous programs. An important aspect of human problem solving may be the ability to structure a problem space so that forward chaining techniques can be used effectively.}, file = {AIM-303.pdf:/home/pedro/Actividades/Investigacao/ArqArtigos/DemGeo/AIM-303.pdf:PDF}, owner = {pedro}, timestamp = {2007.04.05} } @ARTICLE{Nevis75, author = {Nevis, A.J.}, title = {Plane geometry theorem proving using forward chaining}, journal = {Artificial Intelligence}, year = {1975}, volume = {6}, pages = {1--23}, number = {1}, note = {% gramy} } @INPROCEEDINGS{Nickalls99, author = {Nickalls, Richard}, title = {mathsPIC - A filter for use with {\PiC\TeX}}, booktitle = {EuroTeX'99 Proceedings}, year = {1999} } @INPROCEEDINGS{Nipkow90srds, author = {Tobias Nipkow}, title = {Formal Verification of Data Type Refinement --- Theory and Practice}, booktitle = {Stepwise Refinement of Distributed Systems}, year = {1990}, editor = {J.W. de Bakker and W.-P. de Roever and G. Rozenberg}, pages = {561--591}, publisher = {Springer-Verlag LNCS 430}, keywords = {Isabelle} } @INPROCEEDINGS{Nipkow93le, author = {Tobias Nipkow}, title = {Order-Sorted Polymorphism in {Isabelle}}, booktitle = {Logical Environments}, year = {1993}, editor = {G. Huet and G. Plotkin}, pages = {164--188}, publisher = {Cambridge University Press}, keywords = {Isabelle} } @INPROCEEDINGS{Nipkow90ctrs, author = {Tobias Nipkow}, title = {Higher-Order Unification, Polymorphism and Subsorts}, booktitle = {Proceedings of the 2nd International Workshop on Conditional and Typed Rewriting Systems}, year = {1990}, editor = {S. Kaplan and M. Okada}, publisher = {Springer-Verlag LNCS 516}, keywords = {Isabelle, unification} } @ARTICLE{Nipkow89fac, author = {Tobias Nipkow}, title = {Term Rewriting and Beyond --- Theorem Proving in {Isabelle}}, journal = {Formal Aspects of Computing}, year = {1989}, volume = {1}, pages = {320--338}, keywords = {Isabelle, rewriting} } @ARTICLE{Nipkow89scp, author = {Tobias Nipkow}, title = {Equational Reasoning in {Isabelle}}, journal = {Science of Computer Programming}, year = {1989}, volume = {12}, pages = {123--149}, keywords = {Isabelle} } @INPROCEEDINGS{Nipkow92, author = {Tobias Nipkow and Lawrence C. Paulson}, title = {{Isabelle}-91}, booktitle = {Proceedings of the 11th International Conference on Automated Deduction}, year = {1992}, editor = {D. Kapur}, pages = {673--676}, address = {Saratoga Springs, NY}, publisher = {Springer-Verlag LNAI 607}, note = {System abstract}, keywords = {Isabelle} } @BOOK{Nordstrom90, title = {Programming in Martin-L{\"o}f's Type Theory -- An Introduction}, publisher = {Claredon Press}, year = {1990}, author = {Bengt Nordstr{\"o}m and Kent Petersson and Jan M. Smith}, series = {International Series of Monographs on Computer Science - 7}, address = {Oxford}, annote = {Type Theory;} } @BOOK{Notari05, title = {Lernsysteme und ICT: CMS-LMS-LCMS-C3MS}, year = {2005}, author = {Michel Notari}, owner = {pedro}, timestamp = {2008.01.22} } @ARTICLE{Noel93, author = {Philippe No{\"e}l}, title = {Experimenting with {Isabelle} in {ZF} Set Theory}, journal = {Journal of Automated Reasoning}, year = {1993}, volume = {10}, pages = {15--58}, number = {1}, annote = {ucdee}, keywords = {Isabelle} } @TECHREPORT{Noel91, author = {Philippe No{\"e}l}, title = {A Set Theoretic Semantics for a first order Temporal Logic: Definition and Application using {Isabelle}}, institution = {Department of Computer Science, University of Manchester}, year = {1991}, number = {UMCS-91-12-4}, keywords = {Isabelle} } @UNPUBLISHED{Obrecht04, author = {Obrecht, Christian}, title = {Eukleides}, note = {http://www.eukleides.org/} } @BOOK{Oliveira79, title = {L{\'o}gica Elementar (Introdu\c{c}{\~a}o {\`a} L{\'o}gica Matem{\'a}tica)}, publisher = {Associa\c{c}{\~a}o de Estudantes da Faculdade de Ci{\^e}ncias de Lisboa}, year = {1979}, author = {Oliveira, A. J. Franco}, volume = {1}, series = {Textos de L{\'o}gica Matem{\'a}tica, Teoria de Conjuntos e Fundamentos}, address = {Faculdade de Ci{\^e}ncias de Lisboa}, annote = {L{\'o}gica} } @MANUAL{Otten99, title = {Con\TeX t an excursion}, author = {Otten, Ton and Hagen, Hans}, organization = {Pragma ADE}, address = {Hasselt}, year = {1999} } @BOOK{Papert88, title = {Logo : computadores e educa\c{c}{\~a}o}, publisher = {Brasiliense}, year = {1988}, author = {Papert, Seymour}, address = {S\~ao Paulo}, edition = {3a} } @INPROCEEDINGS{Paulson92, author = {Paulson, Lawrence C.}, title = {Designing a Theorem Prover}, booktitle = {Handbook of Logic in Computer Science}, year = {1992}, editor = {Abransky}, volume = {II}, address = {Oxford}, publisher = {Oxford Science Publications}, annote = {Tenho fotocopias.} } @INPROCEEDINGS{Paulson94cade, author = {Lawrence C. Paulson}, title = {A Fixedpoint Approach to Implementing (Co)Inductive Definitions}, booktitle = {Proceedings of the 12th International Conference on Automated Deduction}, year = {1994}, editor = {Alan Bundy}, pages = {148--161}, address = {Nancy, France}, month = {June}, publisher = {Springer-Verlag LNAI 814}, keywords = {Isabelle} } @INPROCEEDINGS{Paulson88cade, author = {Lawrence C. Paulson}, title = {Isabelle: The Next Seven Hundred Theorem Provers}, booktitle = {Proceedings of the 9th International Conference on Automated Deduction}, year = {1988}, editor = {E. Lusk and R. Overbeek}, pages = {772--773}, address = {Argonne, Illinois}, publisher = {Springer Verlag LNCS 310}, note = {System abstract}, keywords = {Isabelle} } @INPROCEEDINGS{Paulson88colog, author = {Lawrence C. Paulson}, title = {A Formulation of the Simple Theory of Types (for {Isabelle})}, booktitle = {Proceedings of the International Conference on Computer Logic {COLOG'88}}, year = {1988}, editor = {P. Martin-Lof and G. Mints}, pages = {246--274}, address = {Tallinn, Estonia}, month = {December}, publisher = {Springer-Verlag LNCS 417}, keywords = {Isabelle} } @INCOLLECTION{Paulson90lacs, author = {Lawrence C. Paulson}, title = {{Isabelle}: The Next 700 Theorem Provers}, booktitle = {Logic and Computer Science}, publisher = {Academic Press}, year = {1990}, editor = {P. Odifreddi}, pages = {361--386}, keywords = {Isabelle} } @MANUAL{Paulson98, title = {The Isabelle Reference Manual}, author = {Lawrence C. Paulson}, organization = {Computer Laboratory, University of Cambridge}, year = {1998}, annote = {Descarregado a partir da "Internet", ficheiro "postscript".} } @BOOK{Paulson94book, title = {Isabelle: A Generic Theorem Prover}, publisher = {Springer-Verlag}, year = {1994}, author = {Lawrence C. Paulson}, volume = {828}, series = {LNCS}, keywords = {Isabelle} } @TECHREPORT{Paulson94tr, author = {Lawrence C. Paulson}, title = {A Concrete Final Coalgebra Theorem for ZF Set Theory}, institution = {University of Cambridge, Computer Laboratory}, year = {1994}, number = {334}, keywords = {Isabelle} } @ARTICLE{Paulson93, author = {Lawrence C. Paulson}, title = {Set Theory for Verification: I. From Foundations to Fuctions}, journal = {Journal of Automated Reasoning}, year = {1993}, volume = {11}, pages = {353--389}, number = {3}, annote = {ucdee} } @TECHREPORT{Paulson93a, author = {Lawrence C. Paulson}, title = {Introduction to {Isabelle}}, institution = {University of Cambridge, Computer Laboratory}, year = {1993}, number = {280}, keywords = {Isabelle} } @TECHREPORT{Paulson93b, author = {Lawrence C. Paulson}, title = {{Isabelle}'s Object-Logics}, institution = {University of Cambridge, Computer Laboratory}, year = {1993}, number = {286}, keywords = {Isabelle} } @TECHREPORT{Paulson93c, author = {Lawrence C. Paulson}, title = {The {Isabelle} Reference Manual}, institution = {University of Cambridge, Computer Laboratory}, year = {1993}, number = {283}, keywords = {Isabelle} } @ARTICLE{Paulson93jar, author = {Lawrence C. Paulson}, title = {Set Theory for Verification: {I}. {From} Foundations to Functions}, journal = {Journal of Automated Reasoning}, year = {1993}, volume = {11}, pages = {353--389}, number = {3}, keywords = {Isabelle} } @TECHREPORT{Paulson93trd, author = {Lawrence C. Paulson}, title = {Set Theory for Verification: {II}. {Induction} and Recursion}, institution = {University of Cambridge, Computer Laboratory}, year = {1993}, number = {312}, keywords = {Isabelle} } @TECHREPORT{Paulson93tre, author = {Lawrence C. Paulson}, title = {Co-induction and Co-recursion in Higher-Order Logic}, institution = {University of Cambridge, Computer Laboratory}, year = {1993}, number = {304}, month = {July}, keywords = {Isabelle} } @BOOK{Paulson91, title = {ML for the Working Programmer}, publisher = {Cambridge University Press}, year = {1991}, author = {Lawrence C. Paulson}, address = {Cambridge}, annote = {Standard ML; Programa\c{c}{\~a}o Funcional} } @ARTICLE{Paulson89, author = {Lawrence C. Paulson}, title = {The Foundation of a Generic Theorem Prover}, journal = {Journal of Automated Reasoning}, year = {1989}, volume = {5}, pages = {363--397}, number = {3}, keywords = {Isabelle} } @ARTICLE{Paulson86, author = {Lawrence C. Paulson}, title = {Natural Deduction as Higher-order Resolution}, journal = {Journal of Logic Programming}, year = {1986}, volume = {3}, pages = {237--258}, keywords = {Isabelle} } @TECHREPORT{Paulson90tr, author = {Lawrence C. Paulson and Tobias Nipkow}, title = {{Isabelle} Tutorial and User's Manual}, institution = {University of Cambridge, Computer Laboratory}, year = {1990}, number = {189}, month = {January}, keywords = {Isabelle} } @MANUAL{manflex, title = {Flex man page}, author = {Vern Paxson}, year = {2000} } @UNPUBLISHED{Pereira04, author = {Ana Pereira}, title = {Demonstra\c{c}\~oes \mbox{G}eom\'etricas}, note = {Primeiro Trabalho Cient{\'\i}fico, Est\'agio Pedag\'ogico, Licenciatura em Matem\'atica - Ramo Educacional, F.C.T.U.C.}, year = {2004} } @MANUAL{Haskell97a, title = {Report on the Programming Language Haskell}, author = {Peterson, John and Hammond, Kevin and Augustsson, Lennart and Boutel, Brian and Burton, Warren and Fasel, Joseph and Gordon, Andrew and Hughes, John and Hudak, Paul and Johnsson, Thomas and Mark Jones and Meijer, Erik and Peyton-Jones, Simon and Reid, Alastair and Wadler Philip}, edition = {Version 1.4}, month = {April, 7}, year = {1997} } @INPROCEEDINGS{Pfenning91, author = {Frank Pfenning}, title = {Logic Programming in the {LF} Logical Framework}, booktitle = {Logical Frameworks}, year = {1991}, editor = {G\'{e}rard Huet and Gordon D. Plotkin}, publisher = {Cambridge University Press}, key = {Pfenning91} } @INPROCEEDINGS{Pfenning92, author = {Frank Pfenning and Ekkehard Rohwedder}, title = {Implementing the Meta-Theory of Deductive Systems}, booktitle = {Proceedings of the 11th International Conference on Automated Deduction}, year = {1992}, editor = {D. Kapur}, pages = {537--551}, address = {Saratoga Springs, New York}, month = {June}, publisher = {Springer-Verlag LNAI 607}, key = {Pfenning92} } @BOOK{Pierce98, title = {Basic Category Theory for Computer Scientists}, publisher = {The MIT Press}, year = {1998}, author = {Pierce, Benjamin}, series = {Foundations of Computing}, address = {London, England} } @BOOK{Pohlers80, title = {Proof Theory, An Introduction}, publisher = {Springer-Verlag}, year = {1980}, author = {Wolfram Pohlers}, volume = {1407}, series = {Lecture Notes in Mathematics}, address = {Berlin}, annote = {ucma XIX 1407}, isbn = {3-540-51842-8} } @BOOK{Ponnambalan98, title = {A C++ Primer for Engineers: An Object-oriented Approach}, publisher = {McGraw-Hill International Editions}, year = {1998}, author = {Ponnambalam, K. and Alguindigue, Tiuley} } @PHDTHESIS{Puls90, author = {Thomas Puls}, title = {Annotation Logic for {Standard ML}}, school = {Technical University of Denmark}, year = {1990}, address = {Lyngby}, month = {Oct}, note = {Department of Computer Science Report ID-TR:1990-74}, keywords = {Isabelle} } @MISC{Punin01, author = {Punin, John and Krishnamoorthy, Mukkai}, title = {XGMML 1.0 Draft Specification}, howpublished = {URL:http://www.cs.rpi.edu/\~{}puninj/XGMML/draft-xgmml-20010628.html}, year = {2001} } @INPROCEEDINGS{Quaresma95, author = {Quaresma, Pedro}, title = {Implementing a Deduction System for a Guarded Commands Procedural Language using a Generic Theorem Prover}, booktitle = {Proceedings of the 11th Israeli Symposium on Artificial Intelligence}, year = {1995}, editor = {Shaul Markovitch}, number = {9502}, series = {CIS Report}, pages = {14 -- 26}, address = {Haifa - Israel}, month = {January}, annote = {(pqa)}, optorganization = {Technion - Israel Institute of Technology} } @UNPUBLISHED{Quaresma04, author = {Quaresma, Pedro}, title = {Eukleides{PT}}, note = {http://gentzen.mat.uc.pt/\~{}eukleides} } @INPROCEEDINGS{Quaresma07b, author = {Quaresma, Pedro}, title = {Constru\c{c}{\~a}o din{\^a}mica de documentos {PDF} em p{\'a}ginas {W}eb}, booktitle = {Livro de Actas da Confer{\^e}ncia Ibero-Americana, 3-5 Dezembro 2007, Porto, Portugal}, year = {2007}, pages = {21-27}, organization = {IASK}, owner = {pedro}, timestamp = {2007.12.06} } @ARTICLE{pedro05, author = {Pedro Quaresma}, title = {Stacks in TeX}, journal = {TUGboat}, year = {2005}, volume = {26}, number = {1} } @INPROCEEDINGS{Quaresma02a, author = {Quaresma, Pedro}, title = {Constru{\c c}{\~a}o Modular de Sistemas de Dedu{\c c}{\~a}o}, booktitle = {Mem{\'o}rias da Conferencia Iberoamericana en Sistemas Cibern{\'e}tica e Inform{\'a}tica, CISCI2002}, year = {2002}, month = {July}, organization = {SCI}, publisher = {Orlando, USA} } @TECHREPORT{Quaresma02b, author = {Quaresma, Pedro}, title = {Logical Specification of Commutative Diagrams in a (La)\TeX\ Document}, institution = {CISUC}, year = {2002}, number = {TR 2002/001} } @INPROCEEDINGS{Quaresma01a, author = {Quaresma, Pedro}, title = {The Electronic Publishing Toolbox}, booktitle = {Proceedings of the conference Electronic Media in Mathematics}, year = {2001}, address = {Coimbra, Portugal}, month = {September} } @INPROCEEDINGS{Quaresma01b, author = {Quaresma, Pedro}, title = {{DC}pic, Commutative Diagrams in a {(La)\TeX} Document}, booktitle = {Proceedings of the conference Euro\TeX\ 2001}, year = {2001}, address = {Rolduc, The Netherlands}, month = {September} } @PHDTHESIS{Quaresma98, author = {Quaresma, Pedro}, title = {Constru\c{c}{\~a}o Modular de Sistemas de Dedu\c{c}{\~a}o}, school = {Departamento Inform{\'a}tica, Universidade do Minho}, year = {1998}, note = {in portuguese}, language = {Portugu{\^e}s}, optmonth = {Novembro} } @BOOK{Quaresma96, title = {Introdu\c{c}{\~a}o ao \LaTeX}, publisher = {Escolar Editora}, year = {1996}, author = {Quaresma, Pedro}, isbn = {972-592-091-0}, language = {Portugu{\^e}s} } @MASTERSTHESIS{Quaresma88, author = {Quaresma, Pedro}, title = {Estudo Comparativo de Algoritmos para o Problemas de Transportes com Custos-Fixos}, school = {Departamento de Matem{\'a}tica da Universidade de Coimbra}, year = {1988}, address = {Apartado 3008, 3000 COIMBRA}, annote = {investiga\c{c}{\~a}o operacional, np-completos, custos c{\^o}ncavos} } @TECHREPORT{Quaresma06b, author = {Quaresma, Pedro and Janicic, Predrag}, title = {Framework for Constructive Geometry (Based on the Area Method)}, institution = {Centre for Informatics and Systems of the University of Coimbra}, year = {2006}, number = {2006/001} } @TECHREPORT{Quaresma06c, author = {Quaresma, Pedro and Janicic, Predrag}, title = {{G}eo{T}hms - Geometry Framework}, institution = {Centre for Informatics and Systems of the University of Coimbra}, year = {2006}, number = {2006/002} } @INPROCEEDINGS{Quaresma06f, author = {Quaresma, Pedro and Jani{\v c}i{\'c}, Predrag}, title = {{G}eo{T}hms - a {W}eb System for {E}uclidean Constructive Geometry}, booktitle = {Proceedings of the 7th Workshop on User Interfaces for Theorem Provers (UITP 2006)}, year = {2007}, editor = {Autexier, S. and Benzm{\"u}ller, C.}, volume = {174}, number = {2}, series = {Electronic Notes in Theoretical Computer Science}, pages = {35--48}, month = {May}, publisher = {Elsevier B.V.} } @INPROCEEDINGS{Quaresma06e, author = {Quaresma, Pedro and Jani{\v c}i{\'c}, Predrag and Jelena Toma{\v s}evi{\'c}, Milena Vujo\v{s}evic-Jani{\v c}i{\'c}, Dusan Tosi{\'c}}, title = {XML-based Format for Descriptions of Geometrical Constructions and Geometrical Proofs}, booktitle = {CMDE 2006}, year = {2006}, number = { }, series = { }, address = { }, publisher = { } } @ARTICLE{Quaresma08a, author = {Quaresma, Pedro and Lopes, Elsa}, title = {Criptografia}, journal = {Gazeta de Matem{\'a}tica}, year = {aceite para publica{\c c}{\~a}o} } @INPROCEEDINGS{Quaresma86, author = {Quaresma, Pedro and Martins, L{\'u}cia}, title = {A Factoriza\c{c}{\~a}o de Equa\c{c}{\~o}es do Segundo Grau numa Aprendizagem Assistida por Computador}, booktitle = {Actas Epia86}, year = {1986}, address = {Lisboa}, annote = {intelig{\^e}ncia artificial} } @ARTICLE{Quaresma06a, author = {Quaresma, Pedro and Pereira, Ana}, title = {Visualiza{\c c\~a}o de Constru{\c c\~o}es Geom\'etricas}, journal = {Gazeta de Matem\'atica}, year = {2006}, volume = {151}, pages = {38--41}, month = {Junho} } @ARTICLE{Quaresma08b, author = {Quaresma, Pedro and Pinho, Augusto}, title = {Criptoan{\'a}lise}, journal = {Gazeta de Matem{\'a}tica}, year = {aceite para publica{\c c}{\~a}o}, owner = {pedro}, timestamp = {2007.02.22} } @INPROCEEDINGS{Quaresma07a, author = {Quaresma, Pedro and Pinho, Augusto}, title = {An{\'a}lise de Frequ{\^e}ncias da L{\'\i}ngua {P}ortuguesa}, booktitle = {Livro de Actas da Confer{\^e}ncia Ibero-Americana, InterTIC, 3-5 Dezembro 2007, Porto, Portugal}, year = {2007}, pages = {267-272}, organization = {IASK}, owner = {pedro}, timestamp = {2007.12.06} } @UNPUBLISHED{queiro02, author = {Queir{\'o}, Jo{\~a}o}, title = {Teoria dos N{\'u}meros}, note = {Departamento de Matem{\'a}tica, Universidade de Coimbra}, year = {2002} } @BOOK{Reichel87, title = {Initial Computability, Algebraic Specification and Partial Algebras}, publisher = {The claredon Press, Oxford University Press}, year = {1987}, author = {Horst Reichel}, series = {Oxford Science Publications -- The International Serie of Monographs on Computer Science, 2}, address = {New York}, annote = {Especifica\c{c}{\~a}o alg{\'e}brica, sem{\^a}ntica inicial} } @MANUAL{Reynolds87, title = {User's Manual for Diagram Macros}, author = {Reynolds, John}, address = {http://www.cs.cmu.edu/{\~{}}jcr/}, year = {1987}, note = {{\tt diagmac.doc}} } @BOOK{Richter-Gebert99, title = {The Interactive Geometry Software Cinderella}, publisher = {Springer}, year = {1999}, author = {Richter-Gebert, J{{\"u}}rgen and Kortenkamp, Ulrich} } @BOOK{Riesel94, title = {Prime Numbers and Computer Methods for Factorization}, publisher = {Birkh{\"a}user}, year = {1994}, author = {Riesel, Hans}, volume = {126}, series = {Progress in Mathematics}, edition = {2nd} } @ARTICLE{Rivest78, author = {Rivest, R. and Shamir, A. and Adleman, L.}, title = {A Method for Obtaining Digital Signatures and Public-Key Cryptosystems}, journal = {Communications of the ACM}, year = {1978}, volume = {21}, pages = {120--126}, number = {2} } @ARTICLE{Robinson65, author = {Robinson, J. A.}, title = {A Machine-Oriented Logic Based on the Resolution Principle}, journal = {Journal of the Association for Computing Machinery}, year = {1965}, volume = {12}, pages = {23--41}, number = {1}, month = {January}, annote = {Tenho fotocopia} } @BOOK{Rodrigues98, title = {Programa\c{c}{\~a}o em C++}, publisher = {FCA, Editora de Inform{\'a}tica LDA}, year = {1998}, author = {Rodrigues, Pimenta and Pereira, Pedro and Sousa, Manuela}, edition = {2} } @INPROCEEDINGS{Rossen91ho, author = {Lars Rossen}, title = {Proving (facts about) {Ruby}}, booktitle = {IV Higher Order Workshop}, year = {1990}, editor = {G. Birtwistle}, pages = {265--283}, address = {Banff, Alberta}, month = {September}, publisher = {Springer-Verlag Workshops in Computing}, keywords = {Isabelle} } @INPROCEEDINGS{Rossen91dcc, author = {Lars Rossen}, title = {Ruby Algebra}, booktitle = {Designing Correct Circuits}, year = {1990}, editor = {G. Jones and M. Sheeran}, address = {Oxford, England}, month = {September}, publisher = {Springer-Verlag Workshops in Computing}, keywords = {Isabelle} } @INCOLLECTION{Rossen90, author = {Lars Rossen}, title = {Formal {Ruby}}, booktitle = {Formal Methods for {VLSI} Design}, publisher = {Elsevier}, year = {1990}, editor = {J. Staunstrup}, keywords = {Isabelle} } @BOOK{Rydeheard88, title = {Computacional Category Theory}, publisher = {Prentice-Hall International}, year = {1988}, author = {D.E. Rydheard and R.M. Burstall}, series = {Computer Science}, annote = {Teoria das Categorias, Standard ML} } @ARTICLE{Sadagopan82, author = {S. Sadagopan and A. Ravidran}, title = {A Vertex Ranking Algorithm for the Fixed--Charge Transportation Problem}, journal = {Jota}, year = {1982}, volume = {37}, number = {2} } @INPROCEEDINGS{Salibra93, author = {Antonino Salibra and Giuseppe Scollo}, title = {A Soft Stairway to Institutions}, booktitle = {Recent Trends in Data Type Specification}, year = {1993}, editor = {M. Bidoit and C. Choppy}, volume = {655}, series = {Lecture Notes in Computer Science}, pages = {310--329}, address = {Berlin}, publisher = {Springer-Verlag}, annote = {Biblioteca da Univ. do Minho. Tenho fotocopias.} } @MASTERSTHESIS{Santos07, author = {Santos, Vanda}, title = {Constru\c{c}{\~a}o de um Módulo de e-Aprendizagem para a Geometria Euclidiana}, school = {Departamento de Matemática, Faculdade de Ciências e Tecnologia da Universidade de Coimbra}, year = {2007}, note = {(submetida)}, owner = {pedro}, timestamp = {2008.01.23} } @TECHREPORT{Saraiva95, author = {Saraiva, {Jo\~ao Alexandre}}, title = {Especifica\c{c}\~ao e Processamento de Linguagens}, institution = {Departamento de Inform\'atica da Universidade do Minho}, year = {1995}, type = {Texto Pedag\'ogico}, month = {Mar\c{c}o} } @INPROCEEDINGS{Schneider92b, author = {Klaus Schneider and Ramayya Kumar Thomas Kropf}, title = {Efficient Representation and Computation of Tableaux Proofs}, booktitle = {Proceedings of the International Workshop on Higher Order Logic Theorem Proving and its applications}, year = {1992}, address = {Leuven, Belgium} } @INPROCEEDINGS{Schneider93, author = {Klaus Schneider and Ramayya Kumar and Thomas Kropf}, title = {Hardware-Verification using First Order BDDs}, booktitle = {Proceedings of the 11th International Conference on Computer Hardware Description Languages and their Applications}, year = {1993}, volume = {32}, series = {IFIP Transactions A: Computer Science and Technology}, pages = {45--62}, address = {Amsterdam, The Netherlands}, month = {apr}, publisher = {North-Holland}, annote = {est{\~a}p no arquivo relativo ao Faust}, keywords = {Faust} } @INPROCEEDINGS{Schneider92, author = {Klaus Schneider and Ramayya Kumar and Thomas Kropf}, title = {Structuring Hardware Proofs: First steps towards Automation in a Higher-Order Environment, CAV-91}, booktitle = {Proceedings of the Conference on Computer Aided Verification}, year = {1992}, number = {575}, series = {Lecture Notes in Computer Science}, address = {Berlin}, publisher = {Springer-Verlag}, keywords = {Faust} } @ARTICLE{Schneider92a, author = {Klaus Schneider and Ramayya Kumar and Thomas Kropf}, title = {The {Faust-Prover}}, journal = {Lectures Notes in Computer Science}, year = {1992}, volume = {607}, keywords = {Faust} } @ARTICLE{Schumann94, author = {J. Schumann}, title = {Tableau-Based Theorem Provers: Systems and Implementations}, journal = {Journal of Automated Reasoning}, year = {1994}, volume = {13}, pages = {409--421}, annote = {pqa} } @BOOK{Schutte77, title = {Proof Theory}, publisher = {Springer-Verlag}, year = {1977}, author = {Kurt Sch{\"u}tte}, address = {Berlin}, annote = {ucmt 03F/SCH/trdiny}, isbn = {3-540-07911-4}, keywords = {Proof Theory} } @BOOK{Sengupta94, title = {C++, Object-Oriented Data Structures}, publisher = {Springer-Verlag}, year = {1994}, author = {Semgupta, Saumyendra and Korobkin, {Carl Philip}}, address = {New-York}, note = {DMAT 68N/SEN} } @TECHREPORT{Sernadas93, author = {Am\'{\i}lcar Sernadas and Cristina Sernadas}, title = {Denotational Semantics of Object Specification Within an Arbitrary Temporal Logic Institution}, institution = {Instituto Superior T{\'e}cnico --- Departamento de Matem{\'a}tica}, year = {1993}, type = {Preprint}, number = {12/93}, address = {Instituto Superior T{\'e}cnico, Lisboa}, month = {June} } @INCOLLECTION{Sernadas97c, author = {Sernadas, A. and Sernadas, C. and Caleiro, C.}, title = {Synchronization of logics with mixed rules: Completeness preservation}, booktitle = {Algebraic Methodology and Software Technology}, publisher = {Springer-Verlag}, year = {1997}, editor = {Johnson, M.}, volume = {1349}, series = {Lecture Notes in Computer Science}, pages = {465--478} } @ARTICLE{Sernadas99, author = {Sernadas, A. and Sernadas, C. and Caleiro, C.}, title = {Fibring of logics as a categorial construction}, journal = {Journal of Logic and Computation}, year = {1999}, volume = {9}, pages = {149--179}, number = {2} } @TECHREPORT{Sernadas97a, author = {Sernadas, A. and Sernadas, C. and Caleiro, C.}, title = {Fibring of logics as a categorial construction}, institution = {Section of Computer Science, Department of Mathematics, Instituto Superior T\'ecnico}, year = {1997}, type = {Research Report}, number = {Submitted for publication}, address = {1096 Lisboa} } @ARTICLE{Sernadas97b, author = {A. Sernadas and C. Sernadas and C. Caleiro}, title = {Synchronization of logics}, journal = {Studia Logica}, year = {1997}, volume = {59}, pages = {217--247}, number = {2}, annote = {CIM Summer School} } @INPROCEEDINGS{Sernadas95, author = {Am\'{\i}lcar Sernadas and Cristina Sernadas and Jos{\'e} Manuel Valen\c{c}a}, title = {A Theory-based Topological Notion of Institution}, booktitle = {Recent Trends in Data Type Specification}, year = {1995}, editor = {Egidio Astesian and Gianna Reggio and Andrzej Tarlecki}, number = {906}, series = {Lecture Notes in Computer Science}, pages = {420--436}, address = {Berlin}, publisher = {Springer-Verlag}, annote = {Fotocopiado do livro pertencente a JMV} } @BOOK{Serrao07, title = {Programa{\c c}{\~a}o com PHP 5}, publisher = {FCA}, year = {2007}, author = {Serr{\~a}o, Carlos and Marques Joaquim}, address = {Lisboa}, owner = {pedro}, timestamp = {2007.08.17} } @INPROCEEDINGS{Shankar92, author = {N. Shankar}, title = {Proof Search in the Intuicionistic Sequent Calculus}, booktitle = {Automated Deduction --- Cade -- 11}, year = {1992}, editor = {D. Kapur}, volume = {607}, series = {Lecture Notes in Artificial Intelligence}, pages = {522--536}, address = {Berlin}, publisher = {Springer-Verlag}, annote = {ucdee C1230 INT} } @BOOK{Silberschatz06, title = {Database System Concepts}, publisher = {McGraw Hill}, year = {2006}, author = {Silberschatz, A. and Korth, H. and Sudarshan, S.}, address = {New York}, edition = {5th} } @BOOK{sinkov66, title = {Elementary Cryptanalysis, a mathematical approach}, publisher = {The Mathematical Association of America}, year = {1966}, author = {Sinkov, Abraham} } @BOOK{Smullyan68, title = {First-Order Logic}, publisher = {Springer-Verlag}, year = {1968}, author = {R. M. Smullyan}, volume = {43}, series = {Ergebnisse der Mathematik und ihrer Grenzgebiete}, address = {Berlin}, annote = {Logica} } @BOOK{Spillman05, title = {Classical and Contemporary Cryptology}, publisher = {Prentice Hall}, year = {2005}, author = {Spillman, Richard} } @BOOK{Spillman05a, title = {Classical and Contemporary Criptology}, publisher = {Pearson Prentice-Hall}, year = {2005}, author = {Spillman, Richard}, address = {Upper Saddle River, NJ 07458} } @ARTICLE{Stefani97, author = {Raymond T. Stefani}, title = {Survey of the major world sports rating systems}, journal = {Journal of Applied Statistics}, year = {1997}, volume = {24}, pages = {635 - 646}, number = {6}, month = {December}, owner = {pedro}, timestamp = {2007.12.12} } @MANUAL{Stevens93, title = {Mechanised Theorem Proving with 2OBJ: A Tutorial Introduction}, author = {Andrew Stevens and Keith Hobley}, edition = {Draft}, month = {February}, year = {1993}, annote = {Demonstra\c{c}{\~a}o Autom{\'a}tica de Teoremas.} } @ARTICLE{Stickel88, author = {Stickel, Mark}, title = {A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler}, journal = {Journal of Automated Reasoning}, year = {1988}, volume = {4}, pages = {353--380}, note = {% tenho c{\'o}pia} } @BOOK{Stinson2006, title = {Cryptography: Theory and Practice}, publisher = {Chapman \& Hall/CRC}, year = {2006}, author = {Stinson, Douglas}, edition = {3rd}, owner = {pedro}, timestamp = {2007.07.30} } @MISC{Sutcliffe, author = {Sutcliffe, Geoff}, title = {The TPTP Problem Library}, howpublished = {http://www.cs.miami.edu/\~{}tptp/TPTP/TR/TPTPTR.shtml} } @BOOK{Szabo78, title = {Algebra of Proofs}, publisher = {North-Holland Publishing Company}, year = {1978}, author = {M. E. Szabo}, volume = {88}, series = {Studies in Logic and The foundations of Mathematics}, address = {Amsterdam}, annote = {1.Proof Theory 2. Categories 3. Combinatory Logic.} } @ARTICLE{Szabo76, author = {M. E. Szabo}, title = {Quantifier-Complete Categories}, journal = {Journal of Pure and Applied Algebra}, year = {1976}, volume = {7}, pages = {97--114}, note = {North-Holland Publishing Company}, annote = {Fotocopia (ucma)} } @BOOK{Takeuti75, title = {Proof Theory}, publisher = {North-Holland Publishing Company}, year = {1975}, author = {Gaisi Takeuti}, volume = {81}, series = {Studies in Logic and The Foundations of Mathematics}, address = {Amsterdam}, annote = {ucmt 03F/TAK}, isbn = {S 0-7204-2200-0}, keywords = {Proof Theory} } @MANUAL{Thanh99, title = {The pdfTeX manual}, author = {Th\`anh, {H{\`a}n Th{$\acute{\hat{\mathrm e}}$}} and Rahtz, Sebastian and Hagen, Hans}, year = {1999} } @INPROCEEDINGS{Thery92, author = {Laurent Thery and Yves Bertot and Gilles Kahn}, title = {Real Theorem Provers Deserve Real User-Interfaces}, booktitle = {Proceedings of the Fifth {ACM} {SIGSOFT} Symposium on Software Development Environments}, year = {1992}, pages = {120--129}, note = {Published as {SIGSOFT} Software Engineering Notes, Vol.~17, No.~5}, keywords = {Coq, Isabelle} } @BOOK{Thompson96, title = {Haskell, The Craft of Funcional Programming}, publisher = {Addison-Wesley}, year = {1996}, author = {Thompson, Simon}, address = {Harlow}, isbn = {0-201-40357-9} } @BOOK{Tkotz05, title = {CRIPTOGRAFIA - Segredos Embalados para Viagem}, publisher = {NOVATEC Editora}, year = {2005}, author = {Tkotz, Viktoria}, address = {S{\~a}o Paulo, Brasil} } @BOOKLET{Valenca00, title = {Fundamentos da Computa{\c c}{\~a}o Livro {II}: Programa{\c c}{\~a}o Funcional}, author = {Jos{\'e} M. Valen{\c c}a and Jos{\'e} B. Barros}, address = {Departamento de Inform{\'a}tica, Universidade do Minho}, owner = {pedro}, timestamp = {2007.03.26} } @BOOK{Veloso83, title = {Estruturas de Dados}, publisher = {Editora Campus Ltda.}, year = {1983}, author = {Paulo Veloso and Cl{\'e}sio dos Santos and Paulo Azeredo and Ant{\'o}nio Furtado}, address = {Rio de Janeiro}, isbn = {85-7001-094-X}, keywords = {Modelos Matematicos, Programacao.}, language = {Portugues} } @BOOK{Vickers89, title = {Topology via Logic}, publisher = {Cambridge University Press}, year = {1989}, author = {Steven Vickers}, address = {Cambridge}, annote = {sdum??}, isbn = {0 521 36062 5}, language = {ingles} } @INPROCEEDINGS{Wang95, author = {Wang, D.}, title = {Reasoning about geometric problems using an elimination method}, booktitle = {Automated Pratical Reasoning}, year = {1995}, editor = {Pfalzgraf, J. and Wang, D.}, pages = {147--185}, address = {New York}, publisher = {Springer}, note = {%citado em Gramy} } @MISC{GeotherWeb, author = {Wang, Dongming}, title = {Geother (GEOmetry THeorem provER)}, howpublished = {http://www-calfor.lip6.fr/\~{}wang/GEOTHER/} } @ARTICLE{Wang04, author = {Wang, Dongming}, title = {{GEOTHER} 1.1: Handling and Proving Geometric Theorems Automatically}, journal = {Lecture Notes in Artificial Intelligence}, year = {2004}, volume = {2930}, pages = {194--215}, comment = {Automated Deduction in Geometry}, owner = {pedro}, timestamp = {2007.05.18} } @BOOK{Weiss97, title = {Data Structures and Algorithm Analysis in C}, publisher = {Addison-Wesley}, year = {1997}, author = {Weiss, Mark Allen}, address = {Menlo Park, California} } @BOOK{Welling05, title = {PHP and MySQL Web Development}, publisher = {Sams Publishing}, year = {2005}, author = {Welling, Luke and Thomson, Laura}, edition = {3rd} } @BOOK{Welsh82, title = {Introduction to Pascal}, publisher = {Prentice-Hall International, Inc.}, year = {1979}, author = {Jim Welsh and John Elder}, series = {Computer Science}, address = {London}, edition = {2nd Edition}, isbn = {0-13-491530-5} } @BOOK{Wichura92, title = {The \PiCTeX\ Manual}, publisher = {Personal \TeX\ Inc}, year = {1992}, author = {Wichura, Michael}, address = {12 Madrona Avenue, Mill Valley, CA 94941}, edition = {3rd}, month = {March} } @BOOK{Wichura87, title = {The {\PiCTeX} Manual}, publisher = {M. Pfeffer \& Co.}, year = {1987}, author = {Michael Wichura}, address = {New York} } @BOOK{Wikstrom89, title = {Functional Programming Using Standard ML}, publisher = {Prentice-Hall International}, year = {1989}, author = {Ake Wikstrom}, series = {Computer Science}, annote = {Standard ML, Programa{\c c}{\~a}o Funcional} } @INPROCEEDINGS{Wilson05, author = {Wilson, Sean and Fleuriot, Jacques}, title = {Combining Dynamic Geometry, Automated Geometry Theorem Proving and Diagrammatic Proofs}, booktitle = {Proceedings of UITP 2005}, year = {2005}, address = {Edinburgh, UK}, month = {April} } @BOOK{Wirth89, title = {Algoritmos e Estruturas de Dados}, publisher = {Prentice-Hall do Brasil}, year = {1989}, author = {Wirth, Niklaus}, address = {Rio de Janeiro} } @BOOK{Wirth86, title = {Algorithms \& Data Structures}, publisher = {Prentice-Hall}, year = {1986}, author = {Wirth, Niklaus}, address = {Englewood Cliffs, New Jersey, USA} } @BOOK{Wirth76, title = {Algorithms + Data Structures = Programs}, publisher = {Prentice-Hall, Inc.}, year = {1976}, author = {Niklaus Wirth}, series = {Automatic Computation}, address = {Englewood Clifs, New Jersey}, annote = {ucmat I-07-35}, isbn = {0-13-022418-9} } @BOOK{Wirth73, title = {Systematic Programming}, publisher = {Prentice-Hall, Inc.}, year = {1973}, author = {Niklaus Wirth}, address = {Englewood Clifs, New Jersey}, annote = {ucmat I-7-36}, isbn = {0-13-880369-2} } @BOOK{Wos92, title = {Automated Reasoning - Introduction and Applications}, publisher = {McGraw-Hill}, year = {1992}, author = {L. Wos and R. Overbeek and E. Lusk and J. Boyle}, address = {New York}, edition = {2nd Edition}, annote = {ucma O-22-5}, isbn = {0-07-911251-X}, keywords = {Logic, Automated Reasoning, Automated Deduction} } @INPROCEEDINGS{Wu00, author = {Wu, W.-T.}, title = {The characteristic set method and its application}, booktitle = {Mathematics Mechanization and Applications}, year = {2000}, editor = {Gao, X.-S. and Wang, D.}, pages = {3--41}, address = {San Diego, CA}, publisher = {Academic Press} } @ARTICLE{Wu1999, author = {Wu, Wen-ts{\"u}n}, title = {Automatic Geometry Theorem-Proving and Automatic Geometry Problem-Solving}, journal = {Lectures Notes in Artificial Inteligence}, year = {1999}, volume = {1669}, pages = {1-13}, owner = {pedro}, timestamp = {2006.11.24} } @BOOK{Young89, title = {X Window system: Programming and applications with Xt}, publisher = {Prentice-Hall}, year = {1989}, author = {Young, Douglas A.} } @ARTICLE{Zhang95, author = {Zhang, Jing-Zhong and Chou, Shang-Ching and Gao, Xiao-Shan}, title = {Automated production of traditional proofs for theorems in Euclidean geometry I. The Hilbert intersection point theorems}, journal = {Annals of Mathematics and Artificial Intelligenze}, year = {1995}, volume = {13}, pages = {109-137} } @BOOK{Zukowski05, title = {The Definitive Guide to Java Swing}, publisher = {Apress}, year = {2005}, author = {John Zukowski}, edition = {3rd}, owner = {pedro}, timestamp = {2007.02.22} } @BOOK{Abramsky92, title = {Handbook of Logic in Computer Science}, publisher = {Claredon Press}, year = {1992}, editor = {Abramsky, S. and Gabbay, Dov and Maibaum, T.}, volume = {1}, series = {Oxford Science Publications}, address = {Oxford} } @BOOK{Arruda77, title = {Non-Classical Logics, Model Theory and Computability}, publisher = {North-Holland Publishing Company}, year = {1977}, editor = {A. I. Arruda and N. C. A. da Costa and R. Chuaqui}, volume = {89}, series = {Studies in Logic and The Foundations of Mathematics}, address = {Amsterdam}, annote = {L{\'o}gica; Teoria dos Modelos; L{\'o}gicas n{\~a}o cl{\'a}ssicas} } @BOOK{Barwise77, title = {Handbook of Mathematical Logic}, publisher = {North-Holland Publishing Company}, year = {1977}, editor = {John Barwise}, volume = {90}, series = {Studies in Logic and the Foundations of Mathematics}, address = {Amsterdam}, annote = {Logic, Symbolic and mathematical} } @PROCEEDINGS{Broy88, title = {Constructive Methods in Computing Science}, year = {1988}, editor = {Manfred Broy}, address = {Berlin}, publisher = {Springer-Verlag}, annote = {construtivismo, teoria das categorias, teoria dos tipos} } @BOOK{Dold71, title = {Symposium on Semantics of Algorithmic Languages}, publisher = {Springer-Verlag}, year = {1971}, editor = {A. Dold and B. Eckmann}, volume = {188}, series = {Lecture Notes in Mathematics}, address = {Berlin} } @PROCEEDINGS{ijcar06, title = {Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006}, year = {2006}, editor = {Ulrich Furbach and Natarajan Shankar}, volume = {4130}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, booktitle = {Automated Reasoning}, isbn = {3-540-37187-7}, owner = {pedro}, timestamp = {2007.05.21} } @BOOK{Gabbay93, title = {Handbook of Logic in Artificial Intelligence and Logic Programming}, publisher = {Oxford Science Publications}, year = {1993}, editor = {Dov M. Gabbay and C. J. Hogger and J. A. Robinson}, volume = {1}, address = {Oxford}, annote = {ucmt 03-00/Han/V.1}, isbn = {0-19-853745-X(v.1)} } @BOOK{Ehrig87, title = {Categorical Methods in Computer Science, with Aspects from Topology}, publisher = {Springer-Verlag}, year = {1987}, editor = {H. Ehrig, H. Herrlich, H.-J. Kreowski and G. Prenss}, volume = {393}, series = {Lecture Notes in Computer Science}, address = {Berlin} } @PROCEEDINGS{adg04, title = {Automated Deduction in Geometry, 5th International Workshop, ADG 2004, Gainesville, FL, USA, September 16-18, 2004, Revised Papers}, year = {2006}, editor = {Hoon Hong and Dongming Wang}, volume = {3763}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, bibsource = {DBLP, http://dblp.uni-trier.de}, booktitle = {Automated Deduction in Geometry}, isbn = {3-540-31332-X}, owner = {pedro}, timestamp = {2007.05.21} } @BOOK{Lawvere72, title = {Topos, Algebraic Geometry and Logic}, publisher = {Springer-Verlag}, year = {1972}, editor = {F. W. Lawvere}, volume = {274}, series = {Lectures Notes in Mathematics}, address = {Berlin}, annote = {Topos} } @BOOK{Leeuwen90, title = {Formal Models and Semantics}, publisher = {Elsevier}, year = {1990}, editor = {Jan Van Leeuwen}, volume = {B}, series = {Handbook of Theoretical Computer Science}, address = {Amsterdam}, edition = {Second}, annote = {ucmt I-18-17}, isbn = {0-444-88074-7} } @PROCEEDINGS{mkm06, title = {5th International Conference, MKM 2006, Wokingham, UK, August 2006}, year = {2006}, editor = {{M. Borwein}, Jonathan and {M. Farmer}, William}, volume = {4108}, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer}, booktitle = {Mathematical Knowlegde Management}, isbn = {3-540-37104-4}, owner = {pedro}, timestamp = {2007.05.21} } @PROCEEDINGS{Quaresma03, title = {Soft Computing and Complex Systems}, year = {2003}, editor = {Quaresma, Pedro and Dourado, Ant{\'o}nio and Costa, Ernesto and Costa, {J. F\'elix}}, number = {21}, series = {CIM}, month = {June}, organization = {CIM - Centro Internacional de Matem\'atica} } @PROCEEDINGS{Shostak84, title = {7th International Conference on Automated Deduction}, year = {1984}, editor = {R. E. Shostak}, number = {170}, series = {Lecture Notes in Computer Science}, address = {Berlin}, publisher = {Springer-Verlag}, month = {May 14--16}, annote = {ucdee C1230-INT}, isbn = {3-540-96022-8}, keywords = {CADE-7, Automated Deduction} } @PROCEEDINGS{Siekmann86, title = {8th International Conference on Automated Deduction}, year = {1986}, editor = {Jorg H. Siekmann}, number = {230}, series = {Lecture Notes in Computer Science}, address = {Berlin}, publisher = {Springer-Verlag}, annote = {ucdee C1230-INT}, isbn = {3-540-16780-3}, keywords = {CADE-8, Automated Deduction} } @BOOK{Szabo69, title = {The Collected Papers of Gerhard Gentzen}, publisher = {North-Holland Publishing Company}, year = {1969}, editor = {M. E. Szabo}, series = {Studies in Logic and The Foundations of Mathematics}, address = {Amesterdam}, annote = {(ucmat ...) Uma refer{\^e}ncia importante para os sistemas NJ, NK, LJ e LK.}, isbn = {7204 2254 X (SBN)}, keywords = {Natural Deduction, Sequent Calculus} } @MISC{EGF07, title = {EGF Official ratings}, howpublished = {http://gemma.ujf.cas.cz/{\~{}}cieply/GO/gor.html}, owner = {pedro}, timestamp = {2007.12.12} } @MISC{wikipediaDesarguesTheorem, title = {Desargues' theorem}, howpublished = {From Wikipedia, the free encyclopedia}, year = {2006.}, note = {http://en.wikipedia.org/wiki/Desargues%27_theorem} } @MANUAL{HOL88a, title = {The HOL System TUTORIAL}, organization = {DSTO, Cambridge University, CRC-SRI}, edition = {2nd}, year = {1991}, annote = {Faz parte da documenta\c{c}{\~a}o que vem com o programa}, key = {HOL88a}, keywords = {HOL} } @MANUAL{HOL88b, title = {The HOL System DESCRIPTION}, organization = {DSTO, Cambridge University, CRC-SRI}, year = {1991}, annote = {Faz parte da documenta\c{c}{\~a}o que vem com o programa}, key = {HOL88b}, keywords = {HOL} } @MANUAL{HOL88c, title = {The HOL System REFERENCE}, organization = {DSTO, Cambridge University, CRC-SRI}, year = {1991}, annote = {Faz parte da documenta\c{c}{\~a}o que vem com o programa}, key = {HOL88c}, keywords = {HOL} } @MANUAL{HOL88d, title = {The HOL System LIBRARIES}, organization = {DSTO, Cambridge University, CRC-SRI}, year = {1991}, annote = {Faz parte da documenta\c{c}{\~a}o que vem com o programa}, key = {HOL88c}, keywords = {HOL} }