This page is no longer updated, the new one is here
Paola Bruscoli
I'm a visiting researcher at University of Bath, after having spent many years at the International Center for Computational Logic in Dresden, where I taught for the International Masters Programme in Computational Logic. I'm also a wife, mother of two daughters and owner of a cat.
Contents
Research
My research interests focus on structural proof theory, substructural logics and their application in the design of logical languages for planning and concurrency, logic programming, concurrency, and more in general mathematical foundations of language design and theoretical computer science.
I'm interested in the calculus of structures, a proof theoretical formalism employing deep inference, originally conceived by my husband Alessio Guglielmi and further developed by our group. I also am interested in the proof theory of the sequent calculus.
Related Links
Teaching
For students of the summer semester 2005
Introduction to Sequent Calculus and Abstract Logic Programming
References:
Good pointers to books, tutorials, papers on the web can be found from the ProofTheory.org site. Some of these books are available in our library. I'm also using the following papers, available on the web:
- J. Gallier: Constructive Logics. part 1: A Tutorial on Proof Systems and Typed Lambda-Calculi (on the web)
- Miller, Nadathur, Pfenning, Scedrov: Uniform proofs as a Foundation for Logic Programming. Annals of Pure and Applied logic, 1991 (51) p. 125-157.
Some students have asked for the transparencies used during the course (they might very well have typos):
- Cut elimination for LK (refer to Gallier's presentation): b/w handwritten pdf
- A Tutorial on Proof Theoretic Foundations of Logic Programming: color handwritten pdf
- Auxiliary very sketchy notes on linear logic and Forum (please refer to Girard's and Miller's papers)
Courses for the International Masters Programme in Computational Logic
- Introduction to Sequent Calculus and Abstract Logic Programming: during SS2004
- Inductive Logic Programming and Bioinformatics (as assistant of Steffen Hölldobler): during WS2000/01
- Special Topics in Computational Logic (as assistant of Steffen Hölldobler): during SS2000
- Selected Topics in Proof Theory (co-responsible with Alessio Guglielmi): during SS2000, SS2001, SS2002
- Substructural Logics and Proof Search (co-responsible with Alessio Guglielmi): during SS1999
- Introduction to Computational Logic (as assistant of Steffen Hölldobler): during WS1997/98, WS 1998/99, WS 1999/2000, and WS 2000/01
- Deductive Systems (compact repetition classes): during SS 1998
Courses for the Diplom-Informatik, Technische Universität Dresden
Other Courses
- Linguaggi Formali e Compilatori (CdL Scienze dell'Informazione, Cesena AA 1993)
- Metodi per il Trattamento dell'Informazione (CdL Scienze dell'Informazione, Cesena AA 1993)
Organisation of Events
I was one of the organisers of the following events
- Workshop SD'05 -- Structures and Deduction - the quest for the essence of proofs, satellite of ICALP '05, Lisbon 16--17 July 2005. (Proceedings are available here -- pdf 3.5 MB)
- ICCL Summer School on Proof Theory and Automated Theorem Proving, and Workshop on Proof Theory, Computation and Complexity — Dresden, 14 - 26 June 2004
- Summer School and Workshop on Proof Theory, Computation and Complexity — Dresden, 23 June - 4 July 2003
- Workshop on Structural Proof Theory — Dresden, 19 - 21 Nov 2003
- (Summer School and) Workshop on Proof Theory and Computation — Dresden, 3 - 14 June 2002
- Workshop on Proof Theory — Dresden, 8 Dec 2000
Publications
Proof Theory of Sequent Calculus
A Tutorial on Proof Theoretic Foundations of Logic Programming
Paola Bruscoli and Alessio Guglielmi
- Abstract logic programming is about designing logic programming languages via the proof theoretic notion of uniform provability. It allows the design of purely logical, very expressive logic programming languages, endowed with a rich meta theory. This tutorial intends to expose the main ideas of this discipline in the most direct and simple way.
- Pdf © Springer-Verlag September 10, 2003
Invited tutorial at ICLP '03, LNCS 2916, pp. 109–127, BibTeX entry
On Structuring Proof Search for First Order Linear Logic
Paola Bruscoli and Alessio Guglielmi
- Full first order linear logic can be presented as an abstract logic programming language in Miller's system Forum, which yields a sensible operational interpretation in the `proof search as computation´ paradigm. However, Forum still has to deal with syntactic details that would normally be ignored by a reasonable operational semantics. In this respect, Forum improves on Gentzen systems for linear logic by restricting the language and the form of inference rules. We further improve on Forum by restricting the class of formulae allowed, in a system we call G-Forum, which is still equivalent to full first order linear logic. The only formulae allowed in G-Forum have the same shape as Forum sequents: the restriction does not diminish expressiveness and makes G-Forum amenable to proof theoretic analysis. G-Forum consists of two (big) inference rules, for which we show a cut elimination procedure. This does not need to appeal to finer detail in formulae and sequents than is provided by G-Forum, thus successfully testing the internal symmetries of our system.
- Conference version pdf © Springer-Verlag September 10, 2003
LPAR '03, LNCS 2850, pp. 389–406, BibTeX entry
- Full paper pdf November 22, 2005
Technical Report WV-03-10, to appear on Theoretical Computer Science, BibTeX
Calculus of Structures
A Purely Logical Account of Sequentiality in Proof Search
Paola Bruscoli
- We establish a strict correspondence between the proof-search space of a logical formal system and computations in a simple process algebra. Sequential composition in the process algebra corresponds to a logical relation in the formal system—in this sense our approach is purely logical, no axioms or encodings are involved. The process algebra is a minimal restriction of CCS to parallel and sequential composition; the logical system is a minimal extension of multiplicative linear logic. This way we get the first purely logical account of sequentiality in proof search. Since we restrict attention to a small but meaningful fragment, which is then of very broad interest, our techniques should become a common basis for several possible extensions. In particular, we argue about this work being the first step in a two-step research for capturing most of CCS in a purely logical fashion.
- Pdf © Springer-Verlag August 12, 2002
ICLP 2002, LNCS 2401, pp. 302-316 (was Technical Report WV-02-06), BibTeX entry
A purely logical account of sequentiality in proof search - extended abstract
Paola Bruscoli
Language Design for Coordination and Planning
A linear logic view of Gamma style computations as proof searches
Paola Bruscoli and Alessio Guglielmi
- Using the methodology of abstract logic programming in linear logic, we establish a correct and complete translation between the language Nabla and first order linear logic. Nabla is a modification of the coordination language Gamma with parallel and sequential composition. Nabla, without modifying Gamma basic computational model, is amenable to this kind of analysis, at the price of a weaker expressive power. The translation is correct and complete in the sense that we establish a two way correspondence between computations in Nabla and the search for proofs in a suitable fragment of first order linear logic. Moreover, the translation is not an encoding, meaning that to the algebraic structure of Nabla programs is assigned logical meaning through a non-trivial use of linear logic connectives, as opposed to merely reflecting their operational behavior through a simulation into terms of the logic. In this way we hope that the connection established between the two formalisms can compensate for the diminished expressive power of Nabla with a powerful analysis tool, which could lead both to theoretical and practical improvements in semantic foundations of Gamma-style languages and in the design of efficient implementations of their interpreters. The main difficulty has been to deal with sequential composition of programs, and to smoothly integrate its logical treatment in a recursive framework. An intermediate step is the definition of the language SMR, by which it is possible to specify in a very intuitive way Nabla operational semantics, and to prove that this specification is actually equivalent to the SOS-style one derived from Gamma semantics.
- © Imperial College Press, 1996
In Jean-Marc Andreoli, Chris Hankin, and Daniel Le Metayer, editors, Coordination Programming: Mechanisms, Models and Semantics.
A linear logic programming language with parallel and sequential conjunction
Paola Bruscoli and Alessio Guglielmi
- In GULP-PRODE 95, Joint Conference on Declarative Programming, Marina di Vietri, Italy, pp. 409-420, 1995.
On Gamma style computations in abstract linear logic programming
Paola Bruscoli and Alessio Guglielmi
- In Informal Proceedings of the Fourth Compulog-Network Subgroup Meeting on Programming Languages, Marina di Vietri, Italy, 1995.
Expressiveness of the abstract logic programming language Forum in planning and concurrency
Paola Bruscoli and Alessio Guglielmi
- We talk about the expressive power of Forum, an abstract logic programming language recently proposed by Dale Miller. Forum is rich enough to directly express the whole linear logic, and it is a generalization of many existing logic programming languages. In the meantime it retains a pure proof-theoretic view of logic programming. We try to understand and use the set of connectives Forum provides from the perspective of the two diverse areas of planning and of concurrency, which have recently received many attentions by people interested in linear logic. We define a basic paradigm for planning problems, in the two cases of forward and backward search for a plan. Then we state that Forum interprets in a very natural way these two paradigms. Through examples, we show that in fact we have much more expressive power, in ways that suggest directions in which to extend the basic paradigm. Then we give a convincing interpretation, in a concurrency setting, of Forum connectives. We suggest that the concurrency features are related to the planning ones by a switch in the control mechanism of the computations: ``proof as computation'' as opposed to ``proof search as computation.''
- In GULP-PRODE 94, Joint Conference on Declarative Programming, Peniscola, Spain, volume 2, pp 221-237, 1994.
Planning and abstract logic programming: A linear logic approach
Paola Bruscoli, Alessio Guglielmi and Giorgio Levi
- In this paper we give a definition of planning problems, which is in essence multiset rewriting. Then we show that to this notion it can be given logical meaning by a language, called Forum, with the expressive power of the whole linear logic. Doing so we overcome the frame problem, and have a logic programming language to reason about planning. This logic programming language satisfies a very general criterion, namely it is complete wrt uniform proofs. Then we argue that the core paradigm of multiset rewriting can be extended in Forum, and this opens up interesting threads for future research. Meanwhile, we get an understanding of linear logic through planning.
- In XI Brazilian Symposium on Artificial Intelligence, Fortaleza, pages 285-299, 1994.
Extension of Logic Programming Languages with Set Theory
Compiling intensional sets in CLP
Paola Bruscoli, Agostino Dovier, Enrico Pontelli and Gianfranco Rossi
- Constructive negation has been proved to be a valid alternative to negation as failure, especially when negation is required to have, in a sense, an `active' role. In this paper we analyze an extension of the original constructive negation in order to gracefully integrate with the management of set-constraints in the context of a Constraint Logic Programming Language dealing with finite sets. We show that the marriage between CLP with sets and constructive negation gives us the possibility of representing a general class of intensionally defined sets without any further extension to the operational semantics of the language. The presence of intensional sets allows a definite increase in the expressive power and abstraction level offered by the host logic language.
- In Proceedings ICLP'94, Pascal Van Hentenryck ed. pp. 647-661. The MIT Press, 1994.
Extensional and intensional sets in CLP with intensional negation
Paola Bruscoli, Agostino Dovier, Eugenio Omodeo, Enrico Pontelli and Gianfranco Rossi.
Extensional and intensional sets in CLP with intensional negation
Paola Bruscoli, Agostino Dovier, Enrico Pontelli and Gianfranco Rossi.
- In Second Compulog Area Network Meeting joint with Workshop on Logic Languages, Pisa, 1993 - Progetto Finalizzato Informatica (Distributed among participants).
Semantics of Negation in Logic Programming Languages
Compilative constructive negation in constraint logic programs
Paola Bruscoli, Francesca Levi, Giorgio Levi and Maria Chiara Meo
- In this paper we define a new a compilative version of constructive negation (intensional negation) in CLP and we prove its (non-ground) correctness and completeness wrt the 3-valued completion. We show that intensional negation is essentially equivalent to constructive negation and that it is indeed more efficient, as one would expect from the fact that it is a compilative technique, with the transformation and the associated normalization process being performed once and for all on the source program. We define several formal non-ground semantics, based either on the derivation rule or on the least fixpoint of an immediate consequence operator. All these semantics are proved to correctly model the observable behavior, from the viewpoint of answer constraints. We give some equivalence theorems and we show that all our denotations are the non-ground representation of a single partial interpretation, which is exactly Kunen's semantics and therefore a 3-valued model of the completion.
- © Springer-Verlag 1994
Colloquium on Trees in Algebra and Programming, CAAP 94, Edinburgh (Scotland), LNCS 787 pp. 52-67.
Intensional negation in constraint logic programs
Paola Bruscoli, Francesca Levi, Giorgio Levi and Maria Chiara Meo
- In GULP 93, Proceedings of the 8th Italian Conference on Logic Programming, Gizzeria Lido, Italy, pages 359-373. Mediterranean Press s.r.l, Via S. Pellico 13, 87030 Rende (CS), Italy, 1993.
Intensional negation in constraint logic programs
Paola Bruscoli, Francesca Levi, Giorgio Levi and Maria Chiara Meo
- In Second Compulog Area Network Meeting joint with Workshop on Logic Languages, Pisa, 1993 (Distributed among participants).
Intensional negation in CLP
Paola Bruscoli, Francesca Levi, Giorgio Levi and Maria Chiara Meo
- Technical Report TR 11/93, Dipartimento di Informatica, Università di Pisa, Italy, 1993.
Other Material
Note sulla semantica denotazionale del linguaggio imperativo IMP
Paola Bruscoli
- Course Notes for Metodi per il Trattamento dell’Informazione, Cesena 1993 (in Italian).
Linear Logic for Spatial and Temporal Reasoning - Proof Search and Partial Order Planning
Paola Bruscoli
- PhD thesis, University of Ancona (Italy), 1997
Postal Address
Computer Science Department
University of Bath
Bath BA2 7AY
UK
Fax: +44 (0870) 7052029, or please send me an email.
Paola Bruscoli