Previous Up

References

[BC96]
Alexandre Boudet and Hubert Comon. Diophantine equations, Presburger arithmetic and finite automata. In Hélène Kirchner, editor, Colloquium on Trees in Algebra and Programming (CAAP'96), pages 30–43. Springer Verlag LNCS 1059, 1996.

[GL04]
Jean Goubault-Larrecq. Une fois qu'on n'a pas trouvé de preuve, comment le faire comprendre à un assistant de preuve ? In Actes 15èmes journées francophones sur les langages applicatifs (JFLA 2004), Sainte-Marie-de-Ré, France, Jan. 2004, pages 1–40. INRIA, collection didactique, 2004.

[GL06a]
Jean Goubault-Larrecq. Determinizing alternating tree automata, and models. Information Processing Letters, 2006. Submitted.

[GL06b]
Jean Goubault-Larrecq. Implementing H1 by resolution. Journal of Automated Reasoning, 2006. Submitted.

[Gou05]
Jean Goubault-Larrecq. Deciding H1 by resolution. Information Processing Letters, 95(3):401–408, August 2005.

[NNS02]
Flemming Nielson, Hanne Riis Nielson, and Helmut Seidl. Normalizable Horn clauses, strongly recognizable relations and Spi. In Proc. 9th Static Analysis Symposium, pages 20–35. Springer Verlag LNCS 2477, 2002.

Previous Up