Research Fellow at University of Bath (EPSRC Project: Efficient and Natural Proof Systems).

Previously, I have been: Substitute Professor in Computational Logic, at the International Center for Computational Logic, TU Dresden; Researcher (in the Project ANR-Démosthène) at INRIA Nancy-Grand Est; Research Fellow at the University of Bath; and before that, I spent many years as researcher at the International Center for Computational Logic in Dresden, where I also taught for the International Masters Programme in Computational Logic.

- Curriculum Vitae
- Research
- Esteem
- Teaching
- Organisation of Events
- Publications
- Public Service
- Postal Address

A short CV is here.

- Computer Science Logic 2013 - Turin, PC Member
- EPSRC ICT Panel Member, February 2013
- EPSRC Proposal Reviewer (2012, 2009, 2008)
- Audit for the Internationalisation Process, TU Dresden, May 2011, interviewee
- CL&C'08 (co-located with ICALP) - Reykjavik, PC Member
- Structures and Deduction 2005 (co-located with ICALP) - Lisbon, PC Member and co-editor

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 deep inference: the calculus of structures is a proof theoretical formalism, employing deep inference, originally conceived by Alessio Guglielmi and further developed by our research group in Dresden. These initial investigations have evolved a lot along the years, of course: find more on deep inference and current research topics.

Recently, my investigations are more focused on complexity of proofs in deep inference based formalisms.

- Deep Inference site (including people, publications, events, funding and resources)
- EPSRC- Project EP/K018868/1: Efficient and Natural Proof Systems (2013-2016)
- ANR-Project Démosthène site
- INRIA - Action de Recherche Collaborative 2009 Project REDO site
- Kai Brünnler
- Alessio Guglielmi
- Tom Gundersen
- Ozan Kahramanogullari (papers and implementations)
- François Lamarche
- Richard McKinley
- Luca Roversi
- Lutz Straßburger
- Alwen Tiu (papers)
- Proof theory mailing list
- The frogs mailing list (specifically devoted to deep inference, structads, the calculus of structures, proof nets and other amphibians of structural proof theory)

Structural Proof Theory and Abstract Logic Programming

Selected Topics in Proof Theory (seminar)

Foundations of Logic Programming

Foundations of Constraint Programming

Structural Proof Theory and Abstract Logic Programming

Selected Topics in Proof Theory (seminar)

Programmation Java

Instructor for the group X' (Friday morning , Room 418). Further information for the group available here.

C2I-niveau 2 (Certificat d'Informatique et Internet)

Mandatory course (second part) for (almost) all first year students at Nancy Universities, I am the instructor for the groups Droit-Eco-04 and Droit-A05. Find here more information on the the certificate (in french).

C2I-niveau 1 (Certificat d'Informatique et Internet)

Mandatory course for (almost) all first year students at Nancy Universities, I am the instructor for the groups LEA 2 and Droit 9. Find here more information on the the certificate (in french).

Introduction to Deep Inference and Proof Nets.

Taught with Lutz Straßburger at Technische Universität Dresden (17-21 Dec 2007).

Some slides on the first two lectures.

- Introduction to Sequent Calculus and Abstract Logic Programming: during SS2004, SS2005
- 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

- ReDo: Redesigning Logical Syntax -- Bath, 14 -- 16 September 2010
- Geometric and Logic Approaches to Computation — Nancy, 23 - 24 February 2010
- ReDo: Redesigning Logical Syntax — Nancy, 16 - 18 November 2009
- Proof Theory Meeting — Bath, 6 - 8 July 2006
- 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 Workshop on Proof Theory — Dresden, 21 - 23 February 2005
- ICCL Workshop on Proof Theory — Dresden, 27 - 28 September 2004
- 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 22 November 2005

Theoretical Computer Science 360 (1–3) 2006, pp. 42–76

Technical Report WV-03-10, 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.

*On Analytic Inference Rules in the Calculus of Structures*

Paola Bruscoli and Alessio Guglielmi

- We discuss the notion of analytic inference rule for propositional logics in the calculus of structures.
- Pdf 15 September 2007.

Unpublished note.

*On Analyticity in Deep Inference*

Paola Bruscoli and Alessio Guglielmi

- A refinement of the previous unpublished note, work in progress, to be submitted soon.
- Pdf 25 November 2009.

Unpublished note.

*On the Proof Complexity of Deep Inference*

Paola Bruscoli and Alessio Guglielmi

- We obtain two results about the proof complexity of deep inference: 1) deep-inference proof systems are as powerful as Frege ones, even when both are extended with the Tseitin extension rule or with the substitution rule; 2) there are analytic deep-inference proof systems that exhibit an exponential speed-up over analytic Gentzen proof systems that they polynomially simulate.
- Pdf April 19, 2009

ACM Transactions on Computational Logic 10 (2:14) 2009, pp. 1–34 - Extended abstract presented at PCC'07

*Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae
*Paola Bruscoli, Alessio Guglielmi, Tom Gundersen and Michel Parigot

- Jerábek showed that analytic propositional-logic deep-inference proofs can be constructed in quasipolynomial time from nonanalytic proofs. In this work, we improve on that as follows: 1) we significantly simplify the technique; 2) our normalisation procedure is direct, i.e., it is internal to deep inference. The paper is self-contained, and provides a starting point and a good deal of information for tackling the problem of whether a polynomial-time normalisation procedure exists.
- Preliminary version of this work was presented at PCC'08.
- Pdf 31 March 2009

Work in progress, almost ready for submission.

*A Quasipolynomial Cut Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae
*Paola Bruscoli, Alessio Guglielmi, Tom Gundersen and Michel Parigot

- Jerábek showed in 2008 that cuts in propositional-logic deep-inference proofs can be eliminated in quasipolynomial time. The proof is an indirect one relying on a result of Atserias, Galesi and Pudlák about monotone sequent calculus and a correspondence between this system and cut-free deep-inference proos. In this paper we givea direct proof of Jerábek's result: we give a quasipolynomial-time cut-elimination procedure in propositionl-logic deep-inference. The main new ingredient is the use of a computational trace of deep-inference proofs called atomic flows, which are both very simple (they trace only structural rules and forget logical rules) and strong enough to faithfully represent the cut-elimination procedure.
- Pdf January 2010 (submitted version)

Accepted at LPAR 16.

*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

University of Bath

Computer Science Dept

Claverton Down

BA2 7AY Bath

United Kingdom

.. or please send me an email.

1.2.2013Paola Bruscoliemail