isabelle-93

1 definition found

isabelle-93 - Free On-line Dictionary of Computing (26 May 2007) :

  Isabelle
  Isabelle-92
  Isabelle-93
  
     <theory, tool> A generic theorem prover with support for
     several object-logics, developed by Lawrence C. Paulson
     <Larry.Paulson@cl.cam.ac.uk> in collaboration with Tobias Nipkow (http://in.tum.de/~nipkow/)
      at the Technical University of Munich
     .
  
     A system of type classes allows polymorphic object-logics
     with overloading and automatic type inference.
  
     Isabelle supports first-order logic - constructive and
     classical versions; higher-order logic, similar to Gordon's
     HOL; Zermelo Frankel set theory; an extensional version
     of Martin Lof's type theory, the classical first-order
     sequent calculus, LK; the modal logics T, S4, and
     S43; and Logic for Computable Functions.
  
     An object logic's syntax and inference rules are specified
     declaratively allowing single-step proof construction.
     Proof procedures can be expressed using "tactics" and
     "tacticals".  Isabelle provides control structures for
     expressing search procedures and generic tools such as
     simplifiers and classical theorem provers which can be applied
     to object-logics.  Isabelle is built on top of Standard ML
     and uses its user interface.
  
     (http://cl.cam.ac.uk/Research/HVG/Isabelle/).
  
     Mailing list: isabelle-users@cl.cam.ac.uk.
  
     ["tactics"?  "tacticals"?]
  
     (1999-07-26)