Abstract
This paper shows how a dialogue system for information-seekingdialogues can be implemented in a type-theory-based syntax editor,originally developed for editing mathematical proofs.The implementation gives a simple logical metatheory tosuch dialogue systems and also suggests new functions forthem, e.g., a local undo operation. The method developed provides alogically based declarative way of implementing simple dialoguesystems that is easy to port to new domains.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Black, A.W., 1999, “The festival speech synthesis system,” http://www.cstr.ed.ac.uk/projects/festival/
Bohlin, P., Bos, J., Larsson, S., Lewin, I., Matheson, C., and Milward, D., 1999, “Survey of existing interactive systems,” Trindi deliverable D1.3, Gothenburg University, Gothenburg.
Coquand, C. and Coquand, T., 1999, “Structured type theory,” in Workshop on Logical Frameworkds and Meta-Languages, Paris, France, A. Felty, ed. Available in http://www.cs.belllabs.com/who/felty/LFM99
Donzeau-Gouge, V., Huet, G., Kahn, G., Lang, B., and Levy, J.J., 1975, “A structure-oriented program editor: a first step towards computer assisted programming,” Technical Report 114, IRIA-LABORIA, France.
Dymetman, M., Lux, V., and Ranta, A., 2000, “XML and multilingual document authoring: Convergent trends,” pp. 243-249 in Proceedings of Computational Linguistics COLING, Saarbrücken, Germany, International Committee on Computational Linguistics.
Ericsson, S.I. and Rupp, C.J., 2000, “Dialogue moves in negotiative dialogues,” Siridus deliverable D1.2, SRI International, Cambridge.
Gabriel Amores, J. and Quesada, J.F., 2000, “Dialogue moves in natural command languages,” Siridus deliverable D1.1, SRI International, Cambridge.
Hipp, D.R., 1994, Spoken Natural Language Dialogue Systems, Oxford: Oxford University Press.
Larsson, S. and Traum, D., 2001, “Information state and dialogue management in the Trindi Dialogue Move Engine Toolkit,” Natural Language Engineering, Special Issue on Best Practice in Spoken Language Dialogue Systems Engineering, to appear.
Magnusson, L., 1996, “An algorithm for checking incomplete proof objects in type theory with localization and unification,” pp. 183-200 in Types For Proofs and Programs, S. Berardi and M. Coppo, eds., Berlin: Springer-Verlag.
Magnusson, L. and Nordström, B., 1994, “The ALF proof editor and its proof engine,” pp. 213-237 in Types for Proofs and Programs, H. Barendregt and T. Nipkow, eds., Berlin: Springer-Verlag.
Martin-Löf, P., 1984, Intuitionistic Type Theory, Napoli: Bibliopolis.
Paulson, L.C., 1990, “Isabelle: The next 700 theorem provers,” pp. 361-386 in Logic and Computer Science, P. Odifreddi, ed., London: Academic Press.
Raman, T.V., 1994, “Audio system for technical readings,” Ph.D. Thesis, Cornell University.
Ranta, A., 1994, Type Theoretical Grammar, Oxford: Oxford University Press.
Ranta, A., 2000, “Grammatical framework homepage,” http://www.cs.chalmers.se/~aarne/GF/
Ranta, A., 2004, “Grammatical framework: A type-theoretical grammar formalism,” The Journal of Functional Programming 14, 145-189.
The Coq Team, 1999, “Coq Homepage,” http://pauillac.inria.fr/coq/
Thompson, S., 1999, Haskell the Craft of Functional Programming, 2nd edition, Harlow: Addison-Wesley.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Ranta, A., Cooper, R. Dialogue Systems as Proof Editors. Journal of Logic, Language and Information 13, 225–240 (2004). https://doi.org/10.1023/B:JLLI.0000024736.34644.48
Issue Date:
DOI: https://doi.org/10.1023/B:JLLI.0000024736.34644.48