Paola Bruscoli
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.
Contents
Curriculum Vitae
A short CV is here.
Esteem
-
- 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
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 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.
Related Links
Teaching
Courses at TUD, European MSc Programme in Computational Logic (Summer Semester 2012)
Deductive Systems
Structural Proof Theory and Abstract Logic Programming
Selected Topics in Proof Theory (seminar)
Courses at TUD, European MSc Programme in Computational Logic (Winter Semester 2011/2012)
Foundations of Logic Programming
Foundations of Constraint Programming
Logic Programming Engineering
Courses at TUD, European MSc Programme in Computational Logic (Summer Semester 2011)
Deductive Systems
Structural Proof Theory and Abstract Logic Programming
Selected Topics in Proof Theory (seminar)
Courses at ENS des Mines, Nancy
Programmation Java
Instructor for the group X' (Friday morning , Room 418). Further information for the group available here.
Courses at Université de Nancy 2
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).
Course as Guest Lecturer
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.
Courses at University of Bath
Courses for the International Masters Programme in Computational Logic
- 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
Courses for the Diplom-Informatik, Technische Universität Dresden
Other Old 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
- 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
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. 109127, 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. 389406, BibTeX entry
- Full paper pdf 22 November 2005
Theoretical Computer Science 360 (13) 2006, pp. 4276
Technical Report WV-03-10, 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 systemin 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
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.
Proof Complexity and Deep Inference
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. 134
- 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.
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
Public Service
Postal Address
University of Bath
Computer Science Dept
Claverton Down
BA2 7AY Bath
United Kingdom
.. or please send me an email.