An Infrastructure for Intertheory Reasoning

1. Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth through Proof. Academic Press, London (1986)

   MATH  Google Scholar 

2. Burstall, R., Goguen, J.: The semantics of Clear, a specification language. In: Bjorner, D. (ed.) Abstract Software Specifications. LNCS, vol. 86, pp. 292–332. Springer, Heidelberg (1980)

   Google Scholar 

3. Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic 5, 56–68 (1940)

   Article  MATH  MathSciNet  Google Scholar 

4. Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, London (1972)

   MATH  Google Scholar 

5. Farmer, W.M.: A partial functions version of Church’s simple theory of types. Journal of Symbolic Logic 55, 1269–1291 (1990)

   Article  MATH  MathSciNet  Google Scholar 

6. Farmer, W.M.: A simple type theory with partial functions and subtypes. Annals of Pure and Applied Logic 64, 211–240 (1993)

   Article  MATH  MathSciNet  Google Scholar 

7. Farmer, W.M.: A general method for safely overwriting theories in mechanized mathematics systems. Technical report, The MITRE Corporation (1994)

   Google Scholar 

8. Farmer, W.M.: Theory interpretation in simple type theory. In: Heering, J., Meinke, K., Möller, B., Nipkow, T. (eds.) HOA 1993. LNCS, vol. 816, pp. 96–123. Springer, Heidelberg (1994)

   Google Scholar 

9. Farmer, W.M., Guttman, J.D., Thayer Fábrega, F.J.: IMPS: An updated system description. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 8–302. Springer, Heidelberg (1996)

   Google Scholar 

10. Farmer, W.M., Guttman, J.D., Thayer, F.J.: Little theories. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 567–581. Springer, Heidelberg (1992)

    Google Scholar 

11. Farmer, W.M., Guttman, J.D., Thayer, F.J.: IMPS: An Interactive Mathematical Proof System. Journal of Automated Reasoning 11, 213–248 (1993)

    Article  MATH  Google Scholar 

12. Goguen, J.A., Winkler, T.: Introducing OBJ3. Technical Report SRI-CSL-99-9, SRI International (August 1988)

    Google Scholar 

13. Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

14. Hamilton, N., Nickson, R., Traynor, O., Utting, M.: Interpretation and instantiation of theories for reasoning about formal specifications. In: Pate, M. (ed.) Proceedings of the Twentieth Australasian Computer Science Conference. Australian Computer Science Communications, vol. 19, pp. 37–45 (1997)

    Google Scholar 

15. Kaufmann, M., Moore, J.S.: Structured theory development for a mechanized logic (1999), Available at http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html

16. Nakajima, R., Yuasa, T. (eds.): The IOTA Programming System. LNCS, vol. 160. Springer, Heidelberg (1982)

    Google Scholar 

17. Nickson, R., Traynor, O., Utting, M.: Cogito ergo sum–providing structured theorem prover support for specification formalisms. In: Ramamohanarao, K. (ed.) Proceedings of the Nineteenth Australian computer science conference. Australian Computer Science Communications, vol. 18, pp. 149–158 (1997)

    Google Scholar 

18. Rushby, J., von Henke, F., Owre, S.: An introduction to formal specification and verification using EHDM. Technical Report SRI-CSL-91-02, SRI International (1991)

    Google Scholar 

19. Shoenfield, J.R.: Mathematical Logic. Addison-Wesley, Reading (1967)

    MATH  Google Scholar 

20. Smith, D.: KIDS: A knowledge-based software development system. In: Lowry, M., McCartney, R. (eds.) Automating Software Design, pp. 483–514. MIT Press, Cambridge (1991)

    Google Scholar 

21. Srinivas, Y., Jullig, R.: Specware: Formal support for composing software. In: Proceedings of the Conference on Mathematics of Program Construction (1995)

    Google Scholar 

Download references