References

1. Frédéric Blanqui, Jean-Pierre Jouannaud & Mitsuhiro Okada (2002): Inductive-data-type systems. Theoretical Computer Science 272(1), pp. 41–68, doi:10.1016/S0304-3975(00)00347-9.
2. Frédéric Blanqui, Jean-Pierre Jouannaud & Mitsuhiro Okada (2018): Corrigendum to “Inductive-data-type systems” [Theoret. Comput. Sci. 272 (1–2) (2002) 41–68]. Theoretical Computer Science, doi:10.1016/j.tcs.2018.01.010.
3. Wilfried Buchholz (1987): An independence result for (Π^1_1-CA)+BI. Annals of Pure and Applied Logic 33, pp. 131–155, doi:10.1016/0168-0072(87)90078-9.
4. Nachum Dershowitz (1987): Termination of rewriting. Journal of Symbolic Computation 3(1), pp. 69–115, doi:10.1016/S0747-7171(87)80022-6.
5. Nachum Dershowitz & Jean-Pierre Jouannaud (1990): Rewrite Systems. In: Jan van Leeuwen: Handbook of Theoretical Computer Science (Vol. B). MIT Press, Cambridge, MA, USA, pp. 243–320.
6. Nachum Dershowitz & Iddo Tzameret (2003): Gap Embedding for Well-Quasi-Orderings.. Electronic Notes in Theoretical Computer Science 84, pp. 80–90, doi:10.1016/S1571-0661(04)80846-6.
7. Masahiro Hamano & Mitsuhiro Okada (1998): A direct independence proof of Buchholz's Hydra Game on finite labeled trees. Archive for Mathematical Logic 37(2), pp. 67–89, doi:10.1007/s001530050084.
8. Ariya Isihara (2007): Hydra Games and Tree Ordinals. In: Daniel Leivant & Ruy de Queiroz: Logic, Language, Information and Computation. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 238–247, doi:10.1007/978-3-540-73445-1_17.
9. J. P. Jouannaud & M. Okada (1991): A computation model for executable higher-order algebraic specification languages. In: [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp. 350–361, doi:10.1109/LICS.1991.151659.
10. Mitsuhiro Okada (1987): A Simple Relationship between Buchholz's New System of Ordinal Notations and Takeuti's System of Ordinal Diagrams. The Journal of Symbolic Logic 52(3), pp. 577–581, doi:10.2969/jmsj/01340346.
11. Mitsuhiro Okada (1988): Note on a Proof of the Extended Kirby-Paris Theorem on Labeled Finite Trees. European Journal of Combinatorics 9(3), pp. 249–253, doi:10.1016/S0195-6698(88)80016-7.
12. Mitsuhiro Okada & Gaisi Takeuti (1987): On the theory of quasi-ordinal diagrams. In: Logic and combinatorics (Arcata, Calif., 1985), Contemp. Math. 65. Amer. Math. Soc., Providence, RI, pp. 295–308, doi:10.1090/conm/065/891255.
13. Gaisi Takeuti (1987): Proof Theory, second edition, Studies in Logic and the Foundations of Mathematics 81. North-Holland, Amsterdam.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org