papers.html

Publications of Valeria de Paiva

Categorical Semantics of Linear Logic for All, Manuscript, (submitted 2006).
Bridges from Language to Logic: Concepts, Contexts and Ontologies (V. de Paiva) in 5th Logical and Semantic Frameworks with Applications, LSFA'10, parte of ICTAC in Natal, Brazil, 2010.
Constructive Description Logic, Hybrid-Style (V. de Paiva, H. Hausler e A. Rademaker), in Pre-proceedings of the International Workshop on Hybrid Logic and Applications (HyLo 2010), Aug 2010.
Using Intuitionistic Logic as a basis for Legal Ontologies (H. Hausler, A. Rademaker e V. de Paiva), in ``Proceedings of Legal Ontologies and Artificial Intelligence Techniques (LOAIT)", July 2010.
Logic, Language, Information and Computation, special issue of the journal Information and Computations, guest editors: G. Mints, Valeria de Paiva and R. de Queiroz, online 3 September 2009. DOI information: 10.1016/j.ic.2009.03.006

Context Inducing Nouns, (with Charlotte Price and Tracy H. King), in Knowledge and Reasoning for Answering Questions (KRAQ'08) workshop associated with COLING'08, Manchester, UK, 23 August 2008, preliminary version.
Designing Testsuites for Grammar-based Systems in Applications (with Tracy H. King), in Workshop on Grammar Engineering Across Frameworks (GEAF'08), Manchester, UK, 24 August 2008, first version.
Existential implications of transitive verbs: a preliminary classification for textual inference (with Patricia Amaral, Cleo Condoravdi and Annie Zaenen), manuscript, June 2008.
Consequence-informed access control, (with Jessica Staddon), short note for Xerox Innovation Group (XIG) Research and Technology Conference, May 2008.
Deverbal Nouns in Knowledge Representation. (with Olga Gurevich, Richard S. Crouch, Tracy H. King) J. Log. Comput. 18(3): 385-404 (2008).

An Institutional View of Categorical Logic and the Curry-Howard-Tait Isomorphism (with Joseph Goguen, Till Mossakowski, Florian Rabe, and Lutz Schröder). In Int J Software Informatics, 1 (1), pp. 129–152, 2007.
PARC's Bridge and Question Answering System (with Daniel G. Bobrow, Bob Cheslow, Cleo Condoravdi, Lauri Karttunen, Tracy H. King, Rowan Nairn, Charlotte Price and Annie Zaenen). Proceedings of Grammar Engineering Across Frameworks, pp 26--45, 2007.
Hylo 2007 Proceedings of the Workshop (editor with Patrick Blackburn, Thomas Bolander, Torben Brauner, Joergen Villadsen). Electr. Notes Theor. Comput. Sci. 174(6): 1-2 (2007).

Textual Inference Logic: Take Two, (with D. G. Bobrow, C. Condoravdi, R. Crouch, L. Karttunen, T. H. King, R. Nairn and A. Zaenen) Proceedings of the Workshop on Contexts and Ontologies, Representation and Reasoning, CONTEXT 2007.
Precision-focused Textual Inference (with Bobrow, D. G., C. Condoravdi, L. Karttunen, T. H. King, L. Price, R. Nairn, L.Price, A. Zaenen) Proceedings of ACL-PASCAL Workshop on Textual Entailment and Paraphrasing, pp. 16-21, 2007.

Constructive Description Logics: what, why and how. (extended draft) Presented at Context Representation and Reasoning, Riva del Garda, August 2006.
Constructive hybrid logics and contexts. Hybrid Logics Workshop (HYLO 2006); Invited Talk, August 11, 2006; Seattle, WA; USA.

Deverbal Nouns in Knowledge Representation (with O. Gurevich, D. Crouch, and T. H. King), Appeared in FLAIRS (The Florida Artificial Intelligence Research Society), May 11-13, 20006 and won one of the Best Paper Awards in FLAIRS (apparently there were two...).
A short note on Intuitionistic Propositional Logic with Multiple Conclusions (with Luiz Carlos Pereira) Manuscrito-- Rev Int. Fil. Campinas, v. 28, n.2, pp 317-329, jul-dez, 2005. Word version.
Preface of the special volume on Chu Spaces: theory and applications (with Vaughan Pratt), Theory and Applications of Categories, Vol. 17, 2006, No.7, pp 1-9.
Dialectica and Chu constructions: Cousins?Theory and Applications of Categories, Vol. 17, 2006, No. 7, pp 127-152.
A Parigot-style Linear Lambda-calculus for Full Intuitionistic Linear Logic (with Eike Ritter),Theory and Applications of Categories, Vol. 17, 2006, No.3, pp 30-48.
Towards Constructive Hybrid Logic (Extended Abstract) (with T. Brauner), Presented at Methods for Modalities 3, LORIA, Nancy, France, September 22-23, 2003. Also appears as a technical report from the University of Roskilde, 2003.
Full paper from above, submitted with new title Intuitionistic Hybrid Logic to Journal of Applied Logic(JAL). Appeared as JAL 4(2006), 231-- 255, available online from the publishers on 11th August 2005. Apparently it got to be the 2nd hottest paper from that journal, but it has now disappeared from the hot spot..

Constructive CK for Contexts (with Michael Mendler), In Proceedings of the Worskhop on Context Representation and Reasoning, Paris, France, July 2005.
A Basic Logic for Textual inference (with D. Bobrow, C. Condoravdi, R. Crouch, R. Kaplan, L. Karttunen, T. King and A. Zaenen), In Procs. of the AAAI Workshop on Inference for Textual Question Answering, Pittsburgh PA, July 2005.
Constructive CK for Contexts (with Michael Mendler), Abstract in the ASL Meeting in Stanford, March 2005.
Equivalence of Logics: the categorical proof theory perspective Abstract of an Invited Talk at Universal Logic, March 2005.
Relating Algebraic Models of Intuitionistic Predicate Logic (with Milly Maietti) Abstract of talk presented at Universal Logic 2005.
Relating Categorical Semantics for Intuitionistic Linear Logic (with P. Maneggia and M. Maietti and E. Ritter), Invited Talk at Natural Deduction 2001, Rio de Janeiro. Journal paper in Applied Categorical Structures, volume 13(1):1--36, 2005.
Towards constructive description logics. Talk at the Workshop on Intuitionistic Modal Logics and Applications (IMLA2005), associated with LiCS 2005.

Intuitionistic Modal Logic and Application (Special Issue) Journal of Logic and Computation, volume 14, number 4, August 2004. Guest Editors: Valeria de Paiva, Rajeev Gore' and Michael Mendler. The (long) preface is below.
Modalities in Constructive Logics and Type Theories Preface to the special issue on Intuitionistic Modal Logic and Application of the Journal of Logic and Computation, volume 14, number 4, August 2004. Guest Editors: Valeria de Paiva, Rajeev Gore' and Michael Mendler.
Logics of Context and Modal Type Theories. Mathematical Foundantions of Programming Semantics (Talk); 2004 May; Pittsburgh; PA; USA.

Poset-valued sets, or, How to build models for Linear Logic (with Andrea Schalk), Theoretical Computer Science 315 (2004) 83-107, (submitted 1998).
Natural Deduction and Context as (Constructive) Modality. In Modeling and Using Context, Proceedings of the 4th International and Interdisciplinary Conference CONTEXT 2003, Stanford, CA, USA, Springer Lecture Notes in Artificial Intelligence, vol 2680, June 2003.
Entailment, Intensionality and Text Understanding (with Cleo Condoravdi, Richard Crouch, Reinhard Stolle, Daniel G. Bobrow.) Proceedings Human Language Technology Conference (HLT-NAACL-2003), Workshop on Text Meaning, Edmonton, Canada, May 2003.
Knowledge Tracking: Answering Implicit Questions. (with Reinhard Stolle, Daniel Bobrow, Cleo Condoravdi, Richard Crouch) Proceedings AAAI Spring Symposium on New Directions in Question Answering, Stanford, California, March 2003.
Flattened Semantic Representations (with Daniel Bobrow, Cleo Condoravdi, Richard Crouch and Reinhard Stolle.) Abstract accompanying a talk at the Stanford Semantics and Pragmatics Workshop, Stanford, California, March 2003.
Intuitionistic Modal Logic and Applications (IMLA'02) Workshop Proceedings. (eds. R. Gore, M. Mendler and V. de Paiva). Technical Report from the University of Bamberg, Germany, July 2002.
Normalization Bounds in Rudimentary Linear Logic (with M. Maietti and E. Ritter), presented at the Workshop on Implicit Computational Complexity, FLoC'02, Copenhagen, 2002. Also technical report of the University of Padova, Italy, 2002.
Lineales: algebras and categories in the semantics of Linear Logic. Presented at LLC8, Stanford, May 1999. Revised version (June 2000) appears in CSLI book "Words, Proofs, and Diagrams" (eds. D. Barker-Plummer, D. Beaver, Johan van Benthem and P. Scotto di Luzio), 2002. Original version Lineales: Algebraic Models of Linear Logic from a Categorical Perspective.
Scalability of redundancy detection in focused document collections. (with Richard Crouch, Cleo Conodoravdi, Reinhard Stolle, Tracy King, John Everett & Daniel Bobrow) Proceedings of Workshop on Scalability in Natural Language Understanding (ScaNaLU), Heidelberg, 2002.
Making Ontologies Work for Resolving Redundancies Across documents (with J. Everett and D. Bobrow and C. Condoravdi and D. Crouch and M. van der Berg and L. Polanyi), in "Communications of the ACM", February 2002, vol 45, number 2.
Finding Similar Content within Different Documents (with J. O. Everett, D. G. Bobrow, C. Condoravdi, R. Crouch and R. Stolle), in Mining Answers from Texts and Knowledge Bases, Papers from 2002 AAAI Spring Symposium, Eds. Sanda M. Harabagiu and Vinay Chaudhri, 2002.

Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic (with G. Bellin and E. Ritter), In Methods for Modalities 2001, Amsterdam, November 2001. (pdf)
Preventing Existence (with C. Condoravdi, D. Crouch, J. Everett, R. Stolle, D. Bobrow, M. van den Berg), In Proceedings of Formal Ontology in Information Systems, FOIS'01, October 2001 (this is a preliminary version of the paper).
Categorical and Kripke Semantics for Constructive S4 Modal Logic (with Natasha Alechina and and Michael Mendler and Eike Ritter). In Proc. of Computer Science Logic (CSL'01), LNCS 2142, ed L. Fribourg. 2001. (This is a corrected version of "Relating Categorical and Kripke Semantics for Intuitionistic Modal Logics" below.)
Soundness and completeness are not enough (linear type theories and their models) Invited talk. Logic, Language and Computation (10th LLC); 2001 May 26; Stanford, CA.
Abstract algebraic substructural logics (talk). Stanford University/Computer Science Dept. Theory Lunch; 2001 May 24; Stanford, CA.

On an Intuitionistic Modal Logic (with Gavin Bierman), Studia Logica (65):383-416, 2000.
Linear Explicit Substitutions (with Neil Ghani and Eike Ritter), in the Journal of the IGPL, vol 8, Issue 1, January 2000, 7-31.
Categorical Models for Linear and Intuitionistic Type Theory (with Milly Maietti and Eike Ritter), In Proceedings of FOSSACS2000: Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, Springer-Verlag, vol 1784, April 2000.
Explicit Substitutions for Linear Logical Frameworks (with Iliano Cervesato and Eike Ritter), Proc. Workshop on Logical Frameworks and Meta-Languages, September 1999.
Variations on Linear PCF (with Eike Ritter), Proc. WESTAPP-99, 1999.
Building Models of Linear Logic (with Andrea Schalk), Proc. AMAST-99, LNCS 1548, 1999.
Constructive Authentication Logics: a research proposal In PRATICA: Proofs, Types and Categories, eds. E. H. Hausler and L. C. Pereira, 1999.
Categorical Models of Explicit Substitutions (with Neil Ghani and Eike Ritter), Proc FOSSACS-99, LNCS 1578, Springer-Verlag, 1999.
Relating Categorical and Kripke Semantics for Intuitionistic Modal Logics (with Natasha Alechina and Eike Ritter). Proc. AiML II (Advances in Modal Logic), 1998. NOTE: this paper had a serious bug, which was corrected with the help of M. Mendler and M. Fairtlough. Hence it's not down-loadable any more, but see the corrected version above.
Explicit Substitutions for Constructive Necessity (with Neil Ghani and Eike Ritter), presented at 25th International Colloquium on Automata, Languages and Programming (ICALP'98). Lecture Notes in Computer Science LNCS 1443, eds. Larsen, Skyum and Winskel, 1998. This is also available as a technical report.
Linear Explicit Substitutions (with Neil Ghani and Eike Ritter). Presented at Westapp'98. Also Invited Talk at WOLLIC'98. A full version is available as Technical Report CSR-98-02 . Superseded by the paper in the Journal of the IGPL above.
Computational Types from a Logical Perspective I. (with Benton and Bierman) Journal of Functional Programming, 8(2):177-193. March 1998 .
A Formulation of Linear Logic Based on Dependency-Relations (with Torben Brauner) Proceedings of Annual Conference of the European Association for Computer Science Logic, Aarhus, Denmark, LNCS 1414, Springer-Verlag, 1997.
On Explicit Substitutions and Names (with Eike Ritter). Presented at ICALP'97, LNCS 1256 eds. Degano, Gorrieri and Marchetti-Spaccamela. Also Technical Report CSR-97-5, School of Computer Science, University of Birmingham. March 1997.
Intuitionistic Necessity Revisited. (with Gavin Bierman). Technical Report CSRP-96-10, School of Computer Science, University of Birmingham. June 1996. (Updated version of paper in Applied Logic Conference, Amsterdam, 1992. Improved version appears as Studia Logica paper, 2000.)
Cut-Elimination for Full Intuitionistic Linear Logic. (with Brauner). Technical Report 395 from Computer Laboratory, University of Cambridge and BRICS, Denmark. May 1996.
A Dialectica Model of State. (with Correa and Haeusler). In CATS'96, Computing: The Australian Theory Symposium Proceedings, Melbourne, Australia, January 1996.
Linear Logic in Isabelle (with S. Kalvala) in Proceedings of the Isabelle Users Workshop, Technical Report TR379, Computer Laboratory, University of Cambridge, September 1995.
Yet another intuitionistic modal logic (with G. Bierman) Abstract of a contributed paper in the Logic Colloquium 1994, The Bulletin of Symbolic Logic, vol 1(2), June 1995.
A New Proof System for Intuitionistic Logic (with L. C. Pereira) The Bulletin of Symbolic Logic, vol 1(1):101, 1995 (abstract).
Computational Types From a Logical Perspective I. (with Benton and Bierman) University of Cambridge Computer Laboratory Technical Report 365. May 1995.
Rewriting Properties of Combinators for Intuitionistic Linear Logic. (with Nesi and Ritter). Proceedings of the Workshop on Higher Order Algebra, Logic and Term Rewriting, HOA'93. In Volume 816 of Lecture Notes in Computer Science, Springer Verlag. 1994
The ACQUILEX LKB: An Introduction (with Copestake, Sanfilippo and Briscoe). In "Inheritance, Defaults and the Lexicon". Eds. Ted Briscoe, Valeria de Paiva and Ann Copestake. Studies in Natural Language Processing, 1993.
Types and Constraints in the LKB . In "Inheritance, Defaults and the Lexicon". Eds. Ted Briscoe, Valeria de Paiva and Ann Copestake. Studies in Natural Language Processing, 1993.
Full Intuitionistic Linear Logic (extended abstract). (with Martin Hyland). Annals of Pure and Applied Logic, 64(3), pp.273-291, 1993. pdf
A Term Calculus for Intuitionistic Linear Logic. (with Benton, Bierman and Hyland). Proceedings of the First International Conference on Typed Lambda Calculus. In Volume 664 of Lecture Notes in Computer Science, Springer Verlag. 1993
Linear lambda-calculus and Categorical Models Revisited. (with Benton, Bierman and Hyland). Proceedings of Sixth Conference on Computer Science Logic. In Volume 702 of Lecture Notes in Computer Science, Springer Verlag. 1993
Intuitionistic Necessity Revisited (extended abstract). (with Bierman). In Proceedings of Applied Logic Conference, December 1992. Second version in PRATICA: Proofs, Types and Categories, edited by Hermann Hausler and Luiz Carlos Pereira, 1999.
Term Assignment for Intuitionistic Linear Logic. (with Benton, Bierman and Hyland). Technical Report 262, University of Cambridge Computer Laboratory. August 1992.
Lineales. (with J.M.E. Hyland) In "O que nos faz pensar" Special number in Logic of "Cadernos do Dept. de Filosofia da PUC", Pontificial Catholic University of Rio de Janeiro, Abril 1991.
A Dialectica-like Model of Linear Logic.In Proceedings of Category Theory and Computer Science, Manchester, UK, September 1989. Springer-Verlag LNCS 389 (eds. D. Pitt, D. Rydeheard, P. Dybjer, A. Pitts and A. Poigne).
The Dialectica Categories. In Proc of Categories in Computer Science and Logic, Boulder, CO, 1987. Contemporary Mathematics, vol 92, American Mathematical Society, 1989 (eds. J. Gray and A. Scedrov)

Book

Inheritance, Defaults and the Lexicon

review.

Drafts, Technical Reports and Loose Ends

Categorical Proof Theory and Linear Logic. Preliminary notes for a lecture course. This course was taught four times: first at PUC-RJ, Brazil, then as a graduate course in the Computer Lab, Cambridge, then at the European Summer School on Language, Logic and Information (ESLLI), in Prague (1996) and finally at School of Computer Science, Birmingham, UK (1997).
Linear Logic and Applications R. Crouch, Josef van Genabith, V. de Paiva and E. Ritter (editors) Dagstuhl-Seminar-Report, 248, IBFI gem GmbH, Schloss Dagstuhl, D-66687 Wadern, Germany, ISSN 0940-1121, 22.08.99-27.08.99.
Mini-colloquium on Linear Logic for Natural Language Dick Crouch, Josef van Genabith, Mark Hepple and Valeria de Paiva. School of Computer Science, University of Birmingham, B15 2TT, School of Computer Science Technical Reports, CSR-97-6, May 1997.
A Dialectica Model of the Lambek Calculus. This paper was presented at the Amsterdam Colloquium, 1990. I believe the version here is identical to the one in the proceedings, but I'm not absolutely sure.
Cut-elimination for Full Intuitionistic Linear Logic (with Torben Brauner) Technical Report 395, University of Cambridge, Computer Laboratory, May 1996.
Proceedings of the ACQUILEX Workshop on Default Inheritance in the Lexicon. Ted Briscoe, Ann Copestake and Valeria de Paiva Technical Report 238 from Computer Laboratory, University of Cambridge. October 1991.
A Linear Specification Language for Petri Nets. (with C. Brown and D. Gurr) Technical Report 363 from Computer Science Department, University of Aarhus, Denmark, October 1991.
Categorical Multirelations, Linear Logic and Petri Nets. Technical Report 225 from Computer Laboratory, University of Cambridge. June 1991.
The Dialectica Categories. Technical Report 213 from Computer Laboratory, University of Cambridge. January 1991.
Subtyping in Ponder. Technical Report 203 from Computer Laboratory, University of Cambridge. August 1990.
Categorical Modelling of a State Oriented version of Linear Logic by Alex Tucker, ex Ph. D student, 1998.