FibLog: 
Fibring Logics

FCT Project FEDER POCTI/2001/MAT/37239 (January 1, 2002 - December 31, 2004)

• Final Report February 2005
• Result of intercalary evaluation by FCT in early 2004

A project of CLC on fibring and other constructions for combining logics with applications to the development of mixed logics. The problem of combining logics has been a recent target of research. At CLC work is directed at establishing preservation results about fibring, the most powerful form of combination originally proposed by Dov Gabbay. The theoretical significance of fibring results from the fact that, once a completeness preservation result is established, the completeness of a logic is obtained by recognizing it as a fibring of simpler complete logics. Preservation by fibring of completeness and other important properties is being investigated at CLC for a wide class of logics, encompassing higher-order, modal, relevance and non-truth-functional logics, possibly endowed with labeled deductive systems and using a novel topos-theoretic semantics. Research is also directed at refining the notion of fibring in order to solve the collapsing problem identified by Fariñas del Cerro. The relevance of fibring is recognized in software engineering and knowledge representation where working with several logics at the same time is common. Research at CLC is also directed at probabilistic logics, as well as at applications to the analysis of security protocols, with current emphasis on authentication, secure computation and zero knowledge proof protocols.

Relevant papers and theses

• List and preprints

Workshop

• Workshop on Combination of Logics: Theory and Applications (CombLog'04)

Core team

• Amílcar Sernadas (Coordinator)
• Carlos Caleiro
• Cristina Sernadas
• Jaime Ramos
• João Rasga
• Paulo Mateus
• Luís Cruz-Filpe [since February 2004]

Tasks (ongoing and envisaged) and partners

• Homogeneous fibring
  • Fibring of first-order based logics (01)
  • Fibring of labelled deductive systems (02)
  • Fibring of non verum functional logics (03)
  • Fibring of higher-order based logics with topos semantics (01,03)
• Avoiding collapses
  • Modulated fibring (03)
  • Cryptofibring
• Heterogeneous fibring
  • Fibring logics with deductive systems of different kinds (02)
  • Fibring logics with semantics of different kinds (04)
  • Fibring versus institutions (05)
• Preservation results
  • Strong completeness (01,02)
  • Weak completeness (09)
  • Decidability and finite model property (09)
  • Interpolation (01)
• Labelled deduction
  • Natural deduction labelled with truth-values (02)
  • Labelled sequent calculi for modal logic (02)
  • Hybrid logic over truth values (08)
• Topological properties
  • Continuity of fibring (09)
• Applications
  • Security logics
    • Authentication (02)
    • Secure computation (06)
  • Spatial logics (07)
  • Fault tolerance logics (05)
  • Probabilistic and quantum logic
• Book project on composing and decomposing logics (03,10)
  • Combining logic systems: Why, how, what for?

(01) with Alberto Zanardo (U Padova, Italy) - photo taken on December 15, 2000
(02) with David Basin and Luca Viganò (ETH, Switzerland)- photo taken on September 10, 2002, photo taken on September 13, 2002
(03) with Walter Carnielli and Marcelo Coniglio (U Campinas, Brazil) - photo taken on March 6, 2002, photo taken on July 31, 2002
(04) with Razvan Diaconescu (Simion Stoilow Intitute, Romania) and Petros Stefaneas (NTU Athens, Greece)
(05) with Joseph Goguen (U California at San Diego, USA)
(06) with Andre Scedrov (U Pennsylvania, USA) and John Mitchell (Stanford U, USA)
(07) with Luís Caires (UN Lisboa)
(08) with Carlos Areces and Patrick Blackburn (INRIA Lorraine, France)
(09) with Marcelo Finger (U São Paulo, Brazil)
(10) with Dov Gabbay (King's College, UK)

Last update: March 7, 2005.