Publications and Technical Reports

Books

• S. Cerrito. Logique pour l'Informatique : une introduction à la déduction automatique, Vuibert Publisher Co, october 2008, pp 1-178.




Book's Chapters

• S. Cerrito. Negation and Linear Completion. Intensional Logic for Programming, Studies in Logic and Computation, L. Farinas and M. Penttonen (eds.),pages 155-194, Clarendon Press Oxford 1992.


• S. Cerrito and Marta Cialdea-Mayer. Labelled Tableaux for Linear Time Temporal Logic over Finite Time Frames. In : Labelled Deduction , D. Basin, M.D'Agostino, D.M. Gabbay, L, Vigano (eds), Kluwer 2000. ( Page of Labelled Deduction)




Journals

• S. Cerrito and M. Cialdea-Mayer, An efficient approach to nominal equalities in hybrid logic tableaux, JANCL 2009, Hermes-Lavoisier Technical reports related to this work can be found below.


• N.Bidoit and S.Cerrito and V.Thion A first step toward modelling semistructured data in hybrid multi-modal logic, JANCL, vol. 14, No. 4, pages 447-475, 2004, Hermes-Lavoisier . pdf file .


• S.Cerrito and D. Kesner. Pattern Matching as Cut Elimination, Theoretical Computer Science (TCS), Vol. 323, pages 71-127, 2004. postcript gzipped file


• M. Cialdea-Mayer and S.Cerrito. Ground and Free-Variable Tableaux for Variants of Quantified Modal Logic. Studia Logica, special issue on Analityc Tableaux (2000), 69:97-131, 2001. Kluwer, Dordrech.
( postcript file)

• V. Benzaken, S.Cerrito and S. Praud. Static verification of dynamical integrity constraints : a semantics based approach. Networking and Information Systems Journal (NIS) , (1999). Hermes.
( postcript file)

• S. Cerrito and M. Cialdea-Mayer. A polynomial translation of S4 into T and contraction free tableaux for S4. Logic Journal of the IGPL, 5(2):287--30, Oxford University Press, 1997 ( postcript file ),


• N. Bidoit, S. Cerrito and Ch. Froidevaux. A Linear Logic Approach to Consistency Preserving Updates, Journal of Logic and Computation , 6(3):441--463, Oxford University Press, 1996.
  ( postcript file )


• S.Cerrito. A Linear Axiomatization of Negation as Failure. Journal of Logic Programming, 1992 12(1), 1992
  



Conferences and Workshops

• M. Cialdea-Mayer and S. Cerrito. Herod and Pilate: two tableau provers for basic hybrid logic. System Description in International Joint Conference on Automated Reasoning (IJCAR 2010) Herod's page .


• N. Bidoit, S. Cerrito and V. Thion. Un premier pas vers la modèlisation des donnés semi-structurées par la logique modale hybride. Actes de BDA2003, Lyon, october 2003.


• V. Thion, S. Cerrito and M. Cialdea-Mayer. A General Theorem Prover for Quantified Modal Logics. Tableaux 2002 (FLOC 2002) Copenhaghen, july 2002.


• S. Cerrito and M. Cialdea-Mayer Free-Variable Tableaux for Constant-Domain Quantified Modal Logics. In International Joint Conference on Automated Reasoning , ,(IJCAR 2001). LNAI 2083, Springer-Verlag, pp. 137-151 ( postcript file )


• M. Cialdea-Mayer and S. Cerrito. Variants of First-Order Modal Logics. In R. Dyckhoff (ed.), Automated Resoning with Analytic Tableaux and Related Methods (Tableaux 2000). LNCS, Springer-Verlag. ( postcript file )


• S.Cerrito, M. Cialdea-Mayer and S. Praud. First Order Linear Temporal Logic over Finite Time Structures. Proceedings of the 6th International Conference on Logic for Programming and Automated Reasoning (LPAR'99), Tblisi, Georgia,September 99. LNAI, Springer-Verlag. ( postcript file)


• S. Cerrito and D. Kesner. Pattern Matching as Cut Elimination : Extended Abstract. Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS99), Trento, Italy, july 1999. ( postcript file) )


• V. Benzaken, S. Cerrito and S. Praud. Vérification Statique de Contraintes d'Integrité Dynamiques. Actes de BDA99, Bordeaux, october 99. ( postcript file ),


• S. Cerrito and M. Cialdea-Mayer. Using Temporal Logic to Model and Solve Planning Problems. In F. Giunchiglia, editor, Proceedings of the 8th International Conference on Artificial Intelligence Methodology (AIMSA), September 1998, LNCS vol. 1480, Springer-Verlag.


• S. Cerrito and M. Cialdea-Mayer. Bounded Model Search in Linear Temporal Logic and Its Application to Planning. In H. de Swart, editor, Proceedings of the 7th International Conference on Theorem Proving with Analytic Tableaux and Related Methods (Tableaux '98), May 1998, LNCS vol. 1397, Springer-Verlag.


• S. Cerrito and M. Cialdea-Mayer. Hintikka Multiplicities in Matrix Decision Methods. In D. Galmiche, editor, Proceedings of the 6th Int. Conference on Theorem Proving with Analytic Tableaux and Related Methodds (Tableaux '97), May 1997, LNCS vol. 1227, Springer-Verlag.
  ( postcript file )
• S. Cerrito, A. Cesta and M. Cialdea Mayer Planning as model construction in linear temporal logic. In Technical Report RT-DIA-23-97, {Dipartimento di Informatica ed Automazione, Universitá Roma Tre, Presented as a poster session at IJCAI-97. ( poster )


• N. Bidoit, S. Cerrito and Ch. Froidevaux. Consistency Preserving Updates. Proceedings of the Post-ILPS'94 Workshop on Uncertainty in Databases and Deductive Systems, 1994, published as Technical Report, Department of Computer Science, Concordia University.


• S. Cerrito.Herbrand Methods for Sequent Calculi. Proceedings of the Joint International Conference and Symposium on Logic Programming , Octobre 1992, The MIT Press. ( postcript file ),


• S. Cerrito. A Linear Semantics for Allowed Logic Programs. Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS90), June 1990, IEEE Computer Society Press..


• S. Cerrito. An Application of Linear Logic to Logic Programming. In Abstracts of Logic Colloquium'88. August 1988, Technical Report, Universitá di Padova
  




Others

• Tutorial for the international conference "Tableaux 2007". S. Cerrito, Logics for Reasoning on Web Information. Tutorial for the international conference "Tableaux 2007".




Recent Technical Reports and Drafts

• S. Cerrito and M. Cialdea Mayer, Tableaux with Substitution for Hybrid Logic with the Global and Converse Modalities , Technical Report, Dipartimento di Informatica e Automazione, Universit\`a di Roma Tre,2009, RT-DIA-155-2009
  
• M. Cialdea Mayer, S. Cerrito, E. Benassi, F. Giammarinaro, F. and C. Varani, Two tableau provers for basic hybrid logic , Technical Report, Dipartimento di Informatica e Automazione, Universit\`a di Roma Tre,2009, RT-DIA-145-2009
  
• S. Cerrito and M. Cialdea Mayer, Terminating Tableau for H(@) without loop-checking. Rapport IBISC, 2007




Dissertations

• Contribution de la Logique Linéaire au Probleme de la Négation par Echec , Thèse présentée pour obtenir le titre de docteur es sciences, Université Paris XI, june 1990.



• Systèmes de Preuve á la Gentzen et leur Contenu Algorithmique , Memoire d'Habilitation à Diriger les Recherches, Paris XI, octobre 2000. ( postcript file)
  




Back to my home page