Daniel Méry

Position

Research Interests

Currently working in the field of resource logics, and more particularly BI, the Logic of Bunched Implications, with Didier Galmiche.
More precisely, I'm interested in proof-search, automated deduction, semantics and counter-model construction.

Publications

D. Galmiche and D. Méry Characterizing Provability in BI's Pointer Logic through Resource Graphs. paper (ps) slides (pdf) slides (ps)
LPAR'05, Montego Bay, Jamaica, December 2005.

D. Galmiche and D. Méry The Semantics of BI and Resource Tableaux.
Mathematical Structures in Computer Science, December 2005.

D. Méry Preuves et Sémantiques dans des Logiques de Ressources. ps pdf
Mémoire de thèse de l'Université Henri Poincaré, Nancy 1, Novembre 2004.

D. Galmiche and D. Méry Resource Graphs and Countermodels in Resource Logics.
Workshop on Disproving, Non-Theorem, Non-Validity, Non-Provability,
Cork, Ireland, July 2004.

D. Galmiche and D. Méry Semantic Labelled Tableaux for propositional BI (without bottom).
Journal of Logic and Computation, vol. 13, n. 5, October 2003.

D. Galmiche, D. Méry and D. Pym Resource Tableaux (extended abstract).
Int. Conference on Computer Science Logic, CSL 2002,
Edinburgh, Scotland, September 2002.

D. Galmiche and D. Méry Connection-based proof search in propositional BI logic.
Int. Conference on Automated Deduction, CADE 2002,
Copenhagen, Denmark, July 2002.

D. Galmiche and D. Méry Proof-search and Countermodel Generation in Propositional BI Logic.
International Symposium on Theoretical Aspects of Computer Software, TACS 2001,
Tohoku University, Sendai, Japan, October 2001.

The BILL Theorem Prover

A first version of a theorem prover for propositional BI, based on BI's labelled semantic tableaux, is available here.

Daniel Méry
LORIA UMR 7503 - UHP Nancy 1
Campus Scientifique - BP 239
54506 Vandoeuvre-lès-Nancy, France
Email: Daniel.Mery@loria.fr
Homepage: http://www.loria.fr/~dmery