Skip to main content
SpringerLink
Log in

Goal Reasoning with Context Record Types

  • Conference paper
Modeling and Using Context (CONTEXT 2007)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 4635))

  • 1389 Accesses

Abstract

The concept of goal is central in Artificial Intelligence and its modelling is a challenging issue. It has been given much attention in areas such as Requirement Engineering (RE) and Planning and Scheduling, where its modelling can support formal reasoning through goal types, goal attributes and relations to other components. However there is a lack of formalisms able to reason with goal structures in dynamic environments. We claim that a logical framework based on Intuitionistic Type Theory and more precisely, on Dependent Record Types is able to address this problem. The formal foundations rely on context modelling through dependent record types allowing partial knowledge and dynamic reasoning. For the purpose of goal modelling, we introduce a family of functions which map Context Record Types to Intentional Record Types expressing their related actions and goals. A case study in planning illustrates this approach.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Betarte, G.: Type checking dependent (record) types and subtyping. Journal of Functional and Logic Programming 10(2), 137–166 (2000)

    Article  MATH  Google Scholar 

  2. Boldini, P.: Formalizing Context in Intuitionistic Type theory. Fundamenta Informaticae 42, 1–23 (2000)

    Google Scholar 

  3. Bove, A., Capretta, V.: Nested General Recursion and Partiality in Type Theory TPHOL R. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 121–135. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  4. Cooper, R.: Records and Record Types in Semantic Theory. Journal of Logic and Computation 15(2), 99–112 (2005)

    Article  MATH  Google Scholar 

  5. Coquand, C., Coquand, T.: Structured type theory. In: Workshop on Logical Frameworks and Meta-languages (1999)

    Google Scholar 

  6. Coquand, T., Pollack, R., Takeyama, M.: A Logical Framework with Dependently Typed Records. Fundamenta Informaticae 20, 1–22 (2005)

    Google Scholar 

  7. Dapoigny, R., Barlatier, P.: Dependent Record Types for Dynamic context representation. In: Bramer, M., Coenen, F., Tuson, A. (eds.) Research and Development in Intelligent Systems: Procs. of AI-06, vol. 23, Springer, Heidelberg (2006)

    Google Scholar 

  8. Dapoigny, R., Barlatier, P.: Towards a Context Theory for Context-aware systems. In: Procs. of the 2nd IJCAI Workshop on Artificial Intelligence Techniques for Ambient Intelligence (2007)

    Google Scholar 

  9. Friesen, A., Börger, E.: A High-Level Specification for Semantic Web Service Discovery Services. In: Procs. of the sixth ACM Workshop ICWE 2006, pp. 16–23. ACM Press, New York (2006)

    Chapter  Google Scholar 

  10. Gil, Y.: Description Logics and Planning. AI Magazine 26(2), 73–84 (2005)

    Google Scholar 

  11. Ginzburg, J.: Abstraction and Ontology: Questions as Propositional Abstracts in Type Theory with Records. Journal of Log. Comput. 15(2), 113–130 (2005)

    Article  MATH  Google Scholar 

  12. Giunchiglia, F.: Contextual Reasoning. Istituto per la Ricerca Scientifica e Technologica, 9211-9220 (1992)

    Google Scholar 

  13. Ghidini, C., Giunchiglia, F.: Local Models Semantics, or Contextual Reasoning = Locality + Compatibility. Artificial Intelligence 127(2), 221–259 (2001)

    Article  MATH  Google Scholar 

  14. Hoffman, G., Breazeal, C.: Collaboration in Human-Robot Teams. In: Procs. of AIAA First Intelligent Systems Technical Conference (2004)

    Google Scholar 

  15. Howard, W.A, Seldin, J.P., Hindley, J.R.: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. The formulae-as-types notion of construction, pp. 479–490. Academic Press, London (1980)

    Google Scholar 

  16. Keller U., Lara R., Polleres A., Toma I., Kifer M., Fensel D.: WSMO Web Service Discovery DERI International, D5.1 v0.1 (2004)

    Google Scholar 

  17. Kopylov, A.: Dependent Intersection: A New Way of Defining Records in Type Theory. In: Procs. of the 18th Annual IEEE Symposium on Logic in Computer Science, pp. 86–95. IEEE Computer Society Press, Los Alamitos (2003)

    Chapter  Google Scholar 

  18. Van Lamsweerde, A.: Goal-Oriented Requirements Engineering: A Guided Tour. In: Procs. of the 5th IEEE International Symposium on Requirements Engineering, pp. 249–263. IEEE Computer Society Press, Los Alamitos (2001)

    Google Scholar 

  19. Martin-Lof, P.: Constructive Mathematics and Computer Programming. Methodology and Philosophy of Sciences 6, 153–175 (1982)

    Google Scholar 

  20. McCarthy, J.: Notes on Formalizing Context. In: Procs. of the 13th Int. Joint Conf. on Artificial Intelligence, pp. 555–560 (1993)

    Google Scholar 

  21. Nau, D., Cao, Y., Lotem, A., Munoz-Avila, H.: SHOP: Simple Hierarchical Ordered Planner. In: Procs. of the Sixteenth International Joint Conference on Artificial Intelligence, pp. 968–983 (1999)

    Google Scholar 

  22. Paulson, L.C.: The Foundation of a Generic Theorem Prover. Journal of Automated Reasoning 5, 363–397 (1989)

    Article  MATH  Google Scholar 

  23. Pollock, J.: The logical foundations of goal-regression planning in autonomous agents. Artificial Intelligence 106, 267–335 (1998)

    Article  MATH  Google Scholar 

  24. Prat, N.: Goal formalisation and classification for requirements engineering. In: Procs. of the Third International Workshop on Requirements Engineering: Foundations of Software Quality, pp. 145–156 (1997)

    Google Scholar 

  25. Ranta, A.: Grammatical Framework: A Type-Theoretical Grammar Formalism. Journal of Functional Programming 14(2), 145–189 (2004)

    Article  MATH  Google Scholar 

  26. Rolland, C., Ben Achour, C.: Guiding The Construction Of Textual Use Case Specifications. Data and Knowledge Engineering Journal 25(1-2), 125–160 (1998)

    Article  MATH  Google Scholar 

  27. Sirin, E., Parsia, B., Wu, D., Hendler, J., Nau, D.: HTN planning for web service composition using SHOP2. Journal of Web Semantics 1(4), 377–396 (2004)

    Google Scholar 

  28. Thomason, R.H.: Representing and Reasoning with Context. In: Calmet, J., Plaza, J. (eds.) AISC 1998. LNCS (LNAI), vol. 1476, pp. 29–41. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  29. Thomason, R.H.: Type theoretic foundations for context, part 1: Contexts as complex typetheoretic objects. In: Bouquet, P., Serafini, L., Brézillon, P., Benercetti, M., Castellani, F. (eds.) CONTEXT 1999. LNCS (LNAI), vol. 1688, pp. 352–374. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  30. Valentini, S.: Decidability in Intuitionistic Type Theory is functionally decidable. Mathematical Logic 42, 300–304 (1996)

    Article  MATH  Google Scholar 

  31. Villadsen, J.: Multi-dimensional Type Theory: Rules, Categories, and Combinators for Syntax and Semantics. In: Christiansen, H., et al. (eds.) Int. Workshop on Constraint Solving and Language Processing, pp. 160–165 (2004)

    Google Scholar 

  32. Weld, D.: Recent advances in AI planning. AI Magazine 20(2), 93–123 (1999)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Université de Savoie, ESIA Laboratoire d’Informatique, Sytèmes, Traitement de l’Information et de la Connaissance B.P. 806, F-74016 ANNECY Cedex, France

    Richard Dapoigny & Patrick Barlatier

Authors
  1. Richard Dapoigny
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Patrick Barlatier
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Boicho Kokinov Daniel C. Richardson Thomas R. Roth-Berghofer Laure Vieu

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dapoigny, R., Barlatier, P. (2007). Goal Reasoning with Context Record Types. In: Kokinov, B., Richardson, D.C., Roth-Berghofer, T.R., Vieu, L. (eds) Modeling and Using Context. CONTEXT 2007. Lecture Notes in Computer Science(), vol 4635. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74255-5_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-74255-5_13

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-74254-8

  • Online ISBN: 978-3-540-74255-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation