This page is no longer updated, the new one is here

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.

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.

- Proof Theory Group at TU Dresden (people, publications, events, funding and resources)
- Kai Brünnler (papers)
- Alessio Guglielmi (papers)
- Ozan Kahramanogullari (papers and implementations)
- Charles Stewart (papers)
- Lutz Straßburger (papers)
- Alwen Tiu (papers)
- ProofTheory.ORG
- Proof theory mailing list
- The frogs mailing list (this list is specifically devoted to deep inference, structads, the calculus of structures, proof nets and other amphibians of structural proof theory)

*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)

- 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

- Logik

- Linguaggi Formali e Compilatori (CdL Scienze dell'Informazione, Cesena AA 1993)
- Metodi per il Trattamento dell'Informazione (CdL Scienze dell'Informazione, Cesena AA 1993)

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

*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

*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

- 17. WLP: Workshop Logische Programmierung, Dresden, December 11-13, 2002.

*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.

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.

*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.

- In ICLP 93 Post-Conference Workshop on Logic Programming with Sets, Budapest, Hungary, 1993

(Distributed among participants).

*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).

*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.

*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

Computer Science Department

University of Bath

Bath BA2 7AY

UK

Fax: +44 (0870) 7052029, or please send me an email.

26.3.2006Paola Bruscoliemail