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.